awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsDense
Y Z : D
f : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Z
c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
  { pt := Z,
    ι :=
      {
        app := fun (g : CostructuredArrow F Y) ↦
          ULift.down.{w, v₂}
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op g.left)) :
                (a : (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Y).obj (op g.left))) →
                  (fun (X : Type (max v₂ w)) ↦ X) (((restrictedULiftYoneda F).obj Z).obj (op g.left)))
              { down := g.hom }),
        naturality := ⋯ } }
X : C
x : obj (obj yoneda Y) (F.op.obj (op X))
this :
  Eq (α := F.obj X ⟶ Z)
    ((𝟙 (F.obj X) ≫ x) ≫
        (F.denseAt Y).desc
          { pt := Z,
            ι :=
              {
                app := fun (g : CostructuredArrow F Y) ↦
                  ULift.down.{w, v₂}
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op g.left)) :
                        (a : ((restrictedULiftYoneda F).obj Y).obj (op g.left)) →
                          ((restrictedULiftYoneda F).obj Z).obj (op g.left))
                      { down := g.hom }),
                naturality := ⋯ } } :
      F.obj X ⟶ Z)
    (ULift.down.{w, v₂}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
            (a : ((restrictedULiftYoneda F).obj Y).obj (op X)) → ((restrictedULiftYoneda F).obj Z).obj (op X))
          { down := x }) :
      F.obj X ⟶ Z)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map ((F.denseAt Y).desc c)).app (op X)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda Y) (F.op.obj (op X))) } =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda Y) (F.op.obj (op X))) }

Tactic:
simpa using ULift.down_injective this

Premises used: ULift.down_injective
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
X₁ X₂ : C
f : unop (op X₂) ⟶ unop (op X₁)
x : obj (obj yoneda Y) (F.op.obj (op X₁))
α : CostructuredArrow.mk (F.map f ≫ x) ⟶ CostructuredArrow.mk x := CostructuredArrow.homMk f ⋯
⊢ Eq (α := ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X₂))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).map (op f) ≫
          match (motive :=
            (x : Cᵒᵖ) →
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
            op X₂ with
          | op X =>
            ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
              match (motive :=
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                  ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
                x with
              | { down := x } =>
                { down := s.ι.app (CostructuredArrow.mk x) : ULift.{w, v₂} (obj (obj yoneda s.pt) (F.op.obj (op X))) }))
      { down := x : ULift.{w, v₂} (obj (obj yoneda Y) (F.op.obj (op X₁))) })
    (TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((match (motive :=
            (x : Cᵒᵖ) →
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
            op X₁ with
          | op X =>
            ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
              match (motive :=
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                  ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
                x with
              | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) }) ≫
          ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).map (op f)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda Y) (F.op.obj (op X₁))) })

Tactic:
ULift.down_injective (s.w α).symm

Premises used: CategoryTheory.Limits.Cocone.w, ULift.down_injective, Eq.symm
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
X₁ X₂ : C
f : unop (op X₂) ⟶ unop (op X₁)
x : obj (obj yoneda Y) (F.op.obj (op X₁))
α : CostructuredArrow.mk (F.map f ≫ x) ⟶ CostructuredArrow.mk x := CostructuredArrow.homMk f ⋯
⊢ Eq (α := ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X₂))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).map (op f) ≫
          match (motive :=
            (x : Cᵒᵖ) →
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
            op X₂ with
          | op X =>
            ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
              match (motive :=
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                  ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
                x with
              | { down := x } =>
                { down := s.ι.app (CostructuredArrow.mk x) : ULift.{w, v₂} (obj (obj yoneda s.pt) (F.op.obj (op X))) }))
      { down := x : ULift.{w, v₂} (obj (obj yoneda Y) (F.op.obj (op X₁))) })
    (TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((match (motive :=
            (x : Cᵒᵖ) →
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
            op X₁ with
          | op X =>
            ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
              match (motive :=
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                  ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
                x with
              | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) }) ≫
          ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).map (op f)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda Y) (F.op.obj (op X₁))) })

Tactic:
exact ULift.down_injective (s.w α).symm

Premises used: CategoryTheory.Limits.Cocone.w, ULift.down_injective, Eq.symm
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt :=
  fun (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) ↦
    {
      app := fun (x : Cᵒᵖ) ↦
        match (motive :=
          (x : Cᵒᵖ) →
            ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
          x with
        | op X =>
          ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
            match (motive :=
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
              x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
w :
  ∀ (X : C) (x : obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s).app (op X)))
        { down := x : ULift.{w, v₂} (obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))) } =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)).app (op X)))
        { down := x : ULift.{w, v₂} (obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))) }
⊢ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s =
    (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)

