-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
lemma opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift
    {n m : ℤ} (f : ShiftedHom X Y n) (g : ShiftedHom Y Z m)
    (q : ℤ) (hq : n + m = q) :
    (opEquiv' n m q hq).symm
        (g.op ≫ (opShiftFunctorEquivalence C n).counitIso.inv.app _ ≫ f.op⟦n⟧') =
      f.comp g (by omega)

Proof state:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ ((((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
          (shiftFunctor C n).map
            ((((shiftFunctor Cᵒᵖ n).map (Quiver.Hom.op f)).unop ≫
                ((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y)).unop) ≫
              g)) ≫
        (shiftFunctorAdd' C m n q ⋯).inv.app Z).op =
    (f ≫ (shiftFunctor C n).map g ≫ (shiftFunctorAdd' C m n q ⋯).inv.app Z).op

Tactic:
simp only [assoc, Functor.map_comp, op_comp, Quiver.Hom.op_unop,
  opShiftFunctorEquivalence_unitIso_inv_naturality]

Result:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ ((shiftFunctorAdd' C m n q ⋯).inv.app Z).op ≫
      ((shiftFunctor C n).map g).op ≫
        ((shiftFunctor C n).map ((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y)).unop).op ≫
          (opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op ((shiftFunctor C n).obj Y)) ≫ Quiver.Hom.op f =
    ((shiftFunctorAdd' C m n q ⋯).inv.app Z).op ≫ ((shiftFunctor C n).map g).op ≫ Quiver.Hom.op f

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.56589, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ m + n = q

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
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ (opEquiv' n m q hq).symm
      (Quiver.Hom.op g ≫
        (opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y) ≫
          (shiftFunctor Cᵒᵖ n).map (Quiver.Hom.op f)) =
    f.comp g ⋯

Tactic:
rw [opEquiv'_symm_apply, opEquiv_symm_apply]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ (((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C n).map
          (Quiver.Hom.op g ≫
              (opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y) ≫
                (shiftFunctor Cᵒᵖ n).map (Quiver.Hom.op f)).unop) ≫
      (shiftFunctorAdd' C m n q ⋯).inv.app Z =
    f.comp g ⋯

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ (((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C n).map
          (Quiver.Hom.op g ≫
              (opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y) ≫
                (shiftFunctor Cᵒᵖ n).map (Quiver.Hom.op f)).unop) ≫
      (shiftFunctorAdd' C m n q ⋯).inv.app Z =
    f.comp g ⋯

Tactic:
dsimp [comp]

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

Proof state:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ ((shiftFunctorAdd' C m n q ⋯).inv.app Z).op ≫
      ((shiftFunctor C n).map g).op ≫
        ((shiftFunctor C n).map ((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y)).unop).op ≫
          (opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op ((shiftFunctor C n).obj Y)) ≫ Quiver.Hom.op f =
    ((shiftFunctorAdd' C m n q ⋯).inv.app Z).op ≫ ((shiftFunctor C n).map g).op ≫ Quiver.Hom.op f

Tactic:
erw [(opShiftFunctorEquivalence C n).inverse_counitInv_comp_assoc (Opposite.op Y)]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ (((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C n).map
          ((((shiftFunctor Cᵒᵖ n).map (Quiver.Hom.op f)).unop ≫
              ((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y)).unop) ≫
            g)) ≫
      (shiftFunctorAdd' C m n q ⋯).inv.app Z =
    f ≫ (shiftFunctor C n).map g ≫ (shiftFunctorAdd' C m n q ⋯).inv.app Z

Tactic:
apply Quiver.Hom.op_inj

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