-- 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
Y : Cᵒᵖ
f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y
w :
  ∀ (f : Functor.obj (Functor.obj yoneda X) Y),
    TypeCat.Fun.toFun (X := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y)
        (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))
        ((equivShrink (Functor.obj (Functor.obj yoneda X) Y) :
            (a : (yoneda.obj X).obj Y) → Shrink.{w, v} ((yoneda.obj X).obj Y))
          f) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app Y)).toFun
        ((equivShrink (Functor.obj (Functor.obj yoneda X) Y) :
            (a : (yoneda.obj X).obj Y) → Shrink.{w, v} ((yoneda.obj X).obj Y))
          f)
⊢ 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

Tactic:
obtain ⟨f, rfl⟩ := (equivShrink _).surjective f

Premises used: Equiv.surjective, equivShrink, rfl