-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
τ : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P
w :
  ∀ (Y : Cᵒᵖ) (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (x : P.obj (op X)) ↦
                ({
                    app := fun (Y : Cᵒᵖ) ↦
                      ↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ↦
                        (ConcreteCategory.hom (FC := TypeCat.Fun)
                              (P.map
                                (Quiver.Hom.op
                                  ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Y)) :
                                      (a : Shrink.{w, v} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
                                    f))) :
                            (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
                          x,
                    naturality := ⋯ } :
                  NatTrans (Functor.obj shrinkYoneda.{w, v, u} X) P))
              ((fun (τ : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P) ↦
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op X)) :
                        (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op X))) →
                          (fun (X : Type w) ↦ X) (P.obj (op X)))
                      ((equivShrink (Functor.obj (Functor.obj yoneda X) (op X)) :
                            (a : (yoneda.obj X).obj (op X)) → Shrink.{w, v} ((yoneda.obj X).obj (op X)))
                          (𝟙 X) :
                        Shrink.{w, v} (Functor.obj (Functor.obj yoneda X) (op X))) :
                    (fun (X : Type w) ↦ X) (P.obj (op X))))
                τ))
            Y))
        f =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app Y)).toFun f
⊢ (fun (x : P.obj (op X)) ↦
        ({
            app := fun (Y : Cᵒᵖ) ↦
              ↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun)
                      (P.map
                        (Quiver.Hom.op
                          ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Y)) :
                              (a : Shrink.{w, v} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
                            f))) :
                    (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
                  x,
            naturality := ⋯ } :
          NatTrans (Functor.obj shrinkYoneda.{w, v, u} X) P))
      ((fun (τ : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op X)) :
                (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op X))) →
                  (fun (X : Type w) ↦ X) (P.obj (op X)))
              ((equivShrink (Functor.obj (Functor.obj yoneda X) (op X)) :
                    (a : (yoneda.obj X).obj (op X)) → Shrink.{w, v} ((yoneda.obj X).obj (op X)))
                  (𝟙 X) :
                Shrink.{w, v} (Functor.obj (Functor.obj yoneda X) (op X))) :
            (fun (X : Type w) ↦ X) (P.obj (op X))))
        τ) =
    τ

Tactic:
ext Y f