∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ),
  CategoryTheory.CategoryStruct.comp (-(CochainComplex.mappingCone.inl φ).v (n + 1) n ⋯)
      ((CochainComplex.mappingCone.triangleRotateShortComplex φ).map
          (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).g =
    CategoryTheory.CategoryStruct.id
      ((CochainComplex.mappingCone.triangleRotateShortComplex φ).map
          (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).X₃