awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Yoneda
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
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 := ⋯ : 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:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
ξ : F.obj (op X)
⊢ (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))))
      ((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 })
        ξ) =
    ξ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : obj yoneda X ⟶ F
⊢ Eq.{v₁ + 1} (α := F.obj (op X)) ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (op X)) f : F.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.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)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
x : F.obj (op X)
Y : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α := obj (obj yoneda X) Y ⟶ F.obj Y)
    (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj (op X)) → yoneda.obj X ⟶ F) x) Y)
    (↾fun (f : obj (obj yoneda X) Y) ↦
      (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 Y))
        x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
x : F.obj (op X)
Y : Cᵒᵖ
f : unop Y ⟶ X
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj (op X)) → yoneda.obj X ⟶ F) x) Y) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        f :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((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 (unop Y))))
        x :
      (fun (X : Type v₁) ↦ X) (F.obj (op (unop Y))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : obj yoneda X ⟶ F
g : Y ⟶ X
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
        ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (op X)) f : F.obj (op X)) :
      (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
    ((yonedaEquiv : (a : yoneda.obj Y ⟶ F) → F.obj (op Y)) (map yoneda g ≫ f) : F.obj (op Y))

Tactic:
simp [yonedaEquiv, ← f.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.yonedaEquiv
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : obj yoneda (unop X) ⟶ F
g : X ⟶ Y
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        ((yonedaEquiv : (a : yoneda.obj (unop X) ⟶ F) → F.obj (op (unop X))) f : F.obj (op (unop X))) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((yonedaEquiv : (a : yoneda.obj (unop Y) ⟶ F) → F.obj (op (unop Y))) (map yoneda g.unop ≫ f) : F.obj (op (unop Y)))

Tactic:
yonedaEquiv_naturality _ _

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.yonedaEquiv_naturality
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
α : obj yoneda X ⟶ F
β : F ⟶ G
⊢ Eq.{v₁ + 1} (α := G.obj (op X)) ((yonedaEquiv : (a : yoneda.obj X ⟶ G) → G.obj (op X)) (α ≫ β) : G.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (β.app (op X)) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (G.obj (op X)))
        ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (op X)) α : F.obj (op X)) :
      (fun (X : Type v₁) ↦ X) (G.obj (op X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
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
⊢ (yonedaEquiv : (a : yoneda.obj X ⟶ yoneda.obj Y) → (yoneda.obj Y).obj (op X)) (map yoneda f) = f

Tactic:
rw [yonedaEquiv_apply]

Premises used: CategoryTheory.yonedaEquiv_apply
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (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:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
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)
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'))
⊢ 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))

Tactic:
apply yonedaEquiv.injective

Premises used: Equiv.injective, CategoryTheory.yonedaEquiv
-- Module: Mathlib.CategoryTheory.Yoneda
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.{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:
simp [yonedaEquiv]

Premises used: CategoryTheory.yonedaEquiv
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F F' : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ F'
x : F.obj (op X)
a :
  Eq.{v₁ + 1} (α := 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) x ≫ f) :
      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.app (op X)) :
              (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (F'.obj (op X)))
            x)) :
      F'.obj (op X))
⊢ Eq (α := obj yoneda X ⟶ F')
    ((Equiv.symm yonedaEquiv : (a : F.obj (op X)) → yoneda.obj X ⟶ F) x ≫ f : obj yoneda X ⟶ F')
    ((Equiv.symm yonedaEquiv : (a : F'.obj (op X)) → yoneda.obj X ⟶ F')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
            (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (F'.obj (op X)))
          x) :
      obj yoneda X ⟶ F')

Tactic:
apply yonedaEquiv.injective

Premises used: Equiv.injective, CategoryTheory.yonedaEquiv
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F F' : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ F'
x : F.obj (op X)
⊢ Eq.{v₁ + 1} (α := 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) x ≫ f) :
      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.app (op X)) :
              (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:
simp [yonedaEquiv_comp]

Premises used: CategoryTheory.yonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : obj yoneda X ⟶ F
g : Y ⟶ X
rw :
  Eq.{v₁ + 1} (α := (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
    ((yonedaEquiv : (a : yoneda.obj Y ⟶ F) → F.obj (op Y)) (map yoneda g ≫ f) : F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op Y))) → (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
rw₁ :
  Eq (α := (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op Y))) → (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
        ((yonedaEquiv : (a : yoneda.obj Y ⟶ yoneda.obj X) → (yoneda.obj X).obj (op Y)) (map yoneda g) :
          obj (obj yoneda X) (op Y)) :
      (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op Y))) → (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
rw₂ rw₃ :
  Eq (α := (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op Y))) → (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op Y))) → (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
        ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (op X)) f : F.obj (op X)) :
      (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op Y))) → (fun (X : Type v₁) ↦ X) (F.obj (op Y)))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj (op Y)))

