-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ 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 })))
have 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
Tactic: ext Y x