-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
lemma opEquiv'_add_symm (n m a a' a'' : ℤ) (ha' : n + a = a') (ha'' : m + a' = a'')
    (x : (Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦m + n⟧)) :
    (opEquiv' (m + n) a a'' (by omega)).symm x =
      (opEquiv' m a' a'' ha'').symm ((opEquiv' n a a' ha').symm
        (x ≫ (shiftFunctorAdd Cᵒᵖ m n).hom.app _)).op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)
⊢ a + n = a'

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)
⊢ n + m = m + n

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)
⊢ a + n + m = a''

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)
⊢ (opEquiv' (m + n) a a'' ⋯).symm x =
    (opEquiv' m a' a'' ha'').symm
      (Quiver.Hom.op ((opEquiv' n a a' ha').symm (x ≫ (shiftFunctorAdd Cᵒᵖ m n).hom.app (Opposite.op X))))

Tactic:
simp only [opEquiv'_symm_apply, opEquiv_symm_apply,
  opShiftFunctorEquivalence_unitIso_inv_app_eq _ _ _ _ (add_comm n m)]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)
⊢ ((((shiftFunctor C (m + n)).map ((shiftFunctorAdd' Cᵒᵖ m n (m + n) ⋯).hom.app (Opposite.op X)).unop).op ≫
            ((shiftFunctorAdd' C n m (m + n) ⋯).inv.app
                  (Opposite.unop ((shiftFunctor Cᵒᵖ m ⋙ shiftFunctor Cᵒᵖ n).obj (Opposite.op X)))).op ≫
              ((shiftFunctor C m).map
                    ((opShiftFunctorEquivalence C n).unitIso.inv.app
                        ((shiftFunctor Cᵒᵖ m).obj (Opposite.op X))).unop).op ≫
                (opShiftFunctorEquivalence C m).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C (m + n)).map x.unop) ≫
      (shiftFunctorAdd' C a (m + n) a'' ⋯).inv.app Y =
    (((opShiftFunctorEquivalence C m).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C m).map
          ((((opShiftFunctorEquivalence C n).unitIso.inv.app
                      (Opposite.op
                        ((shiftFunctor C
                              ((Discrete.addMonoidalFunctor
                                      (AddMonoidHom.mk' (fun n => -n)
                                        CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1✝)).obj
                                  { as := m }).as).obj
                          X))).unop ≫
                  (shiftFunctor C n).map (x ≫ (shiftFunctorAdd Cᵒᵖ m n).hom.app (Opposite.op X)).unop) ≫
                (shiftFunctorAdd' C a n a' ⋯).inv.app Y).op.unop) ≫
      (shiftFunctorAdd' C a' m a'' ⋯).inv.app Y

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

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)
⊢ ((((shiftFunctor C (m + n)).map ((shiftFunctorAdd' Cᵒᵖ m n (m + n) ⋯).hom.app (Opposite.op X)).unop).op ≫
            ((shiftFunctorAdd' C n m (m + n) ⋯).inv.app
                  (Opposite.unop ((shiftFunctor Cᵒᵖ m ⋙ shiftFunctor Cᵒᵖ n).obj (Opposite.op X)))).op ≫
              ((shiftFunctor C m).map
                    ((opShiftFunctorEquivalence C n).unitIso.inv.app
                        ((shiftFunctor Cᵒᵖ m).obj (Opposite.op X))).unop).op ≫
                (opShiftFunctorEquivalence C m).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C (m + n)).map x.unop) ≫
      (shiftFunctorAdd' C a (m + n) a'' ⋯).inv.app Y =
    (((opShiftFunctorEquivalence C m).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C m).map
          ((((opShiftFunctorEquivalence C n).unitIso.inv.app
                      (Opposite.op
                        ((shiftFunctor C
                              ((Discrete.addMonoidalFunctor
                                      (AddMonoidHom.mk' (fun n => -n)
                                        CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1✝)).obj
                                  { as := m }).as).obj
                          X))).unop ≫
                  (shiftFunctor C n).map (x ≫ (shiftFunctorAdd Cᵒᵖ m n).hom.app (Opposite.op X)).unop) ≫
                (shiftFunctorAdd' C a n a' ⋯).inv.app Y).op.unop) ≫
      (shiftFunctorAdd' C a' m a'' ⋯).inv.app Y

Tactic:
dsimp

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