awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 :
  CommShift (C := OppositeShift.{v_1, u_1, u_3} C A) (D := OppositeShift.{v_2, u_2, u_3} D A)
    (OppositeShift.functor A F) A
x : C
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))
    (Quiver.Hom.unop
          (map (OppositeShift.functor A F)
            (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (Opposite.unop (Opposite.op x))))) ≫
        Quiver.Hom.unop
          (Quiver.Hom.op
            (NatTrans.app (Iso.inv (shiftFunctorZero D A))
              (Opposite.unop
                (obj
                  (OppositeShift.functor A F :
                    Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                      (OppositeShift.{v_2, u_2, u_3} D A))
                  (Opposite.op x))))) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) x) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj x) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 :
  CommShift (C := OppositeShift.{v_1, u_1, u_3} C A) (D := OppositeShift.{v_2, u_2, u_3} D A)
    (OppositeShift.functor A F) A
a b : A
rw :
  Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b))
    (NatIso.removeOp
      (Iso.symm
        (CommShift.isoAdd (commShiftIso (OppositeShift.functor A F) a) (commShiftIso (OppositeShift.functor A F) b))))
    (CommShift.isoAdd (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) a)))
      (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) b))))
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b))
    (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) (a + b))))
    (CommShift.isoAdd (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) a)))
      (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) b))))

Tactic:
rw [commShiftIso_add]

Premises used: CategoryTheory.Functor.CommShift.commShiftIso_add
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 :
  CommShift (C := OppositeShift.{v_1, u_1, u_3} C A) (D := OppositeShift.{v_2, u_2, u_3} D A)
    (OppositeShift.functor A F) A
a b : A
w :
  ∀ (x : C),
    Eq.{v_2 + 1} (α := (shiftFunctor C (a + b) ⋙ F).obj x ⟶ (F ⋙ shiftFunctor D (a + b)).obj x)
      (NatTrans.app
        (Iso.hom
          (NatIso.removeOp
            (Iso.symm
              (CommShift.isoAdd (commShiftIso (OppositeShift.functor A F) a)
                (commShiftIso (OppositeShift.functor A F) b)))))
        x)
      (NatTrans.app
        (Iso.hom
          (CommShift.isoAdd (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) a)))
            (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) b)))))
        x)
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b))
    (NatIso.removeOp
      (Iso.symm
        (CommShift.isoAdd (commShiftIso (OppositeShift.functor A F) a) (commShiftIso (OppositeShift.functor A F) b))))
    (CommShift.isoAdd (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) a)))
      (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) b))))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F G : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
inst_6 : G.CommShift A
τ : F ⟶ G
inst_7 : CommShift τ A
x : A
w :
  ∀ (x_1 : OppositeShift.{v_1, u_1, u_3} C A),
    Eq (α :=
      Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
        (Functor.obj (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ OppositeShift.functor A G) x_1)
        (Functor.obj (OppositeShift.functor A F ⋙ shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x) x_1))
      (app
        (Iso.hom (Functor.commShiftIso (OppositeShift.functor A G) x) ≫
          Functor.whiskerRight (OppositeShift.natTrans A τ) (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x))
        x_1)
      (app
        (Functor.whiskerLeft (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) (OppositeShift.natTrans A τ) ≫
          Iso.hom (Functor.commShiftIso (OppositeShift.functor A F) x))
        x_1)
⊢ Eq (α :=
    Quiver.Hom (V :=
      Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
      (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ OppositeShift.functor A G)
      (OppositeShift.functor A F ⋙ shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x))
    (Iso.hom (Functor.commShiftIso (OppositeShift.functor A G) x) ≫
      Functor.whiskerRight (OppositeShift.natTrans A τ) (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x))
    (Functor.whiskerLeft (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) (OppositeShift.natTrans A τ) ≫
      Iso.hom (Functor.commShiftIso (OppositeShift.functor A F) x))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F G : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
inst_6 : G.CommShift A
τ : F ⟶ G
inst_7 : CommShift τ A
x : A
x_1 : OppositeShift.{v_1, u_1, u_3} C A
w :
  Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
      (Functor.obj (OppositeShift.functor A G ⋙ shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x) x_1)
      (Functor.obj (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ OppositeShift.functor A F) x_1))
    (CategoryStruct.comp (Y :=
      Functor.obj (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ OppositeShift.functor A G) x_1)
      (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A G) x)) x_1)
      (CategoryStruct.comp (Y :=
        Functor.obj (OppositeShift.functor A F ⋙ shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x) x_1)
        (app
          (Iso.hom (Functor.commShiftIso (OppositeShift.functor A G) x) ≫
            Functor.whiskerRight (OppositeShift.natTrans A τ) (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x))
          x_1)
        (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A F) x)) x_1)))
    (CategoryStruct.comp (Y :=
      Functor.obj (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ OppositeShift.functor A G) x_1)
      (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A G) x)) x_1)
      (CategoryStruct.comp (Y :=
        Functor.obj (OppositeShift.functor A F ⋙ shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x) x_1)
        (app
          (Functor.whiskerLeft (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) (OppositeShift.natTrans A τ) ≫
            Iso.hom (Functor.commShiftIso (OppositeShift.functor A F) x))
          x_1)
        (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A F) x)) x_1)))
