∀ {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),
  CochainComplex.HomComplex.Cochain.ofHom
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.mappingCone.desc (CochainComplex.mappingCone.inr φ) 0
          (CochainComplex.mappingCone.triangle φ).mor₃ ⋯)
        (CochainComplex.mappingCone.lift (CochainComplex.mappingCone.inr φ)
          (-(CochainComplex.HomComplex.Cocycle.ofHom φ).leftShift 1 1 ⋯)
          (-(CochainComplex.mappingCone.inl φ).leftShift 1 0 ⋯) ⋯)) =
    CochainComplex.HomComplex.δ (-1) 0
        (-(CochainComplex.mappingCone.snd (CochainComplex.mappingCone.inr φ)).comp
            ((CochainComplex.mappingCone.snd φ).comp (CochainComplex.mappingCone.inl (CochainComplex.mappingCone.inr φ))
              ⋯)
            ⋯) +
      CochainComplex.HomComplex.Cochain.ofHom
        (CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone (CochainComplex.mappingCone.inr φ)))