-- Lean 4 proof step from Mathlib.CategoryTheory.ShrinkYoneda (goal)
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
⊢ 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
have 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 := sorry } :
                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)
Tactic: obtain ⟨f, rfl⟩ := (equivShrink _).surjective f
Cleared hypotheses: f