-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
x : ↥(↑f.domain : Scheme)
⊢ ∃ (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
have 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 sorry :
          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)
          (sorry.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))
          sorry)))
    ⇑(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 sorry }
        (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)
          (sorry.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))
          sorry)))
  x
Tactic: use ⟨_, (TopologicalSpace.Opens.mem_sSup.mp x.2).choose_spec.1⟩