-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : C
x : P.obj (op X)
⊢ Eq (α := (F.op ⋙ G.obj P).obj (op X))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj P) → (F.op ⋙ G.obj P).obj (op X))
        ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X)) → uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ P) x ≫
          presheafHom.{w, v₁, v₂, u₁, u₂} φ P) :
      (F.op ⋙ G.obj P).obj (op X))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              (G.map ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X)) → uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ P) x))
              (op (F.obj X))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op (F.obj X)))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
        ((hom (FC := TypeCat.Fun) ((φ.app X).app (op (F.obj X))) :
            (a :
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (op (F.obj X)))) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (op (F.obj X))))
          { down := 𝟙 (unop (op (F.obj X))) }) :
      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
have erw : Eq (α := (F.op ⋙ G.obj P).obj (op X))
  ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj P) → (F.op ⋙ G.obj P).obj (op X))
      (NatTrans.app
        (Cocone.ι
          {
            pt :=
              { obj := fun (X : Cᵒᵖ) ↦ (G.obj P).obj (F.op.obj X),
                map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) ↦ (G.obj P).map (F.op.map f), map_id := sorry, map_comp := sorry },
            ι := { app := fun (x : P.Elementsᵒᵖ) ↦ coconeApp.{w, v₁, v₂, u₁, u₂} φ (unop x), naturality := sorry } })
        (op (P.elementsMk (op X) x))) :
    (F.op ⋙ G.obj P).obj (op X))
  ((hom (FC := TypeCat.Fun)
          (NatTrans.app
            (G.map ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X)) → uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ P) x))
            (op (F.obj X))) :
        (a :
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
              ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op (F.obj X)))) →
          (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
      ((hom (FC := TypeCat.Fun) ((φ.app X).app (op (F.obj X))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (op (F.obj X)))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (op (F.obj X))))
        { down := 𝟙 (unop (op (F.obj X))) }) :
    (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
Tactic: erw [(colimitOfRepresentable P).fac _ (Opposite.op (P.elementsMk _ x))]