∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L)
  {Z : HomotopyCategory C (ComplexShape.up ℤ)}
  (h :
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
        (CochainComplex.mappingCone (CochainComplex.mappingCone.inr φ)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃)
      (CategoryTheory.CategoryStruct.comp
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom)
        h) =
    CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
        (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ)))
      h