-- 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 ≫
        (shiftFunctor C b).map ((shiftFunctor C a).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
          (shiftFunctor C b).map ((shiftFunctor C a).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

Tactic:
rw [← Functor.map_comp_assoc, ← Functor.map_comp_assoc,
  ← Functor.map_comp_assoc]

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).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
            (shiftFunctor C a).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 ≫
            ((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
⊢ ((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

Tactic:
dsimp

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

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 ≫
              (shiftFunctor C a).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
            (shiftFunctor C a).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
          (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y) ≫ g).unop ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
erw [← NatTrans.naturality]

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).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
            (shiftFunctor C a).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
          (((shiftFunctor Cᵒᵖ a ⋙ (shiftFunctor C a).op).map g ≫
                (opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z