∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) {Z' : C} (x : Y ⟶ Z') (x_1 : CategoryTheory.CategoryStruct.comp f x = 0) (x_2 : Y ⟶ Z'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) x_2 = x → x_2 = (fun {Z'} x x_3 => x) x x_1