-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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)))
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))))
⊢ 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

Tactic:
obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv, Equiv.surjective, Equiv.symm, rfl