∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {g : X ⟶ Y} {c : CategoryTheory.Limits.KernelFork g} (hc : CategoryTheory.Limits.IsLimit c) {X' Y' : C}
  (g' : X' ⟶ Y') (e : X ≅ X')
  (iff :
    ∀ ⦃W : C⦄ (φ : W ⟶ X),
      CategoryTheory.CategoryStruct.comp φ g = 0 ↔
        CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp e.hom g') = 0)
  {W' : C} (s : W' ⟶ X') (hs : CategoryTheory.CategoryStruct.comp s g' = 0)
  (m :
    W' ⟶
      ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj c.pt).obj
        CategoryTheory.Limits.WalkingParallelPair.zero),
  CategoryTheory.CategoryStruct.comp m (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) e.hom) = s →
    CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.Fork.ι c) =
      CategoryTheory.CategoryStruct.comp
        ((fun {W'} s hs =>
            hc.lift (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.CategoryStruct.comp s e.inv) ⋯))
          s hs)
        (CategoryTheory.Limits.Fork.ι c)