awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    (↑(t.z i j)⁻¹ : CatCenter C) •
      (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
        Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X
have rw : HSMul.hSMul (β :=
    Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
    (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X) =
  (↑(t.z i j)⁻¹ : CatCenter C) •
    (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
      Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)
⊢ HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X) =
    (↑(t.z i j)⁻¹ : CatCenter C) •
      (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
        Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X
have e_a : NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X =
  (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
    Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X =
    (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
      Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X
have e_a : NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X =
  𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C j) (Functor.obj.{v, v, u, u} (shiftFunctor C i) X)) ≫
    Functor.map (shiftFunctor C j) (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C i) X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ 𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
Tactic: change _ = 𝟙 _ ≫ (shiftFunctor C j).map (𝟙 _) ≫ _ ≫ 𝟙 _
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
x : P.obj (op X)
Y Z : Cᵒᵖ
g : Y ⟶ Z
⊢ Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y ⟶ P.obj Z)
    (Functor.map (Functor.obj shrinkYoneda.{w, v, u} X) g ≫
      ↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Z) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (P.map
                (Quiver.Hom.op
                  ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Z)) :
                      (a : Shrink.{w, v} ((yoneda.obj X).obj Z)) → (yoneda.obj X).obj Z)
                    f))) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Z))))
          x)
    ((↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (P.map
                (Quiver.Hom.op
                  ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Y)) :
                      (a : Shrink.{w, v} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
                    f))) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
          x) ≫
      P.map g)
have h : ∀ (x_1 : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj shrinkYoneda.{w, v, u} X) g ≫
          ↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Z) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (P.map
                    (Quiver.Hom.op
                      ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Z)) :
                          (a : Shrink.{w, v} ((yoneda.obj X).obj Z)) → (yoneda.obj X).obj Z)
                        f))) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Z))))
              x))
      x_1 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (P.map
                    (Quiver.Hom.op
                      ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Y)) :
                          (a : Shrink.{w, v} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
                        f))) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
              x) ≫
          P.map g))
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
t : P.obj X
⊢ Eq.{w + 1} (α := P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop Y))) → shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
              (a : (fun (X : Type w) ↦ X) (P.obj X)) → (fun (X : Type w) ↦ X) (P.obj Y))
            t)) :
      P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        (Functor.map shrinkYoneda.{w, v, u} f.unop ≫
          (Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop X))) → shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) t) :
      P.obj (op (unop Y)))
have obtain : ∀ (t : Functor.obj shrinkYoneda.{w, v, u} (unop X) ⟶ P),
  Eq.{w + 1} (α := P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop Y))) → shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
              (a : (fun (X : Type w) ↦ X) (P.obj X)) → (fun (X : Type w) ↦ X) (P.obj Y))
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t :
              P.obj (op (unop X))))) :
      P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        (Functor.map shrinkYoneda.{w, v, u} f.unop ≫
          (Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop X))) → shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P)
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t)) :
      P.obj (op (unop Y)))
Tactic: obtain ⟨t, rfl⟩ := shrinkYonedaEquiv.surjective t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
t : Functor.obj shrinkYoneda.{w, v, u} (unop X) ⟶ P
⊢ Eq.{w + 1} (α := P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop Y))) → shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
              (a : (fun (X : Type w) ↦ X) (P.obj X)) → (fun (X : Type w) ↦ X) (P.obj Y))
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t :
              P.obj (op (unop X))))) :
      P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        (Functor.map shrinkYoneda.{w, v, u} f.unop ≫
          (Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop X))) → shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P)
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t)) :
      P.obj (op (unop Y)))
have rw : Eq (α := P.obj (op (unop Y)))
  ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
      ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop Y))) → shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
            (a : (fun (X : Type w) ↦ X) (P.obj X)) → (fun (X : Type w) ↦ X) (P.obj Y))
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t :
            P.obj (op (unop X))))) :
    P.obj (op (unop Y)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.unop.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
      ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X)))
          ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop X))) → shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P)
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t)) :
        P.obj (op (unop X))) :
    (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
Tactic: rw [← shrinkYonedaEquiv_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
s : P.obj (op X)
Y : C
f : Y ⟶ X
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op X)) → shrinkYoneda.{w, v, u}.obj X ⟶ P) s)
              (op Y)) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op Y))) →
            (fun (X : Type w) ↦ X) (P.obj (op Y)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op Y) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op Y)) f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op Y)) :
      (fun (X : Type w) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
        s :
      (fun (X : Type w) ↦ X) (P.obj (op Y)))
