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 F' : Functor.{v₁, v, u₁, v + 1} C (Type v)
X : C
e : F.CorepresentableBy X
e' : F ≅ F'
Y Y' : C
g : Y ⟶ Y'
f : X ⟶ Y
⊢ Eq.{v + 1} (α := F'.obj Y')
    ((Equiv.trans e.homEquiv (e'.app Y').toEquiv : (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'))
        ((Equiv.trans e.homEquiv (e'.app Y).toEquiv : (a : X ⟶ Y) → F'.obj Y) f : F'.obj Y) :
      (fun (X : Type v) ↦ X) (F'.obj Y'))
have dsimp : Eq (α := F'.obj Y')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app Y') : (a : F.obj Y') → F'.obj Y')
      (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y') (F.obj Y')) : (a : X ⟶ Y') → F.obj Y') (f ≫ g) : F.obj Y') :
    F'.obj Y')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map g) : (a : F'.obj Y) → F'.obj Y')
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app Y) : (a : F.obj Y) → 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) :
        F'.obj Y) :
    F'.obj Y')
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F F' : Functor.{v₁, v, u₁, v + 1} C (Type v)
X : C
e : F.CorepresentableBy X
e' : F ≅ F'
Y Y' : C
g : Y ⟶ Y'
f : X ⟶ Y
⊢ Eq (α := F'.obj Y')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app Y') : (a : F.obj Y') → F'.obj Y')
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y') (F.obj Y')) : (a : X ⟶ Y') → F.obj Y') (f ≫ g) : F.obj Y') :
      F'.obj Y')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map g) : (a : F'.obj Y) → F'.obj Y')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app Y) : (a : F.obj Y) → 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) :
          F'.obj Y) :
      F'.obj Y')
have rw : Eq (α := F'.obj Y')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app Y') : (a : F.obj Y') → 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.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) : (a : X ⟶ Y) → F.obj Y) f : F.obj Y) :
        (fun (X : Type v) ↦ X) (F.obj Y')) :
    F'.obj Y')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map g) : (a : F'.obj Y) → F'.obj Y')
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app Y) : (a : F.obj Y) → 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) :
        F'.obj Y) :
    F'.obj Y')
Tactic: rw [e.homEquiv_comp]
-- 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
e : F.RepresentableBy Y
X : C
f : X ⟶ Y
| (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
have rw : ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
      (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y)) :
  (fun (X : Type v) ↦ X) (F.obj (op X)))
Tactic: rw [← Category.comp_id f, e.homEquiv_comp]
-- 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
e : F.RepresentableBy Y
X : C
f : X ⟶ Y
⊢ Eq.{v + 1} (α := F.obj (op X))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
          F.obj (op Y)) :
      (fun (X : Type v) ↦ X) (F.obj (op X)))
have conv_lhs : Eq.{v + 1} (α := F.obj (op X))
  (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
      (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
        F.obj (op Y)) :
    (fun (X : Type v) ↦ X) (F.obj (op X)))
Tactic: conv_lhs => rw [← Category.comp_id f, e.homEquiv_comp]
-- 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
e : F.RepresentableBy Y
X : C
f : X ⟶ Y
conv_lhs :
  Eq.{v + 1} (α := F.obj (op X))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
          F.obj (op Y)) :
      (fun (X : Type v) ↦ X) (F.obj (op X)))
⊢ Eq.{v + 1} (α := F.obj (op X))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
          F.obj (op Y)) :
      (fun (X : Type v) ↦ X) (F.obj (op X)))
