∀ {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) [inst_2 : CategoryTheory.IsIso φ.τ₂]
  [inst_3 : CategoryTheory.Mono φ.τ₃] {W' : C} (x : W' ⟶ S₂.X₂) (hx : CategoryTheory.CategoryStruct.comp x S₂.g = 0)
  (b : W' ⟶ h.K),
  CategoryTheory.CategoryStruct.comp b (CategoryTheory.CategoryStruct.comp h.i φ.τ₂) = x →
    b = (fun {W'} x hx => h.liftK (CategoryTheory.CategoryStruct.comp x (CategoryTheory.inv φ.τ₂)) ⋯) x hx