-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
w :
  ∀ (X : Cᵒᵖ) (x : P.obj X),
    TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun
                  (f :
                    Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
                      (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
                      (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)) ↦
                ({
                    app := fun (x : Cᵒᵖ) ↦
                      ↾fun (x_1 : P.obj x) ↦
                        {
                          down :=
                            f.app
                              (CostructuredArrow.mk (Y := unop x)
                                ((Equiv.symm uliftYonedaEquiv :
                                    (a : P.obj (op (unop x))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x) ⟶ P)
                                  x_1)) :
                          ULift.{max v₁ w, v₂} (Functor.obj (Functor.obj yoneda E) (A.op.obj x)) },
                    naturality := ⋯ } :
                  NatTrans P ((restrictedULiftYoneda A).obj E)))
              ((fun (g : P ⟶ (restrictedULiftYoneda A).obj E) ↦
                  ({
                      app := fun (y : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P) ↦
                        ULift.down
                          ((uliftYonedaEquiv :
                              (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
                                ((restrictedULiftYoneda A).obj E).obj (op y.left))
                            (y.hom ≫ g)),
                      naturality := ⋯ } :
                    NatTrans (C := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
                      (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
                      (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)))
                g))
            X))
        x =
      (hom (FC := TypeCat.Fun) (g.app X)).toFun x
⊢ (fun
          (f :
            Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
              (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
              (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)) ↦
        ({
            app := fun (x : Cᵒᵖ) ↦
              ↾fun (x_1 : P.obj x) ↦
                {
                  down :=
                    f.app
                      (CostructuredArrow.mk (Y := unop x)
                        ((Equiv.symm uliftYonedaEquiv :
                            (a : P.obj (op (unop x))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x) ⟶ P)
                          x_1)) },
            naturality := ⋯ } :
          NatTrans P ((restrictedULiftYoneda A).obj E)))
      ((fun (g : P ⟶ (restrictedULiftYoneda A).obj E) ↦
          ({
              app := fun (y : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P) ↦
                ULift.down
                  ((uliftYonedaEquiv :
                      (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
                        ((restrictedULiftYoneda A).obj E).obj (op y.left))
                    (y.hom ≫ g)),
              naturality := ⋯ } :
            NatTrans (C := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
              (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
              (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)))
        g) =
    g

Tactic:
ext X x