∀ {C : Type u_4} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F G : CochainComplex C ℤ} (φ : F ⟶ G)
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)] (n m : ℤ)
  (hnm : n + 1 = m),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
          ((↑(CochainComplex.mappingCone.fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n m ⋯)
          (H.map ((CochainComplex.mappingCone.inl φ).v m n ⋯)) +
        CategoryTheory.CategoryStruct.comp
          ((CochainComplex.mappingCone.snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯)
          (H.map ((CochainComplex.mappingCone.inr φ).f n)))
      (CategoryTheory.CategoryStruct.comp (H.map ((↑(CochainComplex.mappingCone.fst φ)).v n m ⋯))
          ((CochainComplex.mappingCone.inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n ⋯) +
        CategoryTheory.CategoryStruct.comp (H.map ((CochainComplex.mappingCone.snd φ).v n n ⋯))
          ((CochainComplex.mappingCone.inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n)) =
    CategoryTheory.CategoryStruct.id
      ((CochainComplex.mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).X n)