∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K X Y : Cᵒᵖ} (i : K ⟶ X) {f : X ⟶ Y} (w : CategoryTheory.CategoryStruct.comp i f = 0)
  (h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i w)) {Z' : C} (x : Opposite.unop X ⟶ Z')
  (hx : CategoryTheory.CategoryStruct.comp f.unop x = 0) (b : Opposite.unop K ⟶ Z'),
  CategoryTheory.CategoryStruct.comp i.unop b = x →
    CategoryTheory.CategoryStruct.comp b.op (CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.ofι i w)) =
      CategoryTheory.CategoryStruct.comp
        ((fun {Z'} x hx => (h.lift (CategoryTheory.Limits.KernelFork.ofι x.op ⋯)).unop) x hx).op
        (CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.ofι i w))