-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
T : Triangle.{v, u} C
rw :
  HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
      (a + b).negOnePow
      (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₃ ≫
        NatTrans.app (Iso.hom (shiftFunctorComm C 1 (a + b))) T.obj₁ ≫
          Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₁)) =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
      (b.negOnePow * a.negOnePow)
      (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₃ ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁) ≫
          Functor.map (CategoryTheory.shiftFunctor C b) (NatTrans.app (Iso.hom (shiftFunctorComm C 1 a)) T.obj₁) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm C 1 b))
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁))
⊢ HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₁))
        (a + b).negOnePow
        (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorComm C 1 (a + b))) T.obj₁ :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₁)) ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₁) =
    NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₃ ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃) ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
        b.negOnePow
        (Functor.map (CategoryTheory.shiftFunctor C b)
              (HSMul.hSMul (β :=
                Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃ ⟶
                  Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
                    (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁))
                a.negOnePow
                (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₃ ≫
                    NatTrans.app (Iso.hom (shiftFunctorComm C 1 a)) T.obj₁ :
                  Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃ ⟶
                    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
                      (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁))) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm C 1 b))
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁) :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃) ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
                (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))

Tactic:
rw [Linear.units_smul_comp, Linear.comp_units_smul, Functor.map_units_smul,
          Linear.units_smul_comp, Linear.comp_units_smul, smul_smul, assoc, Functor.map_comp, assoc,
          ← dsimp% (CategoryTheory.shiftFunctorAdd' C a b (a + b) rfl).hom.naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.units_smul_comp, smul_smul, CategoryTheory.shiftFunctorAdd', CategoryTheory.Linear.comp_units_smul, CategoryTheory.Functor.map_units_smul, HAdd.hAdd, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.naturality_assoc, rfl