{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {g : X ⟶ Y} →
          {c : CategoryTheory.Limits.KernelFork g} →
            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) →
                      CategoryTheory.Limits.IsLimit
                        (CategoryTheory.Limits.KernelFork.ofι
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) e.hom) ⋯)