∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] (K : CochainComplex C ℤ),
  (CochainComplex.HomComplex.Cochain.ofHom
          (CategoryTheory.CategoryStruct.id
            (CochainComplex.mappingCone (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))))).comp
      (CochainComplex.mappingCone.snd (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))) ⋯ =
    CochainComplex.HomComplex.δ (-1) 0 0 +
        (CochainComplex.mappingCone.snd (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))).comp
          (CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))) ⋯ +
      (CochainComplex.HomComplex.Cochain.ofHom 0).comp
        (CochainComplex.mappingCone.snd (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))) ⋯