∀ {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 φ.τ₂]
  (wi : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h.i (CategoryTheory.inv φ.τ₂)) S₁.g = 0)
  (hi :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.CategoryStruct.comp h.i (CategoryTheory.inv φ.τ₂)) wi)),
  CategoryTheory.CategoryStruct.comp (hi.lift (CategoryTheory.Limits.KernelFork.ofι S₁.f ⋯))
      (CategoryTheory.Limits.Fork.ι
        (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.CategoryStruct.comp h.i (CategoryTheory.inv φ.τ₂)) wi)) =
    CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.ofι S₁.f ⋯)