-- 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) ∧
    ∀
      (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)
have 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 sorry }),
    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 sorry :
              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 sorry :
              PreZeroHypercover (↑f.domain : Scheme) }
            i))
      x
Tactic: refine ⟨fun x ↦ ?_, inferInstance⟩