-- Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean
lemma opShiftFunctorEquivalence_unitIso_hom_app_eq (X : Cᵒᵖ) (m n p : ℤ) (h : m + n = p) :
    (opShiftFunctorEquivalence C p).unitIso.hom.app X =
      (opShiftFunctorEquivalence C n).unitIso.hom.app X ≫
      (((opShiftFunctorEquivalence C m).unitIso.hom.app (X⟦n⟧)).unop⟦n⟧').op ≫
      ((shiftFunctorAdd' C m n p h).hom.app _).op ≫
      (((shiftFunctorAdd' Cᵒᵖ n m p (by omega)).inv.app X).unop⟦p⟧').op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C p).map ((shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop).op ≫
        ((shiftFunctor C n).map
              ((shiftFunctor C m).map ((shiftFunctorOpIso C m (-m) ⋯).inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    ((shiftFunctor C (-m)).map ((shiftFunctorOpIso C n (-n) ⋯).hom.app X).unop).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op

Tactic:
erw [Functor.map_id, Functor.map_id, Functor.map_id, Functor.map_id,
  id_comp, id_comp, id_comp, comp_id, comp_id]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map
              ((𝟙 ((shiftFunctor C (-m)).obj (Opposite.unop ((shiftFunctor C (-n)).op.obj X)))).op ≫
                  ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op).unop).op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
          ((shiftFunctor C n).map
              ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app ((shiftFunctor C (-n)).obj (Opposite.unop X)))).op) ≫
        ((shiftFunctorAdd' C m n p h).hom.app
            ((shiftFunctor C (-m)).obj ((shiftFunctor C (-n)).obj (Opposite.unop X)))).op) ≫
      ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op

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

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app ((shiftFunctor C (-n)).obj (Opposite.unop X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              ((shiftFunctor C (-m)).obj ((shiftFunctor C (-n)).obj (Opposite.unop X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ (opShiftFunctorEquivalence C p).unitIso.hom.app X =
    (opShiftFunctorEquivalence C n).unitIso.hom.app X ≫
      ((shiftFunctor C n).map ((opShiftFunctorEquivalence C m).unitIso.hom.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((opShiftFunctorEquivalence C m).functor.obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op

Tactic:
dsimp [opShiftFunctorEquivalence]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C p).map ((shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op =
    (((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
        ((shiftFunctor C n).map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop).op) ≫
      ((shiftFunctor C n).map
            ((shiftFunctor C m).map ((shiftFunctorOpIso C m (-m) ⋯).inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop ≫
              (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ n + m = p

Tactic:
omega

Result:
no goals