awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Yoneda
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
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')
⊢ 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:
rw [e.homEquiv_comp]

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
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')
        ((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:
apply e'.hom.naturality_apply

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Yoneda
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
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)))
| (((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 [← Category.comp_id f, e.homEquiv_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
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)))
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)))
⊢ 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]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
Y Y' : C
e : F.RepresentableBy Y
e' : F.RepresentableBy Y'
ε : {X : C} → (X ⟶ Y) ≃ (X ⟶ Y') := fun {X : C} ↦ Equiv.trans e.homEquiv (Equiv.symm e'.homEquiv)
⊢ ∀ {Z : C} (f : Z ⟶ Y),
    (fun {Z : C} ↦ ((⇑(Equiv.symm ε) : (a : Z ⟶ Y') → Z ⟶ Y) : (a : Z ⟶ Y') → Z ⟶ Y))
        ((fun {Z : C} ↦ ((⇑ε : (a : Z ⟶ Y) → Z ⟶ Y') : (a : Z ⟶ Y) → Z ⟶ Y')) f) =
      f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
Y Y' : C
e : F.RepresentableBy Y
e' : F.RepresentableBy Y'
ε : {X : C} → (X ⟶ Y) ≃ (X ⟶ Y') := fun {X : C} ↦ Equiv.trans e.homEquiv (Equiv.symm e'.homEquiv)
⊢ ∀ {Z : C} (f : Z ⟶ Y'),
    (fun {Z : C} ↦ ((⇑ε : (a : Z ⟶ Y) → Z ⟶ Y') : (a : Z ⟶ Y) → Z ⟶ Y'))
        ((fun {Z : C} ↦ ((⇑(Equiv.symm ε) : (a : Z ⟶ Y') → Z ⟶ Y) : (a : Z ⟶ Y') → Z ⟶ Y)) f) =
      f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
Y Y' : C
e : F.RepresentableBy Y
e' : F.RepresentableBy Y'
ε : {X : C} → (X ⟶ Y) ≃ (X ⟶ Y') := fun {X : C} ↦ Equiv.trans e.homEquiv (Equiv.symm e'.homEquiv)
⊢ ∀ {Z Z' : C} (f : Z' ⟶ Z) (g : Z ⟶ Y),
    Eq (α := Z' ⟶ Y') ((fun {Z : C} ↦ ((⇑ε : (a : Z ⟶ Y) → Z ⟶ Y') : (a : Z ⟶ Y) → Z ⟶ Y')) (f ≫ g))
      (f ≫ (fun {Z : C} ↦ ((⇑ε : (a : Z ⟶ Y) → Z ⟶ Y') : (a : Z ⟶ Y) → Z ⟶ Y')) g)

Tactic:
simp [ε, comp_homEquiv_symm, homEquiv_comp]

Premises used: CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm, CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
X X' : C
e : F.CorepresentableBy X
e' : F.CorepresentableBy X'
ε : {Y : C} → (X ⟶ Y) ≃ (X' ⟶ Y) := fun {Y : C} ↦ Equiv.trans e.homEquiv (Equiv.symm e'.homEquiv)
⊢ ∀ {Z : C} (f : X ⟶ Z),
    (fun {Z : C} ↦ ((⇑(Equiv.symm ε) : (a : X' ⟶ Z) → X ⟶ Z) : (a : X' ⟶ Z) → X ⟶ Z))
        ((fun {Z : C} ↦ ((⇑ε : (a : X ⟶ Z) → X' ⟶ Z) : (a : X ⟶ Z) → X' ⟶ Z)) f) =
      f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
X X' : C
e : F.CorepresentableBy X
e' : F.CorepresentableBy X'
ε : {Y : C} → (X ⟶ Y) ≃ (X' ⟶ Y) := fun {Y : C} ↦ Equiv.trans e.homEquiv (Equiv.symm e'.homEquiv)
⊢ ∀ {Z : C} (f : X' ⟶ Z),
    (fun {Z : C} ↦ ((⇑ε : (a : X ⟶ Z) → X' ⟶ Z) : (a : X ⟶ Z) → X' ⟶ Z))
        ((fun {Z : C} ↦ ((⇑(Equiv.symm ε) : (a : X' ⟶ Z) → X ⟶ Z) : (a : X' ⟶ Z) → X ⟶ Z)) f) =
      f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
X X' : C
e : F.CorepresentableBy X
e' : F.CorepresentableBy X'
ε : {Y : C} → (X ⟶ Y) ≃ (X' ⟶ Y) := fun {Y : C} ↦ Equiv.trans e.homEquiv (Equiv.symm e'.homEquiv)
⊢ ∀ {Z Z' : C} (f : X' ⟶ Z) (g : Z ⟶ Z'),
    Eq (α := X ⟶ Z') ((fun {Z : C} ↦ ((⇑(Equiv.symm ε) : (a : X' ⟶ Z) → X ⟶ Z) : (a : X' ⟶ Z) → X ⟶ Z)) (f ≫ g))
      ((fun {Z : C} ↦ ((⇑(Equiv.symm ε) : (a : X' ⟶ Z) → X ⟶ Z) : (a : X' ⟶ Z) → X ⟶ Z)) f ≫ g)

Tactic:
simp [ε, homEquiv_symm_comp, homEquiv_comp]

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp, CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp
-- Module: Mathlib.CategoryTheory.Yoneda
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)))
rw₂ 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))

Tactic:
rw [e.homEquiv_eq, e'.homEquiv_eq, h]

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_eq
-- Module: Mathlib.CategoryTheory.Yoneda
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))

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]
-- Module: Mathlib.CategoryTheory.Yoneda
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))
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'
⊢ e = e'

Tactic:
obtain ⟨e, he⟩ := e
-- Module: Mathlib.CategoryTheory.Yoneda
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))
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' }
⊢ { homEquiv := @e, homEquiv_comp := @he : F.RepresentableBy Y } = e'

Tactic:
obtain ⟨e', he'⟩ := e'
-- Module: Mathlib.CategoryTheory.Yoneda
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))
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))
⊢ @e = @e'

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Yoneda
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))
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:
apply this
-- Module: Mathlib.CategoryTheory.Yoneda
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 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:
rfl