-- 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
dsimp :
  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₁)))
⊢ (Functor.obj (shiftFunctor C (a + b)) T).mor₃ ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₁)) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₃) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₃

Tactic:
dsimp