awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Yoneda
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))
rw₂ 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)

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

Premises used: CategoryTheory.Functor.CorepresentableBy.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)
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)
⊢ ∀ {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]
-- Module: Mathlib.CategoryTheory.Yoneda
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)
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'
⊢ 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)
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)
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' }
⊢ { homEquiv := @e, homEquiv_comp := @he : F.CorepresentableBy X } = 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)
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)
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)
⊢ @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)
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)
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:
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)
X : C
e : {Y : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)
he 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:
rfl
-- 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
r : F.RepresentableBy Y
X X' : Cᵒᵖ
f : X ⟶ X'
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
⊢ 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)

Tactic:
ext g
-- 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
r : F.RepresentableBy Y
X X' : Cᵒᵖ
f : X ⟶ X'
g : obj (obj yoneda Y) X
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')
⊢ 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:
dsimp
-- 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
r : F.RepresentableBy Y
X X' : Cᵒᵖ
f : X ⟶ X'
g : obj (obj yoneda Y) X
⊢ 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:
apply r.homEquiv_comp

Premises used: 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 : obj yoneda Y ≅ F
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ Eq (α := F.obj (op X)) ((Iso.toEquiv (e.app (op X)) : (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)))
        ((Iso.toEquiv (e.app (op X')) : (a : X' ⟶ Y) → F.obj (op X')) g : F.obj (op X')) :
      (fun (X : Type v₁) ↦ X) (F.obj (op X)))

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
X Y : C
⊢ Eq.{v₁ + 1} (α := (Y ⟶ X) ≃ obj (obj yoneda X) (op Y)) (homEquiv (RepresentableBy.yoneda X)) (Equiv.refl (Y ⟶ X))

Tactic:
rfl

Premises used: CategoryTheory.Iso.toEquiv, Equiv.refl, rfl
-- Module: Mathlib.CategoryTheory.Yoneda
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'
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
⊢ 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)

Tactic:
ext g
-- Module: Mathlib.CategoryTheory.Yoneda
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
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')
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Yoneda
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
⊢ 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:
apply r.homEquiv_comp

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Type v₁
X_1 : C
e : obj coyoneda (op X_1) ≅ F
X X' : C
f : X ⟶ X'
g : X_1 ⟶ X
⊢ Eq (α := F.obj X') (((e.app X').toEquiv : (a : X_1 ⟶ X') → F.obj X') (g ≫ f) : F.obj X')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj X'))
        (((e.app X).toEquiv : (a : X_1 ⟶ X) → F.obj X) g : F.obj X) :
      (fun (X : Type v₁) ↦ X) (F.obj X'))

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
X : Cᵒᵖ
Y : C
⊢ Eq.{v₁ + 1} (α := (unop X ⟶ Y) ≃ obj (obj coyoneda X) Y) (homEquiv (CorepresentableBy.coyoneda X))
    (Equiv.refl (unop X ⟶ Y))

Tactic:
rfl

Premises used: CategoryTheory.Iso.toEquiv, Equiv.refl, rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
R : F.RepresentableBy X
e : Y ≅ X
⊢ ∀ {X_1 X' : C} (f : X_1 ⟶ X') (g : X' ⟶ Y),
    Eq.{w + 1} (α := F.obj (op X_1))
      (((Equiv.trans e.homToEquiv R.homEquiv : Equiv.{v₁ + 1, w + 1} (X_1 ⟶ Y) (F.obj (op X_1))) :
            (a : X_1 ⟶ Y) → F.obj (op X_1))
          (f ≫ g) :
        F.obj (op X_1))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X'))) → (fun (X : Type w) ↦ X) (F.obj (op X_1)))
          (((Equiv.trans e.homToEquiv R.homEquiv : Equiv.{v₁ + 1, w + 1} (X' ⟶ Y) (F.obj (op X'))) :
                (a : X' ⟶ Y) → F.obj (op X'))
              g :
            F.obj (op X')) :
        (fun (X : Type w) ↦ X) (F.obj (op X_1)))

Tactic:
simp [R.homEquiv_comp]

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X Y : C
R : F.CorepresentableBy X
e : Y ≅ X
⊢ ∀ {Y_1 Y' : C} (g : Y_1 ⟶ Y') (f : Y ⟶ Y_1),
    Eq.{w + 1} (α := F.obj Y')
      (((Equiv.trans e.homFromEquiv R.homEquiv : Equiv.{v₁ + 1, w + 1} (Y ⟶ Y') (F.obj Y')) : (a : Y ⟶ Y') → F.obj Y')
          (f ≫ g) :
        F.obj Y')
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w) ↦ X) (F.obj Y_1)) → (fun (X : Type w) ↦ X) (F.obj Y'))
          (((Equiv.trans e.homFromEquiv R.homEquiv : Equiv.{v₁ + 1, w + 1} (Y ⟶ Y_1) (F.obj Y_1)) :
                (a : Y ⟶ Y_1) → F.obj Y_1)
              f :
            F.obj Y_1) :
        (fun (X : Type w) ↦ X) (F.obj Y'))

Tactic:
simp [R.homEquiv_comp]

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
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
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))
⊢ (fun (R : F.RepresentableBy Y) ↦ R.ofIsoObj e.symm) ((fun (R : F.RepresentableBy X) ↦ R.ofIsoObj e) x) = x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Yoneda
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
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
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))
⊢ (fun (R : F.RepresentableBy X) ↦ R.ofIsoObj e) ((fun (R : F.RepresentableBy Y) ↦ R.ofIsoObj e.symm) x) = x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Yoneda
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
⊢ 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:
simp