∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cocycle K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m),
  CochainComplex.HomComplex.δ n m β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0 →
    CochainComplex.HomComplex.δ n m (CochainComplex.mappingCone.liftCochain φ (↑α) β h) = 0