-- 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
w :
  ∀ (Y : Cᵒᵖ)
    (x :
      Functor.obj
        (Functor.obj uliftYoneda.{max w v₂, v₁, u₁}
          (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)))
        Y),
    (hom (FC := TypeCat.Fun)
            ((Functor.map uliftYoneda.{max w v₂, v₁, u₁}
                    (Iso.hom
                      (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 :
                                    ULift.{max v₂ w, v₁} (Functor.obj (Functor.obj yoneda X.left) (op X.left)) })) :
                            CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)))) ≫
                  X.hom).app
              Y)).toFun
        x =
      TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (NatTrans.app
            (CostructuredArrow.hom
              (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 :
                      ULift.{max v₂ w, v₁} (Functor.obj (Functor.obj yoneda X.left) (op X.left)) }))))
            Y))
        x
⊢ Functor.map uliftYoneda.{max w v₂, v₁, u₁}
        (Iso.hom
          (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 :
                        ULift.{max v₂ w, v₁} (Functor.obj (Functor.obj yoneda X.left) (op X.left)) })) :
                CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)))) ≫
      X.hom =
    CostructuredArrow.hom
      (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 })))

Tactic:
ext Y x