-- 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_1 x_2 : Cᵒᵖ
g : x_1 ⟶ x_2
x : P.obj x_1
φ : Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
  (CostructuredArrow.mk (Y := unop x_2)
      ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop x_2))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x_2) ⟶ P)
        ((hom (FC := TypeCat.Fun) (P.map g) :
            (a : (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj x_1)) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj x_2))
          x)) :
    CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
  (CostructuredArrow.mk (Y := unop x_1)
      ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop x_1))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P)
        x) :
    CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P) :=
  CostructuredArrow.homMk g.unop ⋯
h :
  Eq (α := A.obj (unop x_2) ⟶ E)
    (f.app
        (CostructuredArrow.mk (Y := unop x_2)
          ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_2) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_2) ⟶ P)
            ((hom (FC := TypeCat.Fun) (P.map g) : (a : P.obj x_1) → P.obj x_2) x))) :
      Functor.obj (C := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
          (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
          (CostructuredArrow.mk (Y := unop x_2)
            ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_2) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_2) ⟶ P)
              ((hom (FC := TypeCat.Fun) (P.map g) : (a : P.obj x_1) → P.obj x_2) x))) ⟶
        Functor.obj (C := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
          (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E :
            CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
          (CostructuredArrow.mk (Y := unop x_2)
              ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_2) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_2) ⟶ P)
                ((hom (FC := TypeCat.Fun) (P.map g) : (a : P.obj x_1) → P.obj x_2) x)) :
            CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P))
    (A.map g.unop ≫
      f.app
        (CostructuredArrow.mk (Y := unop x_1)
          ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_1) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P) x)))
⊢ Eq (α := ((restrictedULiftYoneda A).obj E).obj x_2)
    ({
        down :=
          f.app
            (CostructuredArrow.mk (Y := unop x_2)
              ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_2) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_2) ⟶ P)
                ((hom (FC := TypeCat.Fun) (P.map g) : (a : P.obj x_1) → P.obj x_2) x))) } :
      ULift.{max v₁ w, v₂} (A.obj (unop x_2) ⟶ E))
    ({
        down :=
          A.map g.unop ≫
            f.app
              (CostructuredArrow.mk (Y := unop x_1)
                ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_1) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P)
                  x)) } :
      ULift.{max v₁ w, v₂} (A.obj (unop x_2) ⟶ E))

Tactic:
congr 1