-- 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 : ℰ
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)
w :
  ∀ (X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P),
    NatTrans.app
        ((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)))
          ((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)))
            f))
        X =
      f.app X
⊢ (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)))
      ((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)))
        f) =
    f

Tactic:
ext X