-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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)
dsimp :
  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 : (F.op ⋙ G.obj P).obj (op X)) → uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj P)
          ((hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (G.map
                    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X)) → uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P) x))
                  (F.op.obj (op X))) :
              (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (F.op.obj (op X))) →
                (G.obj P).obj (F.op.obj (op X)))
            ((hom (FC := TypeCat.Fun) ((φ.app X).app (F.op.obj (op X))) :
                (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (F.op.obj (op X))) →
                  ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X)))
              { down := 𝟙 (unop (F.op.obj (op 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 : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op (F.obj X))) → (G.obj P).obj (op (F.obj X)))
        ((hom (FC := TypeCat.Fun) ((φ.app X).app (op (F.obj X))) :
            (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (op (F.obj X))) →
              ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (op (F.obj X)))
          { down := 𝟙 (F.obj X) }) :
      (G.obj P).obj (op (F.obj 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))
        (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 := ⋯, map_comp := ⋯ },
              ι := { app := fun (x : P.Elementsᵒᵖ) ↦ coconeApp.{w, v₁, v₂, u₁, u₂} φ (unop x), naturality := ⋯ } })
          (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:
dsimp only [coconeApp]

Premises used: CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp