∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)]
  [inst_4 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
  (i j : ι) (hij : c.Rel j i),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inlX K i j hij)
      ((HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K).f j) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inlX K i j hij)
      ((CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) (HomologicalComplex.cylinder.ι₀ K) -
            CategoryTheory.CategoryStruct.id K.cylinder).f
        j)