awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
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
⊢ ((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

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
⊢ (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)))

Tactic:
have := s.w (Quiver.Hom.op (CategoryOfElements.homMk (P.elementsMk X x)
          (P.elementsMk Y (P.map f x)) f rfl))
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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)))
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)
⊢ 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:
dsimp at this x ⊢
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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))))
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)
⊢ 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:
rw [← this, uliftYonedaEquiv_comp]

Premises used: CategoryTheory.uliftYonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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))))
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)
        ((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)
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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))))
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)
⊢ 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)

Tactic:
rw [uliftYonedaEquiv_apply, uliftYonedaEquiv_apply,
          ← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.uliftYonedaEquiv_apply
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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)
        (((@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:
simp [uliftYoneda]

Premises used: CategoryTheory.uliftYoneda
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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ᵒᵖ
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 := ⋯ : NatTrans (coconeOfRepresentable P).pt s.pt })
            X))
        x =
      (hom (FC := TypeCat.Fun) ((s.ι.app j).app X)).toFun x
⊢ (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

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
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 := ⋯ : NatTrans (coconeOfRepresentable P).pt s.pt }
            X))
        x
⊢ 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 := ⋯ }

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
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)
⊢ (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

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 ⊢

Premises used: CategoryTheory.Presheaf.coconeOfRepresentable_pt, CategoryTheory.Functor.leftOp_obj, Opposite.op_unop, TypeCat.Fun.coe_mk, CategoryTheory.Presheaf.functorToRepresentables_obj, TypeCat.Fun.toFun_apply, CategoryTheory.CategoryOfElements.π_obj, CategoryTheory.Presheaf.coconeOfRepresentable_ι_app, CategoryTheory.Functor.const_obj_obj, CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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)
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))))
w₂ 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))))
        ((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))))
⊢ 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:
rw [← hm, uliftYonedaEquiv_comp, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.uliftYonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : HasColimitsOfSize.{v₁, max w u₁ v₁ v₂, v₂, u₂} ℰ
⊢ Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
⊢ IsIso α

Tactic:
(Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α).isIso_hom

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isIso_hom, CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
mp :
  L.IsLeftKanExtension α →
    IsIso α ∧
      PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
          max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
        L
mpr :
  IsIso α ∧
      PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
          max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
        L →
    L.IsLeftKanExtension α
⊢ L.IsLeftKanExtension α ↔
    IsIso α ∧
      PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
          max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
        L

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
h : L.IsLeftKanExtension α
⊢ IsIso α ∧
    PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L

Tactic:
⟨inferInstance, preservesColimits_of_natIso (Functor.leftKanExtensionUnique _
      (uliftYoneda.{max w v₂}.leftKanExtensionUnit A) _ α)⟩

Premises used: inferInstance, CategoryTheory.Functor.leftKanExtensionUnit, CategoryTheory.Functor.leftKanExtensionUnique, And.intro, CategoryTheory.Limits.preservesColimits_of_natIso, CategoryTheory.uliftYoneda
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
h : L.IsLeftKanExtension α
⊢ IsIso α ∧
    PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L

Tactic:
exact ⟨inferInstance, preservesColimits_of_natIso (Functor.leftKanExtensionUnique _
      (uliftYoneda.{max w v₂}.leftKanExtensionUnit A) _ α)⟩