-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasDerivedCategory.{t, v, u} C
inst_8 : HasDerivedCategory.{t', v', u'} D
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
rw :
  Eq.{t' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
        (Functor.obj Q (CochainComplex.mappingCone S.f)))
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
        (Functor.obj (shiftFunctor (DerivedCategory.{t, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁))))
    (Functor.map F.mapDerivedCategory
      (Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁))
    (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) (CochainComplex.mappingCone S.f) ≫
      CategoryStruct.comp (Y :=
        Functor.obj Q
          (Functor.obj (shiftFunctor (CochainComplex.{v', u', 0} D ℤ) (A := ℤ) 1)
            (Pretriangulated.Triangle.obj₁
              (CochainComplex.mappingCone.triangle (K :=
                ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))
                (ShortComplex.f (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))))))
        (Functor.map Q
          (CategoryStruct.comp (Y :=
            CochainComplex.mappingCone (F := Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)
              (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.f))
            (Iso.hom (CochainComplex.mappingCone.mapHomologicalComplexIso S.f F) :
              Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
                (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) (CochainComplex.mappingCone S.f))
                (CochainComplex.mappingCone (F := Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)
                  (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.f)))
            (Pretriangulated.Triangle.mor₃
                (CochainComplex.mappingCone.triangle (K :=
                  ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))
                  (ShortComplex.f (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))) :
              Quiver.Hom (V := CochainComplex.{v', u', 0} D ℤ)
                (Pretriangulated.Triangle.obj₃
                  (CochainComplex.mappingCone.triangle (K :=
                    ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))
                    (ShortComplex.f (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))))
                (Functor.obj (shiftFunctor (CochainComplex.{v', u', 0} D ℤ) (A := ℤ) 1)
                  (Pretriangulated.Triangle.obj₁
                    (CochainComplex.mappingCone.triangle (K :=
                      ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))
                      (ShortComplex.f (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))))))))
        (CategoryStruct.comp (Y :=
          Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
            (Functor.obj Q (ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))))
          (NatTrans.app (Iso.hom (Functor.commShiftIso Q 1))
            (ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ)))))
          (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
              (NatTrans.app (Iso.inv F.mapDerivedCategoryFactors) S.X₁) ≫
            NatTrans.app (Iso.inv (Functor.commShiftIso F.mapDerivedCategory 1)) (Functor.obj Q S.X₁))))
⊢ Eq.{t' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory (Functor.obj Q S.X₃))
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
        (Functor.obj (shiftFunctor (DerivedCategory.{t, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁))))
    (Functor.map F.mapDerivedCategory (triangleOfSESδ hS))
    (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) S.X₃ ≫
      CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (Functor.obj Q (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)))
        (triangleOfSESδ ⋯)
        (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
            (NatTrans.app (Iso.inv F.mapDerivedCategoryFactors) S.X₁) ≫
          NatTrans.app (Iso.inv (Functor.commShiftIso F.mapDerivedCategory 1)) (Functor.obj Q S.X₁)))

Tactic:
rw [← cancel_epi (F.mapDerivedCategory.map
    (Q.map (CochainComplex.mappingCone.descShortComplex S))), ← Functor.map_comp,
    descShortComplex_triangleOfSESδ, F.mapDerivedCategoryFactors_hom_naturality_assoc,
    ← CochainComplex.mappingCone.mapHomologicalComplexIso_hom_descShortComplex,
    Functor.map_comp_assoc, descShortComplex_triangleOfSESδ_assoc, Category.assoc,
    ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CochainComplex.mappingCone.descShortComplex, DerivedCategory.Q, CategoryTheory.Functor.mapDerivedCategory, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality_assoc, CochainComplex.mappingCone.mapHomologicalComplexIso_hom_descShortComplex, CategoryTheory.Functor.map_comp, DerivedCategory.descShortComplex_triangleOfSESδ, DerivedCategory.descShortComplex_triangleOfSESδ_assoc, CategoryTheory.cancel_epi