∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {Z : C} (l : Z ⟶ X) {s : CategoryTheory.Limits.KernelFork f} (hs : CategoryTheory.Limits.IsLimit s)
  (i : Z ≅ s.pt) (h : CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.Fork.ι s) = l),
  CategoryTheory.Limits.IsKernel.isoKernel f l hs i h = hs.ofIsoLimit (CategoryTheory.Limits.Cones.ext i.symm ⋯)