Tactic:
ext ⟨X⟩ ⟨x⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt :=
  fun (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) ↦
    {
      app := fun (x : Cᵒᵖ) ↦
        match (motive :=
          (x : Cᵒᵖ) →
            ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
          x with
        | op X =>
          ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
            match (motive :=
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
              x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
⊢ (CostructuredArrow.proj F Y ⋙ F).map α ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))

Tactic:
have := s.w α
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt :=
  fun (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) ↦
    {
      app := fun (x : Cᵒᵖ) ↦
        match (motive :=
          (x : Cᵒᵖ) →
            ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
          x with
        | op X =>
          ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
            match (motive :=
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
              x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
this : (CostructuredArrow.proj F Y ⋙ F).map α ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
w : { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) } = { down := x ≫ s.ι.app j : ULift.{w, v₂} (F.obj X ⟶ s.pt) }
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s).app (op X)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))) } =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)).app (op X)))
      { down := x : ULift.{w, v₂} (obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))) }

Tactic:
dsimp [uliftYoneda, φ, α] at this ⊢

Premises used: CategoryTheory.uliftYoneda
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt :=
  fun (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) ↦
    {
      app := fun (x : Cᵒᵖ) ↦
        match (motive :=
          (x : Cᵒᵖ) →
            ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
          x with
        | op X =>
          ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
            match (motive :=
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
              x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
this : F.map (F.preimage x) ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
w :
  ULift.down.{w, v₂} { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) } =
    ULift.down.{w, v₂} { down := x ≫ s.ι.app j : ULift.{w, v₂} (F.obj X ⟶ s.pt) }
⊢ { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) } = { down := x ≫ s.ι.app j : ULift.{w, v₂} (F.obj X ⟶ s.pt) }

Tactic:
apply ULift.down_injective

Premises used: ULift.down_injective
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt :=
  fun (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) ↦
    {
      app := fun (x : Cᵒᵖ) ↦
        match (motive :=
          (x : Cᵒᵖ) →
            ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
          x with
        | op X =>
          ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
            match (motive :=
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
              x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : obj (obj yoneda (F.obj j.left)) (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
this : F.map (F.preimage x) ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
⊢ ULift.down.{w, v₂} { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) } =
    ULift.down.{w, v₂} { down := x ≫ s.ι.app j : ULift.{w, v₂} (F.obj X ⟶ s.pt) }

Tactic:
simpa using this.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt :=
  fun (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) ↦
    {
      app := fun (x : Cᵒᵖ) ↦
        match (motive :=
          (x : Cᵒᵖ) →
            ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
          x with
        | op X =>
          ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
            match (motive :=
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
              x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
⊢ ∀ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) (j : CostructuredArrow F Y),
    (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s =
      (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)

Tactic:
have hφ (s) (j) : (restrictedULiftYoneda F).map j.hom ≫ φ s =
        (restrictedULiftYoneda F).map (s.ι.app j) := by
      ext ⟨X⟩ ⟨x⟩
      let α : .mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x)
      have := s.w α
      dsimp [uliftYoneda, φ, α] at this ⊢
      apply ULift.down_injective
      simpa using this.symm
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt :=
  fun (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) ↦
    {
      app := fun (x : Cᵒᵖ) ↦
        match (motive :=
          (x : Cᵒᵖ) →
            ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
          x with
        | op X =>
          ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
            match (motive :=
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
              x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
hφ :
  ∀ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) (j : CostructuredArrow F Y),
    (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s =
      (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
⊢ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map
      (((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).ι.app j ≫ h.preimage (φ s)) =
    (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)

Tactic:
simp [hφ]
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
h : (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y ⟶ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt :=
  fun (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) ↦
    {
      app := fun (x : Cᵒᵖ) ↦
        match (motive :=
          (x : Cᵒᵖ) →
            ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj x ⟶
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj x)
          x with
        | op X =>
          ↾fun (x : ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X)) ↦
            match (motive :=
              ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj Y).obj (op X) →
                ((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).obj s.pt).obj (op X))
              x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
hφ :
  ∀ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) (j : CostructuredArrow F Y),
    (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map j.hom ≫ φ s =
      (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (s.ι.app j)
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
m : ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).pt ⟶ s.pt
hm : ∀ (j : CostructuredArrow F Y), ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).ι.app j ≫ m = s.ι.app j
w :
  ∀ (unop : C)
    (down : obj (obj yoneda ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).pt) (F.op.obj (op unop))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map m).app (op unop)))
        { down := down :
          ULift.{w, v₂}
            (obj (obj yoneda ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).pt) (F.op.obj (op unop))) } =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (h.preimage (φ s))).app (op unop)))
        { down := down :
          ULift.{w, v₂}
            (obj (obj yoneda ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).pt) (F.op.obj (op unop))) }
⊢ (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map m =
    (restrictedULiftYoneda.{w, v₁, v₂, u₁, u₂} F).map (h.preimage (φ s))

Tactic:
ext ⟨_⟩ ⟨_⟩