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
X : C
F F' : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ F'
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')
have 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))
Tactic: apply yonedaEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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)))
    ((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)))
have 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)))
Tactic: rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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))
    ((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))
have 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))
Tactic: rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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))
⊢ 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))
have 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))
Tactic: rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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))
⊢ 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))
have 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))
Tactic: rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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
⊢ 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)
have 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)
Tactic: rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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)
⊢ 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)
have 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)
Tactic: rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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)
⊢ 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)
have rw₂ : map yoneda f.unop ≫ u = map yoneda f.unop ≫ u
Tactic: rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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
⊢ f = g
have 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
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
⊢ ∀ {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)
have 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)
Tactic: (Y, G)
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
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)
have h : ∀ (a : obj yoneda (unop X) ⟶ F),
  Eq (α := obj (yonedaEvaluation C) (Y, G))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (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))))
      a)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (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))
      a)
Tactic: ext (a : yoneda.obj X.unop ⟶ F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
Y : Cᵒᵖ
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : (X, F) ⟶ (Y, G)
a : obj yoneda (unop X) ⟶ F
⊢ Eq (α := obj (yonedaEvaluation C) (Y, G))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (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))))
      a)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (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))
      a)
have h : Eq.{v₁ + 1} (α := obj (evaluationUncurried Cᵒᵖ (Type v₁)) (Y, G))
  (ULift.down.{u₁, v₁}
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (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))))
      a))
  (ULift.down.{u₁, v₁}
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (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))
      a))
Tactic: apply ULift.ext