have obtain : ∀ (g : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P),
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op X)) → shrinkYoneda.{w, v, u}.obj X ⟶ P)
                ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj X ⟶ P) → P.obj (op X)) g))
              (op Y)) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op Y))) →
            (fun (X : Type w) ↦ X) (P.obj (op Y)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op Y) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op Y)) f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op Y)) :
      (fun (X : Type w) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
        ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj X ⟶ P) → P.obj (op X)) g : P.obj (op X)) :
      (fun (X : Type w) ↦ X) (P.obj (op Y)))
Tactic: obtain ⟨g, rfl⟩ := shrinkYonedaEquiv.surjective s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f :
  Quiver.Hom (V := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj shrinkYoneda.{w, v, u} X)
    (Functor.obj shrinkYoneda.{w, v, u} Y)
⊢ Functor.map shrinkYoneda.{w, v, u}
      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → unop (op X) ⟶ Y)
        ((shrinkYonedaEquiv :
            (a : shrinkYoneda.{w, v, u}.obj X ⟶ shrinkYoneda.{w, v, u}.obj Y) →
              (shrinkYoneda.{w, v, u}.obj Y).obj (op X))
          f)) =
    f
have obtain : ∀ (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)),
  Eq (α :=
    Quiver.Hom (V := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj shrinkYoneda.{w, v, u} X)
      (Functor.obj shrinkYoneda.{w, v, u} Y))
    (Functor.map shrinkYoneda.{w, v, u}
        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → unop (op X) ⟶ Y)
          ((shrinkYonedaEquiv :
              (a : shrinkYoneda.{w, v, u}.obj X ⟶ shrinkYoneda.{w, v, u}.obj Y) →
                (shrinkYoneda.{w, v, u}.obj Y).obj (op X))
            ((Equiv.symm shrinkYonedaEquiv :
                (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) →
                  shrinkYoneda.{w, v, u}.obj X ⟶ shrinkYoneda.{w, v, u}.obj Y)
              f))) :
      Quiver.Hom (V := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj shrinkYoneda.{w, v, u} X)
        (Functor.obj shrinkYoneda.{w, v, u} Y))
    ((Equiv.symm shrinkYonedaEquiv :
          (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → shrinkYoneda.{w, v, u}.obj X ⟶ shrinkYoneda.{w, v, u}.obj Y)
        f :
      Quiver.Hom (V := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj shrinkYoneda.{w, v, u} X)
        (Functor.obj shrinkYoneda.{w, v, u} Y))
Tactic: obtain ⟨f, rfl⟩ := shrinkYonedaEquiv.symm.surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
⊢ Eq (α := Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) X_1 ⟶ Functor.obj (Functor.obj yoneda X) Y)
    (Functor.map (Functor.obj shrinkYoneda.{v, v, u} X) f ≫
      Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.toIso shrinkYonedaObjObjEquiv : Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) Y ≅ unop Y ⟶ X))
          Y))
    (Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.toIso shrinkYonedaObjObjEquiv : Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) Y ≅ unop Y ⟶ X))
          X_1) ≫
      Functor.map (Functor.obj yoneda X) f)
have h : ∀ (x : Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) X_1),
  Eq (α := Functor.obj (Functor.obj yoneda X) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj shrinkYoneda.{v, v, u} X) f ≫
          Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso shrinkYonedaObjObjEquiv :
                  Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) Y ≅ unop Y ⟶ X))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso shrinkYonedaObjObjEquiv :
                  Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) Y ≅ unop Y ⟶ X))
              X_1) ≫
          Functor.map (Functor.obj yoneda X) f))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
      (Functor.obj yoneda Y))
    (Functor.map shrinkYoneda.{v, v, u} f ≫
      Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯ :
              Iso (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
                (Functor.obj yoneda X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯ :
              Iso (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
                (Functor.obj yoneda X)))
          X) ≫
      Functor.map yoneda f)
