-- Module: Mathlib.CategoryTheory.Sites.Point.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
S : Sieve.{v, u} X
hS :
  ∀ (Φ : ObjectProperty.FullSubcategory (C := Point.{w, v, u} (C := C) ⊥) (pointsBot C))
    (x : Φ.obj (P := pointsBot C).fiber.obj X),
    ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := pointsBot C).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsBot C).fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
Y : C
a : Y ⟶ X
ha : S.arrows a
b :
  Functor.obj.{v, w, u, w + 1}
    (Point.fiber
      (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
        (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
    Y
hb :
  Eq (α :=
    (fun (X : Type w) ↦ X)
      (Functor.obj.{v, w, u, w + 1}
        (Point.fiber
          (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
            (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
        X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map
              (Point.fiber
                (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
                  (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
              a) :
          (a : (fun (X : Type w) ↦ X) ({ obj := pointBot X, property := ⋯ }.obj.fiber.obj Y)) →
            (fun (X : Type w) ↦ X) ({ obj := pointBot X, property := ⋯ }.obj.fiber.obj X))
        b :
      (fun (X : Type w) ↦ X)
        (Functor.obj.{v, w, u, w + 1}
          (Point.fiber
            (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
              (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
          X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (𝟙 X) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
obtain :
  ∀ (b : unop (op X) ⟶ Y)
    (hb :
      Eq (α :=
        (fun (X : Type w) ↦ X)
          (Functor.obj.{v, w, u, w + 1}
            (Point.fiber
              (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
                (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
            X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Functor.map
                  (Point.fiber
                    (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
                      (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
                  a) :
              (a : (fun (X : Type w) ↦ X) ({ obj := pointBot X, property := ⋯ }.obj.fiber.obj Y)) →
                (fun (X : Type w) ↦ X) ({ obj := pointBot X, property := ⋯ }.obj.fiber.obj X))
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X))
                b :
              Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
          (fun (X : Type w) ↦ X)
            (Functor.obj.{v, w, u, w + 1}
              (Point.fiber
                (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
                  (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) ⋯)))
              X))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
            (𝟙 X) :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))),
    S ∈ (⊥ : (a : C) → Set (Sieve a)) X
⊢ S ∈ (⊥ : (a : C) → Set (Sieve a)) X

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

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