-- 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.76339, u_1} C
inst✝ : HasShift C ℤ
X Y Z : 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)
⊢ m + n + a = 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)
⊢ ((((((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

Tactic:
simp only [assoc, Functor.map_comp, ← shiftFunctorAdd'_eq_shiftFunctorAdd,
  ← NatTrans.naturality_assoc,
  shiftFunctorAdd'_assoc_inv_app a n m a' (m + n) a'' (by omega) (by omega) (by omega)]

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 ≫
        (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