-- 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
⊢ Membership.mem (γ := Set (Presieve (↑f.domain : Scheme)))
    ((precoverage IsOpenImmersion).coverings (↑f.domain : Scheme))
    (PreZeroHypercover.presieve₀
      { 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 ⋯ })
have rw : (∀ (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) ∧
  ∀
    (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 }),
    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 sorry :
          PreZeroHypercover (↑f.domain : Scheme) }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]