-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Dense (goal)
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₁)
⊢ 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))
have 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₁))) })
Tactic: ext ⟨x⟩