have w : ∀ (x : Cᵒᵖ) (x_1 : Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) x),
  Eq (α := Functor.obj (Functor.obj yoneda Y) x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map shrinkYoneda.{v, v, u} f ≫
            Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) sorry :
                    Iso (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
                      (Functor.obj yoneda X)))
                Y))
          x))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) sorry :
                    Iso (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
                      (Functor.obj yoneda X)))
                X) ≫
            Functor.map yoneda f)
          x))
      x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : LocallySmall.{max w w', v, u} C
X Y : C
x : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := Cᵒᵖ ⥤ Type (max w w'))
      (Functor.obj
        (shrinkYoneda.{w, v, u} ⋙
          Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))) uliftFunctor.{w', w})
        X)
      (Functor.obj shrinkYoneda.{max w w', v, u} Y))
    (Functor.map
        (shrinkYoneda.{w, v, u} ⋙
          Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))) uliftFunctor.{w', w})
        x ≫
      Iso.hom
        ((fun (X : C) ↦
            (FunctorToTypes.shrinkCompUliftFunctorIso (Functor.obj yoneda X) :
              Iso (C := Cᵒᵖ ⥤ Type (max w w'))
                (FunctorToTypes.shrink.{w, v, v, u} (Functor.obj yoneda X) ⋙ uliftFunctor.{w', w})
                (FunctorToTypes.shrink.{max w w', v, v, u} (Functor.obj yoneda X))))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (FunctorToTypes.shrinkCompUliftFunctorIso (Functor.obj yoneda X) :
              Iso (C := Cᵒᵖ ⥤ Type (max w w'))
                (FunctorToTypes.shrink.{w, v, v, u} (Functor.obj yoneda X) ⋙ uliftFunctor.{w', w})
                (FunctorToTypes.shrink.{max w w', v, v, u} (Functor.obj yoneda X))))
          X) ≫
      Functor.map shrinkYoneda.{max w w', v, u} x)
have w : ∀ (x_1 : Cᵒᵖ)
  (x_2 :
    Functor.obj
      (Functor.obj
        (shrinkYoneda.{w, v, u} ⋙
          Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))) uliftFunctor.{w', w})
        X)
      x_1),
  Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w w', v, u} Y) x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map
              (shrinkYoneda.{w, v, u} ⋙
                Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))) uliftFunctor.{w', w})
              x ≫
            Iso.hom
              ((fun (X : C) ↦
                  (FunctorToTypes.shrinkCompUliftFunctorIso (Functor.obj yoneda X) :
                    Iso (C := Cᵒᵖ ⥤ Type (max w w'))
                      (FunctorToTypes.shrink.{w, v, v, u} (Functor.obj yoneda X) ⋙ uliftFunctor.{w', w})
                      (FunctorToTypes.shrink.{max w w', v, v, u} (Functor.obj yoneda X))))
                Y))
          x_1))
      x_2)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : C) ↦
                  (FunctorToTypes.shrinkCompUliftFunctorIso (Functor.obj yoneda X) :
                    Iso (C := Cᵒᵖ ⥤ Type (max w w'))
                      (FunctorToTypes.shrink.{w, v, v, u} (Functor.obj yoneda X) ⋙ uliftFunctor.{w', w})
                      (FunctorToTypes.shrink.{max w w', v, v, u} (Functor.obj yoneda X))))
                X) ≫
            Functor.map shrinkYoneda.{max w w', v, u} x)
          x_1))
      x_2)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
⊢ Eq (α :=
    Functor.obj (Functor.obj uliftYoneda.{w', v, u} X) X_1 ⟶
      Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y)
    (Functor.map (Functor.obj uliftYoneda.{w', v, u} X) f ≫
      Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
              ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
          Y))
    (Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
              ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
          X_1) ≫
      Functor.map (Functor.obj shrinkYoneda.{max w' v, v, u} X) f)
have h : ∀ (x : Functor.obj (Functor.obj uliftYoneda.{w', v, u} X) X_1),
  Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj uliftYoneda.{w', v, u} X) f ≫
          Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
                  ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
                  ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
              X_1) ≫
          Functor.map (Functor.obj shrinkYoneda.{max w' v, v, u} X) f))
      x)
Tactic: ext