-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
lemma opEquiv_symm_comp {a b : ℤ}
    (f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a)
    (g : ShiftedHom (Opposite.op Y) (Opposite.op X) b)
    {c : ℤ} (h : b + a = c) :
    (opEquiv _).symm (f.comp g h) =
      ((opEquiv _).symm g).comp ((opEquiv _).symm f) (by omega)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app
            (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X)))) ≫
          (shiftFunctor C c).map
            (𝟙 (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X)))) ≫
              ((shiftFunctor Cᵒᵖ a).map g).unop ≫ Quiver.Hom.unop f) =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
rw [assoc, id_comp, Functor.map_comp, ← NatTrans.naturality_assoc,
  ← NatTrans.naturality, opEquiv_symm_apply]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map ((shiftFunctor Cᵒᵖ a).map g).unop ≫
          (shiftFunctor C a ⋙ shiftFunctor C b).map (Quiver.Hom.unop f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map (Quiver.Hom.unop g) ≫
        (shiftFunctor C b).map
            (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
              (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
          (shiftFunctorAdd' C a b c ⋯).inv.app Z

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ a + b = c

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (((((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
            (shiftFunctor C b).map
              ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop) ≫
          (shiftFunctorAdd' C a b c ⋯).inv.app
            (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))))) ≫
        (shiftFunctor C c).map ((shiftFunctorAdd' Cᵒᵖ b a c ⋯).hom.app (Opposite.op X)).unop) ≫
      (shiftFunctor C c).map
        ((((shiftFunctorAdd' Cᵒᵖ b a c h).inv.app (Opposite.op X)).unop ≫ ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
          Quiver.Hom.unop f) =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
rw [assoc, assoc, assoc, assoc, ← Functor.map_comp, ← unop_comp_assoc,
  Iso.inv_hom_id_app]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app
            (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X)))) ≫
          (shiftFunctor C c).map
            ((𝟙 ((shiftFunctor Cᵒᵖ b ⋙ shiftFunctor Cᵒᵖ a).obj (Opposite.op X))).unop ≫
              ((shiftFunctor Cᵒᵖ a).map g).unop ≫ Quiver.Hom.unop f) =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (opEquiv c).symm (f.comp g h) = ((opEquiv b).symm g).comp ((opEquiv a).symm f) ⋯

Tactic:
rw [opEquiv_symm_apply, opEquiv_symm_apply,
  opShiftFunctorEquivalence_unitIso_inv_app_eq _ _ _ _ (show a + b = c by omega), comp, comp]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (((shiftFunctor C c).map ((shiftFunctorAdd' Cᵒᵖ b a c ⋯).hom.app (Opposite.op X)).unop).op ≫
          ((shiftFunctorAdd' C a b c ⋯).inv.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ b ⋙ shiftFunctor Cᵒᵖ a).obj (Opposite.op X)))).op ≫
            ((shiftFunctor C b).map
                  ((opShiftFunctorEquivalence C a).unitIso.inv.app
                      ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop).op ≫
              (opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C c).map
        (f ≫ (shiftFunctor Cᵒᵖ a).map g ≫ (shiftFunctorAdd' Cᵒᵖ b a c h).inv.app (Opposite.op X)).unop =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z