∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  CochainComplex.HomComplex.δ 0 1
        (CochainComplex.mappingCone.descCochain g 0
          (CochainComplex.HomComplex.Cochain.ofHom
            (CochainComplex.mappingCone.inr (CategoryTheory.CategoryStruct.comp f g)))
          ⋯) +
      (↑(CochainComplex.mappingCone.descCocycle g
              (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr f)) 0 ⋯ ⋯)).comp
        (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingConeCompTriangle f g).mor₁) ⋯ =
    0