-- Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
      CategoryStruct.comp (Y := Functor.obj (singleFunctor C 0) S₂.X₃)
        (Functor.map Q (Functor.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0) f.τ₃) :
          Quiver.Hom (V := DerivedCategory.{w, v, u} C)
            (Functor.obj Q (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) 0) S₁.X₃))
            (Functor.obj Q (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) 0) S₂.X₃)))
        (CategoryStruct.comp (Y :=
            Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁))
            (triangleOfSESδ ⋯ :
              Quiver.Hom (V := DerivedCategory.{w, v, u} C)
                (Functor.obj Q (X₃ (S₂.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))))
                (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
                  (Functor.obj Q (X₁ (S₂.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))))))
            (Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
              (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁)) :
          Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₂.X₃)
            (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
              (Functor.obj (singleFunctor C 0) S₂.X₁))))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
      triangleOfSESδ ⋯ ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (Functor.map Q (Functor.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0) f.τ₁)) ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))

Tactic:
rw [reassoc_of% dsimp% ((triangleOfSES.map (h₁.map_of_exact _) (h₂.map_of_exact _))
      ((HomologicalComplex.single C (.up ℤ) 0).mapShortComplex.map f)).comm₃]

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, Int, CategoryTheory.Functor.map, DerivedCategory.triangleOfSES.map, CategoryTheory.Functor.mapShortComplex, OfNat.ofNat, CategoryTheory.ShortComplex.ShortExact.map_of_exact, ComplexShape.up, HomologicalComplex.single