∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  (s : CategoryTheory.Limits.Fork (CategoryTheory.Limits.biprod.desc f (-g)) 0)
  (m : s.pt ⟶ (CategoryTheory.Abelian.PullbackToBiproductIsKernel.pullbackToBiproductFork f g).pt),
  CategoryTheory.CategoryStruct.comp m
        (CategoryTheory.Limits.Fork.ι
          (CategoryTheory.Abelian.PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) =
      s.ι →
    m =
      (fun s =>
          CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp s.ι CategoryTheory.Limits.biprod.fst)
            (CategoryTheory.CategoryStruct.comp s.ι CategoryTheory.Limits.biprod.snd) ⋯)
        s