Tactic:
rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Premises used: CategoryTheory.yonedaEquiv_yoneda_map, CategoryTheory.yonedaEquiv_naturality, CategoryTheory.yonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : obj yoneda (unop X) ⟶ F
g : X ⟶ Y
rw :
  Eq.{v₁ + 1} (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((yonedaEquiv : (a : yoneda.obj (unop Y) ⟶ F) → F.obj (op (unop Y))) (map yoneda g.unop ≫ f) : F.obj (op (unop Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj (unop X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        g.unop :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
rw₁ :
  Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop Y))) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj (unop X)).obj (op (unop Y)))) →
            (fun (X : Type v₁) ↦ X) (F.obj (op (unop Y))))
        ((yonedaEquiv : (a : yoneda.obj (unop Y) ⟶ yoneda.obj (unop X)) → (yoneda.obj (unop X)).obj (op (unop Y)))
            (map yoneda g.unop) :
          obj (obj yoneda (unop X)) (op (unop Y))) :
      (fun (X : Type v₁) ↦ X) (F.obj (op (unop Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj (unop X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        g.unop :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
rw₂ rw₃ :
  Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop Y))) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj (unop X)).obj (op (unop Y)))) →
            (fun (X : Type v₁) ↦ X) (F.obj (op (unop Y))))
        g.unop :
      (fun (X : Type v₁) ↦ X) (F.obj (op (unop Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj (unop X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        g.unop :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        ((yonedaEquiv : (a : yoneda.obj (unop X) ⟶ F) → F.obj (op (unop X))) f : F.obj (op (unop X))) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj (unop X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        g.unop :
      (fun (X : Type v₁) ↦ X) (F.obj Y))

Tactic:
rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Premises used: CategoryTheory.yonedaEquiv_yoneda_map, CategoryTheory.yonedaEquiv_naturality', CategoryTheory.yonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
t : F.obj X
obtain :
  ∀ (u : obj yoneda (unop X) ⟶ F),
    Eq (α := obj yoneda (unop Y) ⟶ F)
      ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop Y))) → yoneda.obj (unop Y) ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
            ((yonedaEquiv : (a : yoneda.obj (unop X) ⟶ F) → F.obj (op (unop X))) u : F.obj (op (unop X)))) :
        obj yoneda (unop Y) ⟶ F)
      (map yoneda f.unop ≫
          (Equiv.symm yonedaEquiv : (a : F.obj (op (unop X))) → yoneda.obj (unop X) ⟶ F)
            ((yonedaEquiv : (a : yoneda.obj (unop X) ⟶ F) → F.obj (op (unop X))) u) :
        obj yoneda (unop Y) ⟶ F)
⊢ Eq (α := obj yoneda (unop Y) ⟶ F)
    ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop Y))) → yoneda.obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
          t) :
      obj yoneda (unop Y) ⟶ F)
    (map yoneda f.unop ≫ (Equiv.symm yonedaEquiv : (a : F.obj (op (unop X))) → yoneda.obj (unop X) ⟶ F) t :
      obj yoneda (unop Y) ⟶ F)

Tactic:
obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t

Premises used: Equiv.surjective, CategoryTheory.yonedaEquiv, rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
u : obj yoneda (unop X) ⟶ F
rw :
  Eq (α := obj yoneda (unop Y) ⟶ F)
    ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop Y))) → yoneda.obj (unop Y) ⟶ F)
        ((yonedaEquiv : (a : yoneda.obj (unop Y) ⟶ F) → F.obj (op (unop Y))) (map yoneda f.unop ≫ u)) :
      obj yoneda (unop Y) ⟶ F)
    (map yoneda f.unop ≫
        (Equiv.symm yonedaEquiv : (a : F.obj (op (unop X))) → yoneda.obj (unop X) ⟶ F)
          ((yonedaEquiv : (a : yoneda.obj (unop X) ⟶ F) → F.obj (op (unop X))) u) :
      obj yoneda (unop Y) ⟶ F)
rw₁ :
  map yoneda f.unop ≫ u =
    map yoneda f.unop ≫
      (Equiv.symm yonedaEquiv : (a : F.obj (op (unop X))) → yoneda.obj (unop X) ⟶ F)
        ((yonedaEquiv : (a : yoneda.obj (unop X) ⟶ F) → F.obj (op (unop X))) u)
rw₂ rw₃ : map yoneda f.unop ≫ u = map yoneda f.unop ≫ u
⊢ Eq (α := obj yoneda (unop Y) ⟶ F)
    ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop Y))) → yoneda.obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
          ((yonedaEquiv : (a : yoneda.obj (unop X) ⟶ F) → F.obj (op (unop X))) u : F.obj (op (unop X)))) :
      obj yoneda (unop Y) ⟶ F)
    (map yoneda f.unop ≫
        (Equiv.symm yonedaEquiv : (a : F.obj (op (unop X))) → yoneda.obj (unop X) ⟶ F)
          ((yonedaEquiv : (a : yoneda.obj (unop X) ⟶ F) → F.obj (op (unop X))) u) :
      obj yoneda (unop Y) ⟶ F)

Tactic:
rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.yonedaEquiv_naturality'
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : P ⟶ Q
h : ∀ (X : C) (p : obj yoneda X ⟶ P), p ≫ f = p ≫ g
w :
  ∀ (X : Cᵒᵖ) (x : P.obj X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app X)).toFun x
⊢ f = g

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : P ⟶ Q
h : ∀ (X : C) (p : obj yoneda X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app X)).toFun x

Tactic:
simpa only [yonedaEquiv_comp, Equiv.apply_symm_apply]
    using congr_arg (yonedaEquiv) (h _ (yonedaEquiv.symm x))

Premises used: Equiv.apply_symm_apply, congr_arg, Equiv.symm, CategoryTheory.yonedaEquiv, DFunLike.coe, CategoryTheory.yonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : Cᵒᵖ × Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
α : P ⟶ Q
x : obj (yonedaEvaluation C) P
⊢ Eq (α := obj (evaluationUncurried Cᵒᵖ (Type v₁)) Q)
    (ULift.down.{u₁, v₁}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (yonedaEvaluation C) α) :
            (a : (fun (X : Type (max u₁ v₁)) ↦ X) ((yonedaEvaluation C).obj P)) →
              (fun (X : Type (max u₁ v₁)) ↦ X) ((yonedaEvaluation C).obj Q))
          x) :
      obj (evaluationUncurried Cᵒᵖ (Type v₁)) Q)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.2.app Q.1) :
          (a : (fun (X : Type v₁) ↦ X) (P.2.obj Q.1)) → (fun (X : Type v₁) ↦ X) (Q.2.obj Q.1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.2.map α.1) :
              (a : (fun (X : Type v₁) ↦ X) (P.2.obj P.1)) → (fun (X : Type v₁) ↦ X) (P.2.obj Q.1))
            x.down :
          (fun (X : Type v₁) ↦ X) (P.2.obj Q.1)) :
      (fun (X : Type v₁) ↦ X) (Q.2.obj Q.1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ × Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
x y : obj (yonedaPairing C) X
w : ∀ (Y : Cᵒᵖ), x.app Y = y.app Y
⊢ x = y

Tactic:
NatTrans.ext (funext w)

Premises used: CategoryTheory.NatTrans.ext, funext
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : Cᵒᵖ × Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
α : P ⟶ Q
⊢ Eq (α := obj (yonedaPairing C) P ⟶ obj (yonedaPairing C) Q) (map (yonedaPairing C) α)
    (↾fun (β : obj yoneda (unop P.1) ⟶ P.2) ↦ map yoneda α.1.unop ≫ β ≫ α.2)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
this :
  ∀ (Y : Cᵒᵖ) (G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (f : (X, F) ⟶ (Y, G)),
    Eq (α := obj (yonedaPairing C) (X, F) ⟶ obj (yonedaEvaluation C) (Y, G))
      (map (yonedaPairing C) f ≫
        Iso.hom
          ((fun (x : Cᵒᵖ × Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
              (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
                obj (yonedaPairing C) x ≅ obj (yonedaEvaluation C) x))
            (Y, G)))
      (Iso.hom
          ((fun (x : Cᵒᵖ × Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
              (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
                obj (yonedaPairing C) x ≅ obj (yonedaEvaluation C) x))
            (X, F)) ≫
        map (yonedaEvaluation C) f)
⊢ ∀ {Y : Cᵒᵖ × Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)} (f : (X, F) ⟶ Y),
    Eq (α := obj (yonedaPairing C) (X, F) ⟶ obj (yonedaEvaluation C) Y)
      (map (yonedaPairing C) f ≫
        Iso.hom
          ((fun (x : Cᵒᵖ × Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
              (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
                obj (yonedaPairing C) x ≅ obj (yonedaEvaluation C) x))
            Y))
      (Iso.hom
          ((fun (x : Cᵒᵖ × Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
              (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
                obj (yonedaPairing C) x ≅ obj (yonedaEvaluation C) x))
            (X, F)) ≫
        map (yonedaEvaluation C) f)

Tactic:
(Y, G)