awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
rw :
  Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    (Functor.map uliftYoneda.{w, v₁, u₁} (↑f.unop : (unop x₂).fst ⟶ (unop x₁).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₂).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₂).fst) ⟶ P)
        ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
      ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
⊢ Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    (Functor.map uliftYoneda.{w, v₁, u₁} (↑f.unop : (unop x₂).fst ⟶ (unop x₁).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₂).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₂).fst) ⟶ P)
        ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
        ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
      𝟙 P)
have rw₁ : Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
  ((Equiv.symm uliftYonedaEquiv :
        (a : P.obj (op (unop (unop x₁).fst))) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
      ((hom (FC := TypeCat.Fun) (P.map (↑f.unop : (unop x₂).fst ⟶ (unop x₁).fst)) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj (unop x₂).fst)) →
            (fun (X : Type (max v₁ w)) ↦ X) (P.obj (unop x₁).fst))
        ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) :
    Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
  ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
      ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) :
    Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
Tactic: rw [comp_id, ← uliftYonedaEquiv_symm_map, f.unop.2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
rw :
  Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    (Functor.map uliftYoneda.{w, v₁, u₁} (↑f.unop : (unop x₂).fst ⟶ (unop x₁).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₂).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₂).fst) ⟶ P)
        ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
      ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
rw₁ :
  Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    ((Equiv.symm uliftYonedaEquiv :
          (a : P.obj (op (unop (unop x₁).fst))) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
        ((hom (FC := TypeCat.Fun) (P.map (↑f.unop : (unop x₂).fst ⟶ (unop x₁).fst)) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj (unop x₂).fst)) →
              (fun (X : Type (max v₁ w)) ↦ X) (P.obj (unop x₁).fst))
          ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) :
      Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
        ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) :
      Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
⊢ Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    (Functor.map uliftYoneda.{w, v₁, u₁} (↑f.unop : (unop x₂).fst ⟶ (unop x₁).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₂).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₂).fst) ⟶ P)
        ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
        ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
      𝟙 P)
have rw₂ : Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
  ((Equiv.symm uliftYonedaEquiv :
        (a : P.obj (op (unop (unop x₁).fst))) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
      ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) :
    Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
  ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
      ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) :
    Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
Tactic: rw [comp_id, ← uliftYonedaEquiv_symm_map, f.unop.2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ P₂ : Cᵒᵖ ⥤ Type (max w v₁)
α : P₁ ⟶ P₂
j : P₁.Elementsᵒᵖ
⊢ (coconeOfRepresentable P₁).ι.app j ≫ α = (coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)
have w : ∀ (T : Cᵒᵖ) (f : ((functorToRepresentables.{w, v₁, u₁} P₁).obj j).obj T),
  (hom (FC := TypeCat.Fun) (((coconeOfRepresentable P₁).ι.app j ≫ α).app T)).toFun f =
    TypeCat.Fun.toFun
      (@hom _ types TypeCat.Fun _ _ _ _ _
        (NatTrans.app ((coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)) T))
      f
Tactic: ext T f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ((coconeOfRepresentable P).pt.map f ≫
      ↾fun (x : (coconeOfRepresentable P).pt.obj Y) ↦
        (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ s.pt) → s.pt.obj (op (unop Y)))
          (s.ι.app (op (P.elementsMk Y x)))) =
    (↾fun (x : (coconeOfRepresentable P).pt.obj X) ↦
        (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj (op (unop X)))
          (s.ι.app (op (P.elementsMk X x)))) ≫
      s.pt.map f
have h : ∀ (x : (coconeOfRepresentable P).pt.obj X),
  TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((coconeOfRepresentable P).pt.map f ≫
          ↾fun (x : (coconeOfRepresentable P).pt.obj Y) ↦
            (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ s.pt) → s.pt.obj (op (unop Y)))
              (s.ι.app (op (P.elementsMk Y x)))))
      x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((↾fun (x : (coconeOfRepresentable P).pt.obj X) ↦
            (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj (op (unop X)))
              (s.ι.app (op (P.elementsMk X x)))) ≫
          s.pt.map f))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (coconeOfRepresentable P).pt.obj X
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((coconeOfRepresentable P).pt.map f ≫
          ↾fun (x : (coconeOfRepresentable P).pt.obj Y) ↦
            (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ s.pt) → s.pt.obj (op (unop Y)))
              (s.ι.app (op (P.elementsMk Y x)))))
      x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((↾fun (x : (coconeOfRepresentable P).pt.obj X) ↦
            (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj (op (unop X)))
              (s.ι.app (op (P.elementsMk X x)))) ≫
          s.pt.map f))
      x