⊢ Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
      (Functor.obj (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ OppositeShift.functor A G) x_1)
      (Functor.obj (OppositeShift.functor A F ⋙ shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x) x_1))
    (app
      (Iso.hom (Functor.commShiftIso (OppositeShift.functor A G) x) ≫
        Functor.whiskerRight (OppositeShift.natTrans A τ) (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x))
      x_1)
    (app
      (Functor.whiskerLeft (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) (OppositeShift.natTrans A τ) ≫
        Iso.hom (Functor.commShiftIso (OppositeShift.functor A F) x))
      x_1)

Tactic:
rw [← cancel_mono (((OppositeShift.functor A F).commShiftIso _).inv.app _),
      ← cancel_epi (((OppositeShift.functor A G).commShiftIso _).inv.app _)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.OppositeShift.functor, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F G : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
inst_6 : G.CommShift A
τ : F ⟶ G
inst_7 : CommShift τ A
x : A
x_1 : OppositeShift.{v_1, u_1, u_3} C A
⊢ Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
      (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x)
        (Functor.obj (OppositeShift.functor A G) x_1))
      (Functor.obj (OppositeShift.functor A F)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1)))
    (Functor.map (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x) (app (OppositeShift.natTrans A τ) x_1) ≫
      app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A F) x)) x_1)
    (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A G) x)) x_1 ≫
      app (OppositeShift.natTrans A τ)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))

Tactic:
(op_inj_iff _ _).mpr (NatTrans.shift_app_comm τ _ (unop _))

Premises used: Iff.mpr, Quiver.Hom.op, CategoryTheory.NatTrans.shift_app_comm, Opposite.unop, Opposite.op_inj_iff
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F G : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
inst_6 : G.CommShift A
τ : F ⟶ G
inst_7 : CommShift τ A
x : A
x_1 : OppositeShift.{v_1, u_1, u_3} C A
⊢ Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
      (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x)
        (Functor.obj (OppositeShift.functor A G) x_1))
      (Functor.obj (OppositeShift.functor A F)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1)))
    (Functor.map (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) x) (app (OppositeShift.natTrans A τ) x_1) ≫
      app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A F) x)) x_1)
    (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A G) x)) x_1 ≫
      app (OppositeShift.natTrans A τ)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))

Tactic:
exact (op_inj_iff _ _).mpr (NatTrans.shift_app_comm τ _ (unop _))

Premises used: Iff.mpr, CategoryTheory.NatTrans.shift_app_comm, Opposite.unop, Opposite.op_inj_iff
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
x : A
w :
  ∀ (x_1 : OppositeShift.{v_1, u_1, u_3} C A),
    Eq (α :=
      Functor.obj.{v_1, v_1, u_1, u_1}
          (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ 𝟭 (OppositeShift.{v_1, u_1, u_3} C A)) x_1 ⟶
        Functor.obj (OppositeShift.functor A (𝟭 C) ⋙ shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1)
      (app
        (Iso.hom (Functor.commShiftIso (𝟭 (OppositeShift.{v_1, u_1, u_3} C A)) x) ≫
          Functor.whiskerRight (Iso.hom (OppositeShift.natIsoId C A))
            (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x))
        x_1)
      (app
        (Functor.whiskerLeft (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x)
            (Iso.hom (OppositeShift.natIsoId C A)) ≫
          Iso.hom (Functor.commShiftIso (OppositeShift.functor A (𝟭 C)) x))
        x_1)
⊢ Eq (α :=
    Quiver.Hom (V :=
      Functor.{v_1, v_1, u_1, u_1} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_1, u_1, u_3} C A))
      (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ 𝟭 (OppositeShift.{v_1, u_1, u_3} C A))
      (OppositeShift.functor A (𝟭 C) ⋙ shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x))
    (Iso.hom (Functor.commShiftIso (𝟭 (OppositeShift.{v_1, u_1, u_3} C A)) x) ≫
      Functor.whiskerRight (Iso.hom (OppositeShift.natIsoId C A)) (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x))
    (Functor.whiskerLeft (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) (Iso.hom (OppositeShift.natIsoId C A)) ≫
      Iso.hom (Functor.commShiftIso (OppositeShift.functor A (𝟭 C)) x))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