have conv_lhs₁ : Eq (α := F.obj (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
      (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
        F.obj (op Y)) :
    (fun (X : Type v) ↦ X) (F.obj (op X)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
      (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
        F.obj (op Y)) :
    (fun (X : Type v) ↦ X) (F.obj (op X)))
Tactic: conv_lhs => rw [← Category.comp_id f, e.homEquiv_comp]
-- 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
e e' : F.RepresentableBy Y
h :
  Eq.{v + 1} (α := F.obj (op Y))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
X : C
f : X ⟶ Y
⊢ Eq.{v + 1} (α := F.obj (op X))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
have rw : Eq (α := F.obj (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
      (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
        F.obj (op Y)) :
    (fun (X : Type v) ↦ X) (F.obj (op X)))
  (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
Tactic: 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)
Y : C
e e' : F.RepresentableBy Y
h :
  Eq.{v + 1} (α := F.obj (op Y))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
X : C
f : X ⟶ Y
rw :
  Eq (α := F.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
          F.obj (op Y)) :
      (fun (X : Type v) ↦ X) (F.obj (op X)))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
⊢ Eq.{v + 1} (α := F.obj (op X))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
have rw₁ : Eq (α := F.obj (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
      (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
        F.obj (op Y)) :
    (fun (X : Type v) ↦ X) (F.obj (op X)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
        F.obj (op Y)) :
    (fun (X : Type v) ↦ X) (F.obj (op X)))
Tactic: 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)
Y : C
e e' : F.RepresentableBy Y
h :
  Eq.{v + 1} (α := F.obj (op Y))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
X : C
f : X ⟶ Y
rw :
  Eq (α := F.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
          F.obj (op Y)) :
      (fun (X : Type v) ↦ X) (F.obj (op X)))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
rw₁ :
  Eq (α := F.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
          F.obj (op Y)) :
      (fun (X : Type v) ↦ X) (F.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
        (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
          F.obj (op Y)) :
      (fun (X : Type v) ↦ X) (F.obj (op X)))
⊢ Eq.{v + 1} (α := F.obj (op X))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
have rw₂ : Eq (α := F.obj (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
        F.obj (op Y)) :
    (fun (X : Type v) ↦ X) (F.obj (op X)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
        F.obj (op Y)) :
    (fun (X : Type v) ↦ X) (F.obj (op 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)
Y : C
e e' : F.RepresentableBy Y
h :
  Eq.{v + 1} (α := F.obj (op Y))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
⊢ e = e'
have this : ∀ {X : C} (f : X ⟶ Y),
  Eq.{v + 1} (α := F.obj (op X))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
Tactic: have : ∀ {X : 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)
Y : C
e e' : F.RepresentableBy Y
h :
  Eq.{v + 1} (α := F.obj (op Y))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
this :
  ∀ {X : C} (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj (op X))
      (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
⊢ e = e'
have obtain : ∀ (e : {X : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X)))
  (he :
    ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
      Eq.{v + 1} (α := F.obj (op X)) ((e : (a : X ⟶ Y) → F.obj (op X)) (f ≫ g) : F.obj (op X))
        ((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)))
            ((e : (a : X' ⟶ Y) → F.obj (op X')) g : F.obj (op X')) :
          (fun (X : Type v) ↦ X) (F.obj (op X))))
  (h :
    Eq.{v + 1} (α := F.obj (op Y))
      ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) :
            (a : Y ⟶ Y) → F.obj (op Y))
          (𝟙 Y) :
        F.obj (op Y))
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) :
        F.obj (op Y)))
  (this :
    ∀ {X : C} (f : X ⟶ Y),
      Eq.{v + 1} (α := F.obj (op X))
        ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) :
              (a : X ⟶ Y) → F.obj (op X))
            f :
          F.obj (op X))
        (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))),
  { homEquiv := @e, homEquiv_comp := @he : F.RepresentableBy Y } = 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)
Y : C
e' : F.RepresentableBy Y
e : {X : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))
he :
  ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
    Eq.{v + 1} (α := F.obj (op X)) ((e : (a : X ⟶ Y) → F.obj (op X)) (f ≫ g) : F.obj (op X))
      ((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)))
          ((e : (a : X' ⟶ Y) → F.obj (op X')) g : F.obj (op X')) :
        (fun (X : Type v) ↦ X) (F.obj (op X)))
h :
  Eq.{v + 1} (α := F.obj (op Y))
    ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) :
          (a : Y ⟶ Y) → F.obj (op Y))
        (𝟙 Y) :
      F.obj (op Y))
    (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) : (a : Y ⟶ Y) → F.obj (op Y)) (𝟙 Y) : F.obj (op Y))
