-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
x : ↥(↑f.domain : Scheme)
h :
  Membership.mem (γ := Set ↥(↑f.domain : Scheme))
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := (↑f.domain : Scheme))
          { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
            X := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              X.homOfLE ⋯ :
            PreZeroHypercover (↑f.domain : Scheme) }
          (Subtype.mk (p := fun (x : X.Opens) ↦
            Membership.mem (γ := Set X.Opens)
              {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} x)
            (⋯.choose (p := fun (u : TopologicalSpace.Opens ↥X) ↦
              Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
                  {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} u ∧
                (↑x : ↥X) ∈ u))
            ⋯)))
      ⇑(PreZeroHypercover.f
          { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
            X := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              X.homOfLE ⋯ }
          (Subtype.mk (p := fun (x : X.Opens) ↦
            Membership.mem (γ := Set X.Opens)
              {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} x)
            (⋯.choose (p := fun (u : TopologicalSpace.Opens ↥X) ↦
              Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
                  {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} u ∧
                (↑x : ↥X) ∈ u))
            ⋯)))
    x
⊢ ∃ (i :
    PreZeroHypercover.I₀ (C := Scheme) (S := (↑f.domain : Scheme))
      { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
        X := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
          (↑(↑U : X.Opens) : Scheme),
        f := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
          X.homOfLE ⋯ }),
    Membership.mem (γ := Set ↥(↑f.domain : Scheme))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
              X :=
                fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
                (↑(↑U : X.Opens) : Scheme),
              f :=
                fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
                X.homOfLE ⋯ :
              PreZeroHypercover (↑f.domain : Scheme) }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
              X :=
                fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
                (↑(↑U : X.Opens) : Scheme),
              f :=
                fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
                X.homOfLE ⋯ :
              PreZeroHypercover (↑f.domain : Scheme) }
            i))
      x

Tactic:
use ⟨_, (TopologicalSpace.Opens.mem_sSup.mp x.2).choose_spec.1⟩