x : A
x_1 : OppositeShift.{v_1, u_1, u_3} C A
w :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1 ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x)
        (Functor.obj (OppositeShift.functor A (𝟭 C)) x_1))
    (app (Iso.hom (Functor.commShiftIso (𝟭 (OppositeShift.{v_1, u_1, u_3} C A)) x)) x_1 ≫
        Functor.map (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) (𝟙 x_1) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1 ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x)
          (Functor.obj (OppositeShift.functor A (𝟭 C)) x_1))
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1) ≫
        Quiver.Hom.op (app (Iso.inv (Functor.commShiftIso (𝟭 C) x)) (Opposite.unop x_1)) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1 ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x)
          (Functor.obj (OppositeShift.functor A (𝟭 C)) x_1))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ 𝟭 (OppositeShift.{v_1, u_1, u_3} C A)) x_1 ⟶
      Functor.obj (OppositeShift.functor A (𝟭 C) ⋙ shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1)
    (app
      (Iso.hom (Functor.commShiftIso (𝟭 (OppositeShift.{v_1, u_1, u_3} C A)) x) ≫
        Functor.whiskerRight (Iso.hom (OppositeShift.natIsoId C A))
          (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x))
      x_1)
    (app
      (Functor.whiskerLeft (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) (Iso.hom (OppositeShift.natIsoId C A)) ≫
        Iso.hom (Functor.commShiftIso (OppositeShift.functor A (𝟭 C)) x))
      x_1)

Tactic:
dsimp [OppositeShift.natIsoId, Functor.commShiftOp_iso_eq]

Premises used: CategoryTheory.Functor.commShiftOp_iso_eq, CategoryTheory.NatTrans.OppositeShift.natIsoId
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
x : A
x_1 : OppositeShift.{v_1, u_1, u_3} C A
w :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1) =
    𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C x) (Opposite.unop x_1)))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1 ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x)
        (Functor.obj (OppositeShift.functor A (𝟭 C)) x_1))
    (app (Iso.hom (Functor.commShiftIso (𝟭 (OppositeShift.{v_1, u_1, u_3} C A)) x)) x_1 ≫
        Functor.map (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) (𝟙 x_1) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1 ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x)
          (Functor.obj (OppositeShift.functor A (𝟭 C)) x_1))
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1) ≫
        Quiver.Hom.op (app (Iso.inv (Functor.commShiftIso (𝟭 C) x)) (Opposite.unop x_1)) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1 ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x)
          (Functor.obj (OppositeShift.functor A (𝟭 C)) x_1))

Tactic:
simp only [Functor.commShiftIso_id_hom_app, Functor.map_id,
      comp_id, Functor.commShiftIso_id_inv_app, CategoryTheory.op_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.commShiftIso_id_hom_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.commShiftIso_id_inv_app, CategoryTheory.Category.id_comp, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
x : A
x_1 : OppositeShift.{v_1, u_1, u_3} C A
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1) =
    𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C x) (Opposite.unop x_1)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
E : Type u_4
inst_5 : Category.{v_3, u_4} E
inst_6 : HasShift.{v_3, u_4, u_3} E A
G : Functor.{v_2, v_3, u_2, u_4} D E
inst_7 : F.CommShift A
inst_8 : G.CommShift A
x : A
w :
  ∀ (x_1 : OppositeShift.{v_1, u_1, u_3} C A),
    Eq (α :=
      Quiver.Hom (V := OppositeShift.{v_3, u_4, u_3} E A)
        (Functor.obj (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ OppositeShift.functor A (F ⋙ G)) x_1)
        (Functor.obj
          (Functor.comp (D := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A F)
              (OppositeShift.functor A G) ⋙
            shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x)
          x_1))
      (app
        (Iso.hom (Functor.commShiftIso (OppositeShift.functor A (F ⋙ G)) x) ≫
          Functor.whiskerRight (Iso.hom (OppositeShift.natIsoComp A F G))
            (shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x))
        x_1)
      (app
        (Functor.whiskerLeft (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x)
            (Iso.hom (OppositeShift.natIsoComp A F G)) ≫
          Iso.hom
            (Functor.commShiftIso
              (Functor.comp (D := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A F)
                (OppositeShift.functor A G))
              x))
        x_1)
