-- 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ᵒᵖᵒᵖ
w :
  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))
⊢ 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)
    (NatTrans.app (Iso.hom (iso C (p + q))) X) (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (iso C p) (iso C q))) X)

Tactic:
simp only [Functor.CommShift.isoAdd_hom_app, op_comp,
      ← shiftFunctorAdd'_eq_shiftFunctorAdd, Functor.map_comp,
      fun X n ↦ iso_hom_app X n (-n) (add_neg_cancel n),
      shiftFunctorAdd'_op_hom_app _ p q (p + q) rfl (-p) (-q) (-(p + q))
        (add_neg_cancel p) (add_neg_cancel q) (add_neg_cancel (p + q)),
      shiftFunctorAdd'_op_inv_app _ (-p) (-q) (-(p + q)) (by lia) p q (p + q)
        (neg_add_cancel p) (neg_add_cancel q) (neg_add_cancel (p + q)),
      shiftFunctor_op_map _ (-q) q, shiftFunctor_op_map _ q (-q)]

Premises used: CategoryTheory.Functor.CommShift.isoAdd_hom_app, add_neg_cancel, CategoryTheory.op_comp, CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_hom_app, CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_inv_app, neg_add_cancel, HAdd.hAdd, CategoryTheory.Pretriangulated.shiftFunctor_op_map, CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app, CategoryTheory.Functor.map_comp, Neg.neg, rfl, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd