-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X₁ X₂ : C
f : X₁ ⟶ X₂
u : F.Elements
g : obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c)))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app (map shrinkYoneda.{w, v₁, u₁} f) (op (u.fst (β := fun (c : C) ↦ F.obj c))) ≫
          ↾fun
              (t : obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₂) (op (u.fst (β := fun (c : C) ↦ F.obj c)))) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (F.map
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X₂).obj (op u.fst)) → u.fst ⟶ X₂)
                      t)) :
                (a : F.obj u.fst) → F.obj X₂)
              (u.snd (β := fun (c : C) ↦ F.obj c))))
      g =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun
              (t : obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c)))) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (F.map
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst)) → u.fst ⟶ X₁)
                      t)) :
                (a : F.obj u.fst) → F.obj X₁)
              (u.snd (β := fun (c : C) ↦ F.obj c))) ≫
          F.map f))
      g
have h : ∀ (g : unop (op (u.fst (β := fun (c : C) ↦ F.obj c))) ⟶ X₁),
  TypeCat.Fun.toFun (X :=
      obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c))))
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app (map shrinkYoneda.{w, v₁, u₁} f) (op (u.fst (β := fun (c : C) ↦ F.obj c))) ≫
          ↾fun
              (t : obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₂) (op (u.fst (β := fun (c : C) ↦ F.obj c)))) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (F.map
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X₂).obj (op u.fst)) → u.fst ⟶ X₂)
                      t)) :
                (a : F.obj u.fst) → F.obj X₂)
              (u.snd (β := fun (c : C) ↦ F.obj c))))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop (op u.fst) ⟶ X₁) → (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst))
        g) =
    TypeCat.Fun.toFun (X :=
      obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c))))
      (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun
                (t :
                  obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c)))) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (F.map
                      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst)) → u.fst ⟶ X₁)
                        t)) :
                  (a : F.obj u.fst) → F.obj X₁)
                (u.snd (β := fun (c : C) ↦ F.obj c))) ≫
            F.map f) :
        TypeCat.Fun (obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c))))
          (F.obj X₂))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop (op u.fst) ⟶ X₁) → (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst))
          g :
        obj.{v₁, w, u₁, w + 1} (obj shrinkYoneda.{w, v₁, u₁} X₁) (op (u.fst (β := fun (c : C) ↦ F.obj c))))
Tactic: obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g
Cleared hypotheses: g