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

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff