∀ {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),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ).rotate.mor₂
      (CategoryTheory.Iso.refl (CochainComplex.mappingCone.triangle φ).rotate.obj₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CochainComplex.mappingCone.triangle φ).rotate.obj₂).hom
      (CochainComplex.triangleOfDegreewiseSplit (CochainComplex.mappingCone.triangleRotateShortComplex φ)
          (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ)).mor₂