this :
  ∀ {X : C} (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj (op X))
      ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) :
            (a : X ⟶ Y) → F.obj (op X))
          f :
        F.obj (op X))
      (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) f : F.obj (op X))
⊢ { homEquiv := @e, homEquiv_comp := @he : F.RepresentableBy Y } = e'
have obtain : ∀ (e' : {X : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X)))
  (he' :
    ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
      Eq.{v + 1} (α := F.obj (op X)) ((e' : (a : X ⟶ Y) → F.obj (op X)) (f ≫ g) : F.obj (op X))
        ((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)))
            ((e' : (a : X' ⟶ Y) → F.obj (op X')) g : F.obj (op X')) :
          (fun (X : Type v) ↦ X) (F.obj (op X))))
  (h :
    Eq.{v + 1} (α := F.obj (op Y))
      ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) :
            (a : Y ⟶ Y) → F.obj (op Y))
          (𝟙 Y) :
        F.obj (op Y))
      ((({ homEquiv := @e', homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) :
            (a : Y ⟶ Y) → F.obj (op Y))
          (𝟙 Y) :
        F.obj (op Y)))
  (this :
    ∀ {X : C} (f : X ⟶ Y),
      Eq.{v + 1} (α := F.obj (op X))
        ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) :
              (a : X ⟶ Y) → F.obj (op X))
            f :
          F.obj (op X))
        ((({ homEquiv := @e', homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) :
              (a : X ⟶ Y) → F.obj (op X))
            f :
          F.obj (op X))),
  { homEquiv := @e, homEquiv_comp := @he : F.RepresentableBy Y } = { 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)
Y : C
e : {X : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))
he :
  ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
    Eq.{v + 1} (α := F.obj (op X)) ((e : (a : X ⟶ Y) → F.obj (op X)) (f ≫ g) : F.obj (op X))
      ((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)))
          ((e : (a : X' ⟶ Y) → F.obj (op X')) g : F.obj (op X')) :
        (fun (X : Type v) ↦ X) (F.obj (op X)))
e' : {X : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))
he' :
  ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
    Eq.{v + 1} (α := F.obj (op X)) ((e' : (a : X ⟶ Y) → F.obj (op X)) (f ≫ g) : F.obj (op X))
      ((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)))
          ((e' : (a : X' ⟶ Y) → F.obj (op X')) g : F.obj (op X')) :
        (fun (X : Type v) ↦ X) (F.obj (op X)))
h :
  Eq.{v + 1} (α := F.obj (op Y))
    ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) :
          (a : Y ⟶ Y) → F.obj (op Y))
        (𝟙 Y) :
      F.obj (op Y))
    ((({ homEquiv := @e', homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (Y ⟶ Y) (F.obj (op Y))) :
          (a : Y ⟶ Y) → F.obj (op Y))
        (𝟙 Y) :
      F.obj (op Y))
this :
  ∀ {X : C} (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj (op X))
      ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) :
            (a : X ⟶ Y) → F.obj (op X))
          f :
        F.obj (op X))
      ((({ homEquiv := @e', homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) :
            (a : X ⟶ Y) → F.obj (op X))
          f :
        F.obj (op X))
⊢ @e = @e'
have h₁ : ∀ (x : C) (x_1 : x ⟶ Y),
  Eq.{v + 1} (α := F.obj (op x)) ((e : (a : x ⟶ Y) → F.obj (op x)) x_1 : F.obj (op x))
    ((e' : (a : x ⟶ Y) → F.obj (op x)) x_1 : 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₁, 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
⊢ 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))
  (((e'.homEquiv : Equiv.{v₁ + 1, v + 1} (X_1 ⟶ X) (F.obj X)) : (a : X_1 ⟶ X) → F.obj X) f : F.obj X)
Tactic: 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_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)
⊢ 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]