-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst_2 : LocallySmall.{w, v, u} C
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
i : ι
a :
  obj
    (comp (D := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i))
      (obj (evaluation Cᵒᵖ (Type w)) (op V)))
    { as := i : Discrete ι }
hw :
  Eq (α := (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i)) (op V)) :
          (a : (fun (X : Type w) ↦ X) (c.pt.obj (op V))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation Cᵒᵖ (Type w)) (op V)) c))
                  { as := i : Discrete ι }) :
              (a :
                  (fun (X : Type w) ↦ X)
                    (((Discrete.functor fun (i : ι) ↦ shrinkYoneda.{w, v, u}.obj (X i)) ⋙
                          (evaluation Cᵒᵖ (Type w)).obj (op V)).obj
                      { as := i })) →
                (fun (X : Type w) ↦ X)
                  (((const (Discrete ι)).obj (((evaluation Cᵒᵖ (Type w)).obj (op V)).mapCocone c).pt).obj { as := i }))
            a :
          (fun (X : Type w) ↦ X)
            (obj
              (obj (const (Discrete ι))
                (Cocone.pt (F :=
                  comp (D := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
                    (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i))
                    (obj (evaluation Cᵒᵖ (Type w)) (op V)))
                  (mapCocone (obj (evaluation Cᵒᵖ (Type w)) (op V)) c)))
              { as := i : Discrete ι })) :
      (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj shrinkYoneda.{w, v, u} S) v.op) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op U))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g :
          obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op U)) :
      (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))
h :
  ∀ (a : V ⟶ X i)
    (hw :
      Eq (α := (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i)) (op V)) :
              (a : (fun (X : Type w) ↦ X) (c.pt.obj (op V))) →
                (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation Cᵒᵖ (Type w)) (op V)) c))
                      { as := i : Discrete ι }) :
                  (a :
                      (fun (X : Type w) ↦ X)
                        (((Discrete.functor fun (i : ι) ↦ shrinkYoneda.{w, v, u}.obj (X i)) ⋙
                              (evaluation Cᵒᵖ (Type w)).obj (op V)).obj
                          { as := i })) →
                    (fun (X : Type w) ↦ X)
                      (((const (Discrete ι)).obj (((evaluation Cᵒᵖ (Type w)).obj (op V)).mapCocone c).pt).obj
                        { as := i }))
                ((Equiv.symm shrinkYonedaObjObjEquiv :
                      (a : unop (op V) ⟶ X { as := i }.as) → (shrinkYoneda.{w, v, u}.obj (X { as := i }.as)).obj (op V))
                    a :
                  obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} (X { as := i : Discrete ι }.as)) (op V)) :
              (fun (X : Type w) ↦ X)
                (obj
                  (obj (const (Discrete ι))
                    (Cocone.pt (F :=
                      comp (D := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
                        (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i))
                        (obj (evaluation Cᵒᵖ (Type w)) (op V)))
                      (mapCocone (obj (evaluation Cᵒᵖ (Type w)) (op V)) c)))
                  { as := i : Discrete ι })) :
          (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj shrinkYoneda.{w, v, u} S) v.op) :
              (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op U))) →
                (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj S).obj (op V)))
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : U ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) g :
              obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op U)) :
          (fun (X : Type w) ↦ X) (obj.{v, w, u, w + 1} (obj shrinkYoneda.{w, v, u} S) (op V)))),
    ∃ (Y : C) (h : V ⟶ Y) (g_1 : Y ⟶ S), Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g
⊢ ∃ (Y : C) (h : V ⟶ Y) (g_1 : Y ⟶ S), Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g

Tactic:
obtain ⟨a : V ⟶ X i, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective a

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