-- 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 : ((functorToRepresentables.{w, v₁, u₁} P).obj j).obj X
φ : 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 :
  (functorToRepresentables.{w, v₁, u₁} P).map φ.op ≫ s.ι.app (op (unop j)) =
    s.ι.app
      (op
        (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)))
⊢ 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
have w : 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)
Tactic: dsimp [φ] at this x ⊢