⊢ Eq (α :=
    Quiver.Hom (V :=
      Functor.{v_1, v_3, u_1, u_4} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_3, u_4, u_3} E A))
      (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ OppositeShift.functor A (F ⋙ G))
      (Functor.comp (D := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A F) (OppositeShift.functor A G) ⋙
        shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x))
    (Iso.hom (Functor.commShiftIso (OppositeShift.functor A (F ⋙ G)) x) ≫
      Functor.whiskerRight (Iso.hom (OppositeShift.natIsoComp A F G))
        (shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x))
    (Functor.whiskerLeft (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x)
        (Iso.hom (OppositeShift.natIsoComp A F G)) ≫
      Iso.hom
        (Functor.commShiftIso
          (Functor.comp (D := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A F)
            (OppositeShift.functor A G))
          x))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
E : Type u_4
inst_5 : Category.{v_3, u_4} E
inst_6 : HasShift.{v_3, u_4, u_3} E A
G : Functor.{v_2, v_3, u_2, u_4} D E
inst_7 : F.CommShift A
inst_8 : G.CommShift A
x : A
x_1 : OppositeShift.{v_1, u_1, u_3} C A
⊢ Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_3, u_4, u_3} E A)
      (Functor.obj (OppositeShift.functor A (F ⋙ G))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))
      (Functor.obj.{v_3, v_3, u_4, u_4} (shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x)
        (Functor.obj (C := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A G)
          (Functor.obj (OppositeShift.functor A F) x_1))))
    (Quiver.Hom.op (app (Iso.inv (Functor.commShiftIso (F ⋙ G) x)) (Opposite.unop x_1)))
    (app
      (Iso.hom
        (Functor.commShiftIso
          (Functor.comp (D := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A F)
            (OppositeShift.functor A G))
          x))
      x_1)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F_1 F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
x : OppositeShift.{v_2, u_2, u_3} D A
dsimp :
  Eq.{v_1 + 1} (α := Opposite.op (G.obj (Opposite.unop x)) ⟶ Opposite.op (G.obj (Opposite.unop x)))
    ((G.map
          (𝟙 x ≫
              Quiver.Hom.op (adj.counit.app (Opposite.unop x)) ≫
                𝟙 (Opposite.op (F.obj (G.obj (Opposite.unop x))))).unop).op ≫
      𝟙 (Opposite.op (G.obj (F.obj (G.obj (Opposite.unop x))))) ≫
        Quiver.Hom.op (adj.unit.app (G.obj (Opposite.unop x))) ≫ 𝟙 (Opposite.op (G.obj (Opposite.unop x))))
    (𝟙 (Opposite.op (G.obj (Opposite.unop x))))
⊢ Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_1, u_1, u_3} C A) (Functor.obj (functor A G) x) (Functor.obj (functor A G) x))
    (Functor.map (functor A G)
        (NatTrans.app
          (Iso.hom (NatTrans.OppositeShift.natIsoId D A) ≫
            natTrans A adj.counit ≫ Iso.hom (NatTrans.OppositeShift.natIsoComp A G F))
          x) ≫
      NatTrans.app
        (Iso.inv (NatTrans.OppositeShift.natIsoComp A F G) ≫
          natTrans A adj.unit ≫ Iso.inv (NatTrans.OppositeShift.natIsoId C A))
        (Functor.obj (functor A G) x))
    (𝟙 (Functor.obj (functor A G) x))

Tactic:
dsimp [OppositeShift.natTrans, NatTrans.OppositeShift.natIsoComp,
      NatTrans.OppositeShift.natIsoId, OppositeShift.functor]

Premises used: CategoryTheory.OppositeShift.natTrans, CategoryTheory.NatTrans.OppositeShift.natIsoComp, CategoryTheory.OppositeShift.functor, CategoryTheory.NatTrans.OppositeShift.natIsoId