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

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.inv.app X =
    ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
      ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
        ((shiftFunctor C n).map
              ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
          (opShiftFunctorEquivalence C n).unitIso.inv.app X

Tactic:
rw [← cancel_mono ((opShiftFunctorEquivalence C p).unitIso.hom.app X), Iso.inv_hom_id_app,
  opShiftFunctorEquivalence_unitIso_hom_app_eq _ _ _ _ h,
  Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id_app_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
⊢ 𝟙 (((opShiftFunctorEquivalence C p).functor ⋙ (opShiftFunctorEquivalence C p).inverse).obj X) =
    ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
      ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
        ((shiftFunctor C n).map
              ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
          ((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

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

Tactic:
simp only [Category.assoc, ← Functor.map_comp_assoc, Iso.hom_inv_id_app_assoc,
  ← unop_comp, Iso.inv_hom_id_app, Functor.comp_obj, Functor.op_obj, unop_id,
  Functor.map_id, id_comp, ← Functor.map_comp, Iso.hom_inv_id_app]

Result:
no goals

Proof state:
case a
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).functor ⋙ (opShiftFunctorEquivalence C p).inverse).obj X)).unop =
    (((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
        ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
          ((shiftFunctor C n).map
                ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
            ((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).unop

Tactic:
dsimp

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

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

Tactic:
omega

Result:
no goals

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).functor ⋙ (opShiftFunctorEquivalence C p).inverse).obj X) =
    ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
      ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
        ((shiftFunctor C n).map
              ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
          ((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:
apply Quiver.Hom.unop_inj

Result:
case a
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).functor ⋙ (opShiftFunctorEquivalence C p).inverse).obj X)).unop =
    (((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
        ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
          ((shiftFunctor C n).map
                ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
            ((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).unop