-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Presheaf (goal)
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))
⊢ S ∈ (⊥ : (a : C) → Set (Sieve a)) X
have 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) sorry)))
          X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Functor.map
                (Point.fiber
                  (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
                    (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) sorry)))
                a) :
            (a : (fun (X : Type w) ↦ X) ({ obj := pointBot X, property := sorry }.obj.fiber.obj Y)) →
              (fun (X : Type w) ↦ X) ({ obj := pointBot X, property := sorry }.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) sorry)))
            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
Tactic: obtain ⟨b, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective b
Cleared hypotheses: b, hb