∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact)
  (this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃
      ((CategoryTheory.shiftFunctor (DerivedCategory C) 1).map
        (CategoryTheory.Iso.refl
            (DerivedCategory.Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.asIso (DerivedCategory.Q.map (CochainComplex.mappingCone.descShortComplex S))).hom
      (DerivedCategory.triangleOfSES hS).mor₃