-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
rw :
  Eq.{v_1 + 1} (α :=
    X ⟶
      Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ p) X))))
    (CategoryStruct.comp (Y :=
      Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)))
      (CategoryStruct.comp (Y :=
        Opposite.op
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-m))
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))))
        (Quiver.Hom.op
          (Functor.map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-m) m ⋯))
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)))))
        (Quiver.Hom.op
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-m))
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)))) ≫
          Quiver.Hom.op
            (Functor.map (shiftFunctor C p)
              (NatTrans.app (Iso.hom (shiftFunctorAdd' C (-n) (-m) (-p) ⋯)) (Opposite.unop X))))))
    (CategoryStruct.comp (Y :=
      Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)))
      (CategoryStruct.comp (Y :=
        Opposite.op
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))))
        (Quiver.Hom.op
          (Functor.map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-m) m ⋯))
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))
        (Quiver.Hom.op
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))) ≫
          Quiver.Hom.op
            (Functor.map (shiftFunctor C p)
              (NatTrans.app (Iso.hom (shiftFunctorAdd' C (-n) (-m) (-p) ⋯)) (Opposite.unop X))))))
⊢ Eq.{v_1 + 1} (α :=
    X ⟶
      Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ p) X))))
    (((Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)) ≫
          Quiver.Hom.op
            (Functor.map (shiftFunctor C n)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-m) m ⋯))
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))) ≫
        Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-m))
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))) ≫
      Quiver.Hom.op
        (Functor.map (shiftFunctor C p)
          (NatTrans.app (Iso.hom (shiftFunctorAdd' C (-n) (-m) (-p) ⋯)) (Opposite.unop X))))
    (CategoryStruct.comp (Y :=
      Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)))
      (CategoryStruct.comp (Y :=
        Opposite.op
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))))
        (Quiver.Hom.op
          (Functor.map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-m) m ⋯))
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))
        (Quiver.Hom.op
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))) ≫
          Quiver.Hom.op
            (Functor.map (shiftFunctor C p)
              (NatTrans.app (Iso.hom (shiftFunctorAdd' C (-n) (-m) (-p) ⋯)) (Opposite.unop X))))))

Tactic:
rw [Category.assoc, Category.assoc]

Premises used: CategoryTheory.Category.assoc