have this : (functorToRepresentables.{w, v₁, u₁} P).map
      (Quiver.Hom.op
        (CategoryOfElements.homMk (P.elementsMk X x)
          (P.elementsMk Y
            ((hom (FC := TypeCat.Fun) (P.map f) :
                (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (P.obj Y))
              x))
          f sorry)) ≫
    s.ι.app (op (P.elementsMk X x)) =
  s.ι.app
    (op
      (P.elementsMk Y
        ((hom (FC := TypeCat.Fun) (P.map f) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (P.obj Y))
          x)))
Tactic: have := s.w (Quiver.Hom.op (CategoryOfElements.homMk (P.elementsMk X x)
          (P.elementsMk Y (P.map f x)) f rfl))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (coconeOfRepresentable P).pt.obj X
this :
  (functorToRepresentables.{w, v₁, u₁} P).map
        (Quiver.Hom.op
          (CategoryOfElements.homMk (P.elementsMk X x)
            (P.elementsMk Y
              ((hom (FC := TypeCat.Fun) (P.map f) :
                  (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (P.obj Y))
                x))
            f ⋯)) ≫
      s.ι.app (op (P.elementsMk X x)) =
    s.ι.app
      (op
        (P.elementsMk Y
          ((hom (FC := TypeCat.Fun) (P.map f) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (P.obj Y))
            x)))
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((coconeOfRepresentable P).pt.map f ≫
          ↾fun (x : (coconeOfRepresentable P).pt.obj Y) ↦
            (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ s.pt) → s.pt.obj (op (unop Y)))
              (s.ι.app (op (P.elementsMk Y x)))))
      x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((↾fun (x : (coconeOfRepresentable P).pt.obj X) ↦
            (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj (op (unop X)))
              (s.ι.app (op (P.elementsMk X x)))) ≫
          s.pt.map f))
      x
have h : Eq (α := s.pt.obj Y)
  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ s.pt) → s.pt.obj Y)
      (s.ι.app (op (P.elementsMk Y ((hom (FC := TypeCat.Fun) (P.map f) : (a : P.obj X) → P.obj Y) x)))) :
    s.pt.obj Y)
  ((hom (FC := TypeCat.Fun) (s.pt.map f) : (a : s.pt.obj X) → s.pt.obj Y)
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
        (s.ι.app (op (P.elementsMk X x)))) :
    s.pt.obj Y)
Tactic: dsimp at this x ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ s.pt)
    (Functor.map uliftYoneda.{w, v₁, u₁} f.unop ≫ s.ι.app (op (P.elementsMk X x)))
    (s.ι.app (op (P.elementsMk Y ((hom (FC := TypeCat.Fun) (P.map f) : (a : P.obj X) → P.obj Y) x))))
⊢ Eq (α := s.pt.obj Y)
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ s.pt) → s.pt.obj Y)
        (s.ι.app (op (P.elementsMk Y ((hom (FC := TypeCat.Fun) (P.map f) : (a : P.obj X) → P.obj Y) x)))) :
      s.pt.obj Y)
    ((hom (FC := TypeCat.Fun) (s.pt.map f) : (a : s.pt.obj X) → s.pt.obj Y)
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
          (s.ι.app (op (P.elementsMk X x)))) :
      s.pt.obj Y)
have h : Eq (α := s.pt.obj Y)
  (((@hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (s.ι.app (op (P.elementsMk X x))) (op (unop Y))) :
          TypeCat.Fun (Functor.obj (Functor.obj uliftYoneda.{w, v₁, u₁} (unop X)) (op (unop Y)))
            (s.pt.obj (op (unop Y)))) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj (unop X)).obj (op (unop Y)))) →
          (fun (X : Type (max v₁ w)) ↦ X) (s.pt.obj (op (unop Y))))
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ uliftYoneda.{w, v₁, u₁}.obj (unop X)) →
            (uliftYoneda.{w, v₁, u₁}.obj (unop X)).obj (op (unop Y)))
        (Functor.map uliftYoneda.{w, v₁, u₁} f.unop)) :
    (fun (X : Type (max v₁ w)) ↦ X) (s.pt.obj (op (unop Y))))
  ((hom (FC := TypeCat.Fun) (s.pt.map f) : (a : s.pt.obj X) → s.pt.obj Y)
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
        (s.ι.app (op (P.elementsMk X x)))) :
    s.pt.obj Y)
Tactic: rw [← this, uliftYonedaEquiv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ s.pt)
    (Functor.map uliftYoneda.{w, v₁, u₁} f.unop ≫ s.ι.app (op (P.elementsMk X x)))
    (s.ι.app (op (P.elementsMk Y ((hom (FC := TypeCat.Fun) (P.map f) : (a : P.obj X) → P.obj Y) x))))
