∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.LeftHomologyData)
  (wi : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h.i φ.τ₂) S₂.g = 0)
  (hi :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.CategoryStruct.comp h.i φ.τ₂) wi))
  (hf' : CategoryTheory.CategoryStruct.comp φ.τ₁ (hi.lift (CategoryTheory.Limits.KernelFork.ofι S₂.f ⋯)) = h.f')
  {Z' : C} (x : h.K ⟶ Z')
  (hx : CategoryTheory.CategoryStruct.comp (hi.lift (CategoryTheory.Limits.KernelFork.ofι S₂.f ⋯)) x = 0)
  (b : h.H ⟶ Z'), CategoryTheory.CategoryStruct.comp h.π b = x → b = (fun {Z'} x hx => h.descH x ⋯) x hx