-- 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₁)
h₁ :
  ∀ (x : obj (obj yoneda Y) (F.op.obj (op X₁))),
    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₁))) })
⊢ Eq (α :=
    ((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₂))
    (((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) })
    ((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))

Tactic:
ext ⟨x⟩