-- 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)
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 := ⋯, 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))))
⊢ 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))))

Tactic:
erw [(colimitOfRepresentable P).fac _ (Opposite.op (P.elementsMk _ x))]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.elementsMk, CategoryTheory.Presheaf.colimitOfRepresentable, Opposite.op