-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
refine :
  ∀ (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
⊢ (∀ (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) ∧
    ∀
      (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 ⋯ }),
      IsOpenImmersion
        (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)

Tactic:
refine ⟨fun x ↦ ?_, inferInstance⟩