-- 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)
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
e : CostructuredArrow.mk (Y := X.left)
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X.left)) → uliftYoneda.{max w v₂, v₁, u₁}.obj X.left ⟶ P)
      ((hom (FC := TypeCat.Fun) (X.hom.app (op X.left)) :
          (a : (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((uliftYoneda.{max w v₂, v₁, u₁}.obj X.left).obj (op X.left))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj (op X.left)))
        { down := 𝟙 X.left })) ≅
  X :=
  CostructuredArrow.isoMk
    (Iso.refl
      (CostructuredArrow.left (D := Cᵒᵖ ⥤ Type (max (max w v₂) v₁)) (S :=
        (uliftYoneda.{max w v₂, v₁, u₁} : C ⥤ Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (T := P)
        (CostructuredArrow.mk (Y := X.left)
            ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X.left)) → uliftYoneda.{max w v₂, v₁, u₁}.obj X.left ⟶ P)
              ((hom (FC := TypeCat.Fun) (X.hom.app (op X.left)) :
                  (a :
                      (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                        ((uliftYoneda.{max w v₂, v₁, u₁}.obj X.left).obj (op X.left))) →
                    (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj (op X.left)))
                { down := 𝟙 X.left })) :
          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

Tactic:
simpa [e] using f.naturality e.inv

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv