-- 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 c : ℤ
T : Triangle.{v, u} C
h₃ :
  Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T.obj₃ ≫
        Functor.map (CategoryTheory.shiftFunctor C c)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₃) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))
    (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + (b + c))) T.obj₃)
        (TriangleMorphism.hom₃ (eqToHom ⋯))
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + (b + c)) ⋯)) T.obj₃ ≫
          Functor.map (CategoryTheory.shiftFunctor C c)
            (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₃)) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T.obj₃ ≫
        Functor.map (CategoryTheory.shiftFunctor C c)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₃) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))
    (TriangleMorphism.hom₃ (eqToHom ⋯) ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T.obj₃ ≫
          NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C b c (b + c) ⋯))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))

Tactic:
rw [← shiftFunctorAdd'_assoc_hom_app a b c _ _ _ rfl rfl (add_assoc a b c)]

Premises used: add_assoc, rfl, CategoryTheory.shiftFunctorAdd'_assoc_hom_app