awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
X_1 : C
e e' : F.CorepresentableBy X_1
h :
  Eq.{v + 1} (α := F.obj X_1)
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X_1) (F.obj X_1)) : (a : X_1 ⟶ X_1) → F.obj X_1) (𝟙 X_1) : F.obj X_1)
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X_1) (F.obj X_1)) : (a : X_1 ⟶ X_1) → F.obj X_1) (𝟙 X_1) : F.obj X_1)
X : C
f : X_1 ⟶ X
rw :
  Eq (α := F.obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj X_1)) → (fun (X : Type v) ↦ X) (F.obj X))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X_1) (F.obj X_1)) : (a : X_1 ⟶ X_1) → F.obj X_1) (𝟙 X_1) :
          F.obj X_1) :
      (fun (X : Type v) ↦ X) (F.obj X))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X) (F.obj X)) : (a : X_1 ⟶ X) → F.obj X) f : F.obj X)
rw₁ :
  Eq (α := F.obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj X_1)) → (fun (X : Type v) ↦ X) (F.obj X))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X_1) (F.obj X_1)) : (a : X_1 ⟶ X_1) → F.obj X_1) (𝟙 X_1) :
          F.obj X_1) :
      (fun (X : Type v) ↦ X) (F.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj X_1)) → (fun (X : Type v) ↦ X) (F.obj X))
        (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X_1) (F.obj X_1)) : (a : X_1 ⟶ X_1) → F.obj X_1) (𝟙 X_1) :
          F.obj X_1) :
      (fun (X : Type v) ↦ X) (F.obj X))
⊢ Eq.{v + 1} (α := F.obj X)
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X) (F.obj X)) : (a : X_1 ⟶ X) → F.obj X) f : F.obj X)
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X) (F.obj X)) : (a : X_1 ⟶ X) → F.obj X) f : F.obj X)
have rw₂ : Eq (α := F.obj X)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type v) ↦ X) (F.obj X_1)) → (fun (X : Type v) ↦ X) (F.obj X))
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X_1) (F.obj X_1)) : (a : X_1 ⟶ X_1) → F.obj X_1) (𝟙 X_1) :
        F.obj X_1) :
    (fun (X : Type v) ↦ X) (F.obj X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type v) ↦ X) (F.obj X_1)) → (fun (X : Type v) ↦ X) (F.obj X))
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X_1) (F.obj X_1)) : (a : X_1 ⟶ X_1) → F.obj X_1) (𝟙 X_1) :
        F.obj X_1) :
    (fun (X : Type v) ↦ X) (F.obj X))
Tactic: rw [e.homEquiv_eq, e'.homEquiv_eq, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
X : C
e e' : F.CorepresentableBy X
h :
  Eq.{v + 1} (α := F.obj X)
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X)
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X)
⊢ e = e'
have this : ∀ {Y : C} (f : X ⟶ Y),
  Eq.{v + 1} (α := F.obj Y)
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) : (a : X ⟶ Y) → F.obj Y) f : F.obj Y)
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) : (a : X ⟶ Y) → F.obj Y) f : F.obj Y)
Tactic: have : ∀ {Y : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f := fun {X} f ↦ by
    rw [e.homEquiv_eq, e'.homEquiv_eq, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
X : C
e e' : F.CorepresentableBy X
h :
  Eq.{v + 1} (α := F.obj X)
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X)
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj Y)
      (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) : (a : X ⟶ Y) → F.obj Y) f : F.obj Y)
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) : (a : X ⟶ Y) → F.obj Y) f : F.obj Y)
⊢ e = e'
have obtain : ∀ (e : {Y : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y))
  (he :
    ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
      Eq.{v + 1} (α := F.obj Y') ((e : (a : X ⟶ Y') → F.obj Y') (f ≫ g) : F.obj Y')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj Y'))
            ((e : (a : X ⟶ Y) → F.obj Y) f : F.obj Y) :
          (fun (X : Type v) ↦ X) (F.obj Y')))
  (h :
    Eq.{v + 1} (α := F.obj X)
      ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) :
            (a : X ⟶ X) → F.obj X)
          (𝟙 X) :
        F.obj X)
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X))
  (this :
    ∀ {Y : C} (f : X ⟶ Y),
      Eq.{v + 1} (α := F.obj Y)
        ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) :
              (a : X ⟶ Y) → F.obj Y)
            f :
          F.obj Y)
        (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) : (a : X ⟶ Y) → F.obj Y) f : F.obj Y)),
  { homEquiv := @e, homEquiv_comp := @he : F.CorepresentableBy X } = e'
Tactic: obtain ⟨e, he⟩ := e
Cleared hypotheses: e, h, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
X : C
e' : F.CorepresentableBy X
e : {Y : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)
he :
  ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj Y') ((e : (a : X ⟶ Y') → F.obj Y') (f ≫ g) : F.obj Y')
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj Y'))
          ((e : (a : X ⟶ Y) → F.obj Y) f : F.obj Y) :
        (fun (X : Type v) ↦ X) (F.obj Y'))
h :
  Eq.{v + 1} (α := F.obj X)
    ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) :
          (a : X ⟶ X) → F.obj X)
        (𝟙 X) :
      F.obj X)
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj Y)
      ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) :
            (a : X ⟶ Y) → F.obj Y)
          f :
        F.obj Y)
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) : (a : X ⟶ Y) → F.obj Y) f : F.obj Y)
⊢ { homEquiv := @e, homEquiv_comp := @he : F.CorepresentableBy X } = e'
have obtain : ∀ (e' : {Y : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y))
  (he' :
    ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
      Eq.{v + 1} (α := F.obj Y') ((e' : (a : X ⟶ Y') → F.obj Y') (f ≫ g) : F.obj Y')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj Y'))
            ((e' : (a : X ⟶ Y) → F.obj Y) f : F.obj Y) :
          (fun (X : Type v) ↦ X) (F.obj Y')))
  (h :
    Eq.{v + 1} (α := F.obj X)
      ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) :
            (a : X ⟶ X) → F.obj X)
          (𝟙 X) :
        F.obj X)
      ((({ homEquiv := @e', homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) :
            (a : X ⟶ X) → F.obj X)
          (𝟙 X) :
        F.obj X))
  (this :
    ∀ {Y : C} (f : X ⟶ Y),
      Eq.{v + 1} (α := F.obj Y)
        ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) :
              (a : X ⟶ Y) → F.obj Y)
            f :
          F.obj Y)
        ((({ homEquiv := @e', homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) :
              (a : X ⟶ Y) → F.obj Y)
            f :
          F.obj Y)),
  { homEquiv := @e, homEquiv_comp := @he : F.CorepresentableBy X } = { homEquiv := @e', homEquiv_comp := @he' }
Tactic: obtain ⟨e', he'⟩ := e'
Cleared hypotheses: e', h, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
X : C
e : {Y : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)
he :
  ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj Y') ((e : (a : X ⟶ Y') → F.obj Y') (f ≫ g) : F.obj Y')
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj Y'))
          ((e : (a : X ⟶ Y) → F.obj Y) f : F.obj Y) :
        (fun (X : Type v) ↦ X) (F.obj Y'))
e' : {Y : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)
he' :
  ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj Y') ((e' : (a : X ⟶ Y') → F.obj Y') (f ≫ g) : F.obj Y')
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj Y'))
          ((e' : (a : X ⟶ Y) → F.obj Y) f : F.obj Y) :
        (fun (X : Type v) ↦ X) (F.obj Y'))
h :
  Eq.{v + 1} (α := F.obj X)
    ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) :
          (a : X ⟶ X) → F.obj X)
        (𝟙 X) :
      F.obj X)
    ((({ homEquiv := @e', homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) :
          (a : X ⟶ X) → F.obj X)
        (𝟙 X) :
      F.obj X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj Y)
      ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) :
            (a : X ⟶ Y) → F.obj Y)
          f :
        F.obj Y)
      ((({ homEquiv := @e', homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) :
            (a : X ⟶ Y) → F.obj Y)
          f :
        F.obj Y)
⊢ @e = @e'
have h₁ : ∀ (x : C) (x_1 : X ⟶ x),
  Eq.{v + 1} (α := F.obj x) ((e : (a : X ⟶ x) → F.obj x) x_1 : F.obj x) ((e' : (a : X ⟶ x) → F.obj x) x_1 : F.obj x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
Y : C
r : F.RepresentableBy Y
X X' : Cᵒᵖ
f : X ⟶ X'
⊢ Eq (α := obj (obj yoneda Y) X ⟶ F.obj X')
    (map (obj yoneda Y) f ≫
      Iso.hom ((fun (x : Cᵒᵖ) ↦ (Equiv.toIso r.homEquiv : (unop x ⟶ Y) ≅ F.obj (op (unop x)))) X'))
    (Iso.hom ((fun (x : Cᵒᵖ) ↦ (Equiv.toIso r.homEquiv : (unop x ⟶ Y) ≅ F.obj (op (unop x)))) X) ≫ F.map f)
have h : ∀ (g : obj (obj yoneda Y) X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj yoneda Y) f ≫
          Iso.hom ((fun (x : Cᵒᵖ) ↦ (Equiv.toIso r.homEquiv : (unop x ⟶ Y) ≅ F.obj (op (unop x)))) X')))
      g =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom ((fun (x : Cᵒᵖ) ↦ (Equiv.toIso r.homEquiv : (unop x ⟶ Y) ≅ F.obj (op (unop x)))) X) ≫ F.map f))
      g
Tactic: ext g
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
Y : C
r : F.RepresentableBy Y
X X' : Cᵒᵖ
f : X ⟶ X'
g : obj (obj yoneda Y) X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj yoneda Y) f ≫
          Iso.hom ((fun (x : Cᵒᵖ) ↦ (Equiv.toIso r.homEquiv : (unop x ⟶ Y) ≅ F.obj (op (unop x)))) X')))
      g =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom ((fun (x : Cᵒᵖ) ↦ (Equiv.toIso r.homEquiv : (unop x ⟶ Y) ≅ F.obj (op (unop x)))) X) ≫ F.map f))
      g
have h : Eq (α := F.obj X') ((r.homEquiv : (a : unop X' ⟶ Y) → F.obj X') (f.unop ≫ g) : F.obj X')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj X')
      ((r.homEquiv : (a : unop X ⟶ Y) → F.obj X) g : F.obj X) :
    F.obj X')
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Type v₁
X_1 : C
r : F.CorepresentableBy X_1
X X' : C
f : X ⟶ X'
⊢ Eq (α := obj (obj coyoneda (op X_1)) X ⟶ F.obj X')
    (map (obj coyoneda (op X_1)) f ≫ Iso.hom ((fun (x : C) ↦ (Equiv.toIso r.homEquiv : (X_1 ⟶ x) ≅ F.obj x)) X'))
    (Iso.hom ((fun (x : C) ↦ (Equiv.toIso r.homEquiv : (X_1 ⟶ x) ≅ F.obj x)) X) ≫ F.map f)
have h : ∀ (g : obj (obj coyoneda (op X_1)) X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj coyoneda (op X_1)) f ≫ Iso.hom ((fun (x : C) ↦ (Equiv.toIso r.homEquiv : (X_1 ⟶ x) ≅ F.obj x)) X')))
      g =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom ((fun (x : C) ↦ (Equiv.toIso r.homEquiv : (X_1 ⟶ x) ≅ F.obj x)) X) ≫ F.map f))
      g
Tactic: ext g
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Type v₁
X_1 : C
r : F.CorepresentableBy X_1
X X' : C
f : X ⟶ X'
g : obj (obj coyoneda (op X_1)) X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj coyoneda (op X_1)) f ≫ Iso.hom ((fun (x : C) ↦ (Equiv.toIso r.homEquiv : (X_1 ⟶ x) ≅ F.obj x)) X')))
      g =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom ((fun (x : C) ↦ (Equiv.toIso r.homEquiv : (X_1 ⟶ x) ≅ F.obj x)) X) ≫ F.map f))
      g
have h : Eq (α := F.obj X') ((r.homEquiv : (a : X_1 ⟶ X') → F.obj X') (g ≫ f) : F.obj X')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj X')
      ((r.homEquiv : (a : X_1 ⟶ X) → F.obj X) g : F.obj X) :
    F.obj X')
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
e : Y ≅ X
x : F.RepresentableBy X
⊢ (fun (R : F.RepresentableBy Y) ↦ R.ofIsoObj e.symm) ((fun (R : F.RepresentableBy X) ↦ R.ofIsoObj e) x) = x
have h : Eq.{w + 1} (α := F.obj (op X))
  ((homEquiv ((fun (R : F.RepresentableBy Y) ↦ R.ofIsoObj e.symm) ((fun (R : F.RepresentableBy X) ↦ R.ofIsoObj e) x)) :
        (a : X ⟶ X) → F.obj (op X))
      (𝟙 X) :
    F.obj (op X))
  (((x.homEquiv : Equiv.{v₁ + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) : F.obj (op X))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
e : Y ≅ X
x : F.RepresentableBy Y
⊢ (fun (R : F.RepresentableBy X) ↦ R.ofIsoObj e) ((fun (R : F.RepresentableBy Y) ↦ R.ofIsoObj e.symm) x) = x
have h : Eq.{w + 1} (α := F.obj (op Y))
  ((homEquiv ((fun (R : F.RepresentableBy X) ↦ R.ofIsoObj e) ((fun (R : F.RepresentableBy Y) ↦ R.ofIsoObj e.symm) x)) :
        (a : Y ⟶ Y) → F.obj (op Y))
      (𝟙 Y) :
    F.obj (op Y))
  (((x.homEquiv : Equiv.{v₁ + 1, w + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X Y : C
e : Y ≅ X
x : F.CorepresentableBy X
⊢ (fun (R : F.CorepresentableBy Y) ↦ R.ofIsoObj e.symm) ((fun (R : F.CorepresentableBy X) ↦ R.ofIsoObj e) x) = x
have h : Eq.{w + 1} (α := F.obj X)
  ((homEquiv
          ((fun (R : F.CorepresentableBy Y) ↦ R.ofIsoObj e.symm) ((fun (R : F.CorepresentableBy X) ↦ R.ofIsoObj e) x)) :
        (a : X ⟶ X) → F.obj X)
      (𝟙 X) :
    F.obj X)
  (((x.homEquiv : Equiv.{v₁ + 1, w + 1} (X ⟶ X) (F.obj X)) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X Y : C
e : Y ≅ X
x : F.CorepresentableBy Y
⊢ (fun (R : F.CorepresentableBy X) ↦ R.ofIsoObj e) ((fun (R : F.CorepresentableBy Y) ↦ R.ofIsoObj e.symm) x) = x
have h : Eq.{w + 1} (α := F.obj Y)
  ((homEquiv
          ((fun (R : F.CorepresentableBy X) ↦ R.ofIsoObj e) ((fun (R : F.CorepresentableBy Y) ↦ R.ofIsoObj e.symm) x)) :
        (a : Y ⟶ Y) → F.obj Y)
      (𝟙 Y) :
    F.obj Y)
  (((x.homEquiv : Equiv.{v₁ + 1, w + 1} (Y ⟶ Y) (F.obj Y)) : (a : Y ⟶ Y) → F.obj Y) (𝟙 Y) : F.obj Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X_1 : C
R : F.RepresentableBy X_1
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Eq (α := obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ⟶ F.obj Y)
    (map (obj uliftYoneda.{w, v₁, u₁} X_1) f ≫
      Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            ((equivEquivIso :
                  (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                    (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                (Equiv.trans Equiv.ulift R.homEquiv) :
              obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
          Y))
    (Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            ((equivEquivIso :
                  (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                    (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                (Equiv.trans Equiv.ulift R.homEquiv) :
              obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
          X) ≫
      F.map f)
have h : ∀ (x : obj (obj uliftYoneda.{w, v₁, u₁} X_1) X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj uliftYoneda.{w, v₁, u₁} X_1) f ≫
          Iso.hom
            ((fun (X : Cᵒᵖ) ↦
                ((equivEquivIso :
                      (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                        (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
              Y)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (X : Cᵒᵖ) ↦
                ((equivEquivIso :
                      (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                        (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
              X) ≫
          F.map f))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X_1 : C
R : F.CorepresentableBy X_1
X Y : C
f : X ⟶ Y
⊢ Eq (α := obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ⟶ F.obj Y)
    (map (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) f ≫
      Iso.hom
        ((fun (X : C) ↦
            ((equivEquivIso :
                  (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                    (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                (Equiv.trans Equiv.ulift R.homEquiv) :
              obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            ((equivEquivIso :
                  (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                    (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                (Equiv.trans Equiv.ulift R.homEquiv) :
              obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
          X) ≫
      F.map f)
have h : ∀ (x : obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) f ≫
          Iso.hom
            ((fun (X : C) ↦
                ((equivEquivIso :
                      (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                        (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
              Y)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (X : C) ↦
                ((equivEquivIso :
                      (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                        (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
              X) ≫
          F.map f))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
η : obj yoneda X ⟶ F
⊢ (fun (ξ : F.obj (op X)) ↦
        {
          app := fun (x : Cᵒᵖ) ↦
            ↾fun (f : obj (obj yoneda X) x) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op f)) :
                  (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (F.obj (op (unop x))))
                ξ,
          naturality := ⋯ : NatTrans (obj yoneda X) F })
      ((fun (η : obj yoneda X ⟶ F) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
                (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op X))) → (fun (X : Type v₁) ↦ X) (F.obj (op X)))
              (𝟙 X) :
            (fun (X : Type v₁) ↦ X) (F.obj (op X))))
        η) =
    η
have w : ∀ (Y : Cᵒᵖ) (f : obj (obj yoneda X) Y),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (ξ : F.obj (op X)) ↦
              {
                app := fun (x : Cᵒᵖ) ↦
                  ↾fun (f : obj (obj yoneda X) x) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op f)) :
                        (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (F.obj (op (unop x))))
                      ξ,
                naturality := sorry : NatTrans (obj yoneda X) F })
            ((fun (η : obj yoneda X ⟶ F) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
                      (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op X))) →
                        (fun (X : Type v₁) ↦ X) (F.obj (op X)))
                    (𝟙 X) :
                  (fun (X : Type v₁) ↦ X) (F.obj (op X))))
              η))
          Y))
      f =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y)).toFun f
Tactic: ext Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (yonedaEquiv : (a : yoneda.obj X ⟶ yoneda.obj Y) → (yoneda.obj Y).obj (op X)) (map yoneda f) = f
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda f) (op X)) :
      (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op X))) → (fun (X : Type v₁) ↦ X) ((yoneda.obj Y).obj (op X)))
    (𝟙 X) =
  f
Tactic: rw [yonedaEquiv_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X X' : C
f : X' ⟶ X
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
x : F.obj (op X)
⊢ Eq (α := obj yoneda X' ⟶ F) (map yoneda f ≫ (Equiv.symm yonedaEquiv : (a : F.obj (op X)) → yoneda.obj X ⟶ F) x)
    ((Equiv.symm yonedaEquiv : (a : F.obj (op X')) → yoneda.obj X' ⟶ F)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (F.obj (op X')))
        x))
have a : Eq.{v₁ + 1} (α := F.obj (op X'))
  ((yonedaEquiv : (a : yoneda.obj X' ⟶ F) → F.obj (op X'))
      (map yoneda f ≫ (Equiv.symm yonedaEquiv : (a : F.obj (op X)) → yoneda.obj X ⟶ F) x) :
    F.obj (op X'))
  ((yonedaEquiv : (a : yoneda.obj X' ⟶ F) → F.obj (op X'))
      ((Equiv.symm yonedaEquiv : (a : F.obj (op X')) → yoneda.obj X' ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
            (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (F.obj (op X')))
          x)) :
    F.obj (op X'))
Tactic: apply yonedaEquiv.injective