Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
p q : ℤ
X : Cᵒᵖᵒᵖ
⊢ (iso C (p + q)).hom.app X = (Functor.CommShift.isoAdd (iso C p) (iso C q)).hom.app 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)]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
p q : ℤ
X : Cᵒᵖᵒᵖ
⊢ ((shiftFunctorOpIso Cᵒᵖ (p + q) (-(p + q)) ⋯).hom.app X).unop.unop ≫
      ((shiftFunctorOpIso C (-(p + q)) (p + q) ⋯).inv.app (unop X)).unop =
    ((unopUnop C).map ((shiftFunctorOpIso Cᵒᵖ (p + q) (-(p + q)) ⋯).hom.app X) ≫
        ((((unopUnop C).map ((shiftFunctorOpIso C (-(p + q)) (p + q) ⋯).inv.app (unop X)).op ≫
                (unopUnop C).map ((shiftFunctorAdd' C p q (p + q) ⋯).hom.app (unop (unop X))).op.op) ≫
              (unopUnop C).map ((shiftFunctorOpIso C (-q) q ⋯).hom.app ((shiftFunctor C p).op.obj (unop X))).op) ≫
            ((unopUnop C).map
                  ((shiftFunctorOpIso C (-q) q
                            (CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso._proof_2 q)).inv.app
                      ((shiftFunctor C p).op.obj (unop X))).op ≫
                (unopUnop C).map
                  ((shiftFunctor C q).map ((shiftFunctorOpIso C (-p) p ⋯).hom.app (unop X)).unop).op.op) ≫
              (unopUnop C).map
                ((shiftFunctorOpIso C (-q) q
                          (CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso._proof_2 q)).hom.app
                    ((shiftFunctor Cᵒᵖ (-p)).obj (unop X))).op) ≫
          (unopUnop C).map ((shiftFunctorOpIso Cᵒᵖ q (-q) ⋯).inv.app (op ((shiftFunctor Cᵒᵖ (-p)).1 (unop X)))) ≫
            (unopUnop C).map
                ((shiftFunctorOpIso Cᵒᵖ q (-q)
                        (CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso._proof_1 q)).hom.app
                  (op ((shiftFunctor Cᵒᵖ (-p)).1 (unop X)))) ≫
              (((unopUnop C).map
                      ((shiftFunctorOpIso C (-q) q
                                (CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso._proof_2 q)).inv.app
                          ((shiftFunctor Cᵒᵖ (-p)).1 (unop X))).op ≫
                    (unopUnop C).map
                      ((shiftFunctor C q).map ((shiftFunctorOpIso Cᵒᵖ p (-p) ⋯).inv.app X).unop.unop).op.op) ≫
                  (unopUnop C).map
                    ((shiftFunctorOpIso C (-q) q
                              (CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso._proof_2 q)).hom.app
                        (unop ((shiftFunctor Cᵒᵖᵒᵖ p).obj X))).op) ≫
                (unopUnop C).map
                  ((shiftFunctorOpIso Cᵒᵖ q (-q)
                          (CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso._proof_1 q)).inv.app
                    ((shiftFunctor Cᵒᵖᵒᵖ p).obj X))) ≫
      (((shiftFunctorOpIso Cᵒᵖ q (-q) ⋯).hom.app ((shiftFunctor Cᵒᵖᵒᵖ p).obj X)).unop.unop ≫
          ((shiftFunctorOpIso C (-q) q ⋯).inv.app (unop ((shiftFunctor Cᵒᵖᵒᵖ p).obj X))).unop) ≫
        ((shiftFunctor C q).map ((shiftFunctorOpIso Cᵒᵖ p (-p) ⋯).hom.app X).unop.unop ≫
            (shiftFunctor C q).map ((shiftFunctorOpIso C (-p) p ⋯).inv.app (unop X)).unop) ≫
          (shiftFunctorAdd' C p q (p + q) ⋯).inv.app ((unopUnop C).obj X)