awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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))
    (CategoryStruct.comp (Y :=
        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)))
        (Quiver.Hom.unop
          (map (OppositeShift.functor A F) (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ A)) (Opposite.op x))))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.hom (shiftFunctorZero Dᵒᵖ A))
            (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))
have w : 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: erw [oppositeShiftFunctorZero_hom_app, oppositeShiftFunctorZero_inv_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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
⊢ 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))))
have 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))))
Tactic: rw [commShiftIso_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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
⊢ 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))))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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 (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)
have 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)))
Tactic: rw [← cancel_mono (((OppositeShift.functor A F).commShiftIso _).inv.app _),
      ← cancel_epi (((OppositeShift.functor A G).commShiftIso _).inv.app _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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)))
    (CategoryStruct.comp (Y :=
      Functor.obj (OppositeShift.functor A G)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))
      (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A G) x)) x_1)
      (CategoryStruct.comp (Y :=
        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 F) x_1))
        (app (Iso.hom (Functor.commShiftIso (OppositeShift.functor A G) 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)))
    (CategoryStruct.comp (Y :=
      Functor.obj (OppositeShift.functor A G)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))
      (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A G) x)) x_1)
      (CategoryStruct.comp (Y :=
        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 F) 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) ≫
          app (Iso.hom (Functor.commShiftIso (OppositeShift.functor A F) x)) x_1)
        (app (Iso.inv (Functor.commShiftIso (OppositeShift.functor A F) x)) x_1)))
have w : 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: simp only [assoc, Iso.inv_hom_id_app_assoc, Iso.hom_inv_id_app, Functor.comp_obj,
      comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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
⊢ 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)
have 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))
Tactic: dsimp [OppositeShift.natIsoId, Functor.commShiftOp_iso_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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
⊢ 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))
have 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)))
Tactic: simp only [Functor.commShiftIso_id_hom_app, Functor.map_id,
      comp_id, Functor.commShiftIso_id_inv_app, CategoryTheory.op_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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
⊢ 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))
have 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))))
Tactic: dsimp [OppositeShift.natTrans, NatTrans.OppositeShift.natIsoComp,
      NatTrans.OppositeShift.natIsoId, OppositeShift.functor]