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

Tactic:
simp [← Functor.map_comp_assoc, ← unop_comp, ← unop_comp_assoc]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.unop_comp_assoc