-- 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
⊢ (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))))
        τ) =
    τ
have 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 := 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))
      f =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app Y)).toFun f
Tactic: ext Y f