-- 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ᵒᵖ
X : Cᵒᵖ
x : ULift.{w, v₁} (unop X ⟶ unop ((unop j).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
φ : unop j ⟶
  P.elementsMk X
    ((hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((Equiv.symm uliftYonedaEquiv :
                (a : P.obj (op (unop (unop j).1))) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).1) ⟶ P)
              ((unop j).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
            X) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).1)).obj X)) →
          (fun (X : Type (max v₁ w)) ↦ X) (P.obj X))
      x) :=
  Subtype.mk (p :=
    fun
      (f :
        (unop j).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c) ⟶
          (P.elementsMk X
                ((hom (FC := TypeCat.Fun)
                      (NatTrans.app
                        ((Equiv.symm uliftYonedaEquiv :
                            (a : P.obj (op (unop (unop j).1))) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).1) ⟶ P)
                          ((unop j).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
                        X) :
                    (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).1)).obj X)) →
                      (fun (X : Type (max v₁ w)) ↦ X) (P.obj X))
                  x)).fst
            (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ↦
    (hom (FC := TypeCat.Fun) (P.map f) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj (unop j).fst)) →
            (fun (X : Type (max v₁ w)) ↦ X)
              (P.obj
                (P.elementsMk X
                    ((hom
                          (((uliftYonedaEquiv.symm :
                                  (a : P.obj (op (unop (unop j).1))) →
                                    uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).1) ⟶ P)
                                (unop j).snd).app
                            X) :
                        (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).1)).obj X)) →
                          (fun (X : Type (max v₁ w)) ↦ X) (P.obj X))
                      x)).fst))
        ((unop j).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) =
      (P.elementsMk X
            ((hom (FC := TypeCat.Fun)
                  (NatTrans.app
                    ((Equiv.symm uliftYonedaEquiv :
                        (a : P.obj (op (unop (unop j).1))) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).1) ⟶ P)
                      ((unop j).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
                    X) :
                (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).1)).obj X)) →
                  (fun (X : Type (max v₁ w)) ↦ X) (P.obj X))
              x)).snd
        (β := fun (c : Cᵒᵖ) ↦ P.obj c))
    (Quiver.Hom.op x.down) ⋯
this :
  Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop X) ⟶ s.pt) (Functor.map uliftYoneda.{w, v₁, u₁} x.down ≫ s.ι.app j)
    (s.ι.app
      (op
        (P.elementsMk X
          (((@hom _ types TypeCat.Fun _ _ _ _ _
                  (NatTrans.app
                    ((Equiv.symm uliftYonedaEquiv :
                        (a : P.obj (unop j).1) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).1) ⟶ P)
                      ((unop j).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
                    X) :
                TypeCat.Fun (ULift.{w, v₁} (unop X ⟶ unop (unop j).1)) (P.obj X)) :
              (a : ULift.{w, v₁} (unop X ⟶ unop (unop j).1)) → P.obj X)
            x))))
⊢ Eq (α := 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
              (((@hom _ types TypeCat.Fun _ _ _ _ _
                      (NatTrans.app
                        ((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)))
                        X) :
                    TypeCat.Fun (ULift.{w, v₁} (unop X ⟶ unop ((unop j).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                      (P.obj X)) :
                  (a : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)) → P.obj X)
                x)))) :
      s.pt.obj X)
    ((hom (FC := TypeCat.Fun) ((s.ι.app j).app X) : (a : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)) → s.pt.obj X) x :
      s.pt.obj X)
have w : Eq (α := s.pt.obj X)
  (((@hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app (Functor.map uliftYoneda.{w, v₁, u₁} x.down ≫ s.ι.app j) (op (unop X))) :
          TypeCat.Fun (ULift.{w, v₁} (unop X ⟶ unop X)) (s.pt.obj (op (unop X)))) :
        (a : ULift.{w, v₁} (unop X ⟶ unop X)) → s.pt.obj (op (unop X)))
      { down := 𝟙 (unop X) } :
    s.pt.obj (op (unop X)))
  ((hom (FC := TypeCat.Fun) ((s.ι.app j).app X) : (a : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)) → s.pt.obj X) x :
    s.pt.obj X)
Tactic: rw [← this, uliftYonedaEquiv_apply]