⊢ Eq (α := s.pt.obj Y)
    (((@hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (s.ι.app (op (P.elementsMk X x))) Y) :
            TypeCat.Fun (ULift.{w, v₁} (unop Y ⟶ unop X)) (s.pt.obj Y)) :
          (a : ULift.{w, v₁} (unop Y ⟶ unop X)) → s.pt.obj Y)
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ uliftYoneda.{w, v₁, u₁}.obj (unop X)) →
              ULift.{w, v₁} (unop Y ⟶ unop X))
          (Functor.map uliftYoneda.{w, v₁, u₁} f.unop)) :
      s.pt.obj Y)
    ((hom (FC := TypeCat.Fun) (s.pt.map f) : (a : s.pt.obj X) → s.pt.obj Y)
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
          (s.ι.app (op (P.elementsMk X x)))) :
      s.pt.obj Y)
have h : Eq (α := s.pt.obj Y)
  (((@hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (s.ι.app (op (P.elementsMk X x))) Y) :
          TypeCat.Fun (ULift.{w, v₁} (unop Y ⟶ unop X)) (s.pt.obj Y)) :
        (a : ULift.{w, v₁} (unop Y ⟶ unop X)) → s.pt.obj Y)
      (((@hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (Functor.map uliftYoneda.{w, v₁, u₁} f.unop) (op (unop Y))) :
            TypeCat.Fun (ULift.{w, v₁} (unop Y ⟶ unop Y))
              (Functor.obj (Functor.obj uliftYoneda.{w, v₁, u₁} (unop X)) (op (unop Y)))) :
          (a : ULift.{w, v₁} (unop Y ⟶ unop Y)) → (uliftYoneda.{w, v₁, u₁}.obj (unop X)).obj (op (unop Y)))
        { down := 𝟙 (unop Y) }) :
    s.pt.obj Y)
  (((@hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (s.ι.app (op (P.elementsMk X x))) Y) :
          TypeCat.Fun (Functor.obj (Functor.obj uliftYoneda.{w, v₁, u₁} (unop X)) Y) (s.pt.obj Y)) :
        (a : (uliftYoneda.{w, v₁, u₁}.obj (unop X)).obj Y) → s.pt.obj Y)
      ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj uliftYoneda.{w, v₁, u₁} (unop X)) f) :
          (a : (uliftYoneda.{w, v₁, u₁}.obj (unop X)).obj X) → (uliftYoneda.{w, v₁, u₁}.obj (unop X)).obj Y)
        { down := 𝟙 (unop X) }) :
    s.pt.obj Y)
Tactic: rw [uliftYonedaEquiv_apply, uliftYonedaEquiv_apply,
          ← NatTrans.naturality_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
j : P.Elementsᵒᵖ
⊢ (coconeOfRepresentable P).ι.app j ≫
      {
        app := fun (X : Cᵒᵖ) ↦
          ↾fun (x : (coconeOfRepresentable P).pt.obj X) ↦
            (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj (op (unop X)))
              (s.ι.app (op (P.elementsMk X x))),
        naturality := ⋯ } =
    s.ι.app j
have w : ∀ (X : Cᵒᵖ) (x : ((functorToRepresentables.{w, v₁, u₁} P).obj j).obj X),
  TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((coconeOfRepresentable P).ι.app j ≫
            {
              app := fun (X : Cᵒᵖ) ↦
                ↾fun (x : (coconeOfRepresentable P).pt.obj X) ↦
                  (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj (op (unop X)))
                    (s.ι.app (op (P.elementsMk X x))),
              naturality := sorry : NatTrans (coconeOfRepresentable P).pt s.pt })
          X))
      x =
    (hom (FC := TypeCat.Fun) ((s.ι.app j).app X)).toFun x
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm : ∀ (j : P.Elementsᵒᵖ), (coconeOfRepresentable P).ι.app j ≫ m = s.ι.app j
⊢ m =
    {
      app := fun (X : Cᵒᵖ) ↦
        ↾fun (x : (coconeOfRepresentable P).pt.obj X) ↦
          (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj (op (unop X)))
            (s.ι.app (op (P.elementsMk X x))),
      naturality := ⋯ }
have w : ∀ (X : Cᵒᵖ) (x : (coconeOfRepresentable P).pt.obj X),
  (hom (FC := TypeCat.Fun) (m.app X)).toFun x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (NatTrans.app
          {
            app := fun (X : Cᵒᵖ) ↦
              ↾fun (x : (coconeOfRepresentable P).pt.obj X) ↦
                (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj (op (unop X)))
                  (s.ι.app (op (P.elementsMk X x))),
            naturality := sorry : NatTrans (coconeOfRepresentable P).pt s.pt }
          X))
      x
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm : ∀ (j : P.Elementsᵒᵖ), (coconeOfRepresentable P).ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
x : (coconeOfRepresentable P).pt.obj X
⊢ (hom (FC := TypeCat.Fun) (m.app X)).toFun x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (NatTrans.app
          {
            app := fun (X : Cᵒᵖ) ↦
              ↾fun (x : (coconeOfRepresentable P).pt.obj X) ↦
                (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj (op (unop X)))
                  (s.ι.app (op (P.elementsMk X x))),
            naturality := ⋯ : NatTrans (coconeOfRepresentable P).pt s.pt }
          X))
      x
have w : Eq (α := s.pt.obj X) ((hom (FC := TypeCat.Fun) (m.app X) : (a : P.obj X) → s.pt.obj X) x : s.pt.obj X)
  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
      (s.ι.app (op (P.elementsMk X x))) :
    s.pt.obj X)
Tactic: simp only [functorToRepresentables_obj, coconeOfRepresentable_pt, Functor.const_obj_obj,
      coconeOfRepresentable_ι_app, Functor.leftOp_obj, CategoryOfElements.π_obj, op_unop,
      TypeCat.Fun.toFun_apply, hom_ofHom, TypeCat.Fun.coe_mk] at hm ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm :
  ∀ (j : P.Elementsᵒᵖ),
    (Equiv.symm uliftYonedaEquiv : (a : P.obj (unop j).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).fst) ⟶ P)
          ((unop j).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
        m =
      s.ι.app j
X : Cᵒᵖ
x : (coconeOfRepresentable P).pt.obj X
⊢ Eq (α := s.pt.obj X) ((hom (FC := TypeCat.Fun) (m.app X) : (a : P.obj X) → s.pt.obj X) x : s.pt.obj X)
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
        (s.ι.app (op (P.elementsMk X x))) :
      s.pt.obj X)
have w : Eq (α := s.pt.obj X) ((hom (FC := TypeCat.Fun) (m.app X) : (a : P.obj X) → s.pt.obj X) x : s.pt.obj X)
  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
      ((Equiv.symm uliftYonedaEquiv :
            (a : P.obj (unop (op (P.elementsMk X x))).fst) →
              uliftYoneda.{w, v₁, u₁}.obj (unop (unop (op (P.elementsMk X x))).fst) ⟶ P)
          ((unop (op (P.elementsMk X x))).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
        m) :
    s.pt.obj X)
Tactic: rw [← hm, uliftYonedaEquiv_comp, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm :
  ∀ (j : P.Elementsᵒᵖ),
    (Equiv.symm uliftYonedaEquiv : (a : P.obj (unop j).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).fst) ⟶ P)
          ((unop j).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
        m =
      s.ι.app j
X : Cᵒᵖ
x : (coconeOfRepresentable P).pt.obj X
w :
  Eq (α := s.pt.obj X) ((hom (FC := TypeCat.Fun) (m.app X) : (a : P.obj X) → s.pt.obj X) x : s.pt.obj X)
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
        ((Equiv.symm uliftYonedaEquiv :
              (a : P.obj (unop (op (P.elementsMk X x))).fst) →
                uliftYoneda.{w, v₁, u₁}.obj (unop (unop (op (P.elementsMk X x))).fst) ⟶ P)
            ((unop (op (P.elementsMk X x))).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
          m) :
      s.pt.obj X)
⊢ Eq (α := s.pt.obj X) ((hom (FC := TypeCat.Fun) (m.app X) : (a : P.obj X) → s.pt.obj X) x : s.pt.obj X)
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
        (s.ι.app (op (P.elementsMk X x))) :
      s.pt.obj X)
have w₁ : Eq (α := s.pt.obj X) ((hom (FC := TypeCat.Fun) (m.app X) : (a : P.obj X) → s.pt.obj X) x : s.pt.obj X)
  ((hom (FC := TypeCat.Fun) (m.app (op (unop X))) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj (op (unop X)))) →
          (fun (X : Type (max v₁ w)) ↦ X) (s.pt.obj (op (unop X))))
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ P) → P.obj (op (unop X)))
        ((Equiv.symm uliftYonedaEquiv :
            (a : P.obj (unop (op (P.elementsMk X x))).fst) →
              uliftYoneda.{w, v₁, u₁}.obj (unop (unop (op (P.elementsMk X x))).fst) ⟶ P)
          ((unop (op (P.elementsMk X x))).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))) :
    (fun (X : Type (max v₁ w)) ↦ X) (s.pt.obj (op (unop X))))
Tactic: rw [← hm, uliftYonedaEquiv_comp, Equiv.apply_symm_apply]