-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem toBasicOpen_surjective (f : R) : Function.Surjective (toBasicOpen R f)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j
s_eq :
  ∀ i ∈ t,
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s =
      const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
hn : f ^ n * f ∈ Ideal.span (h '' ↑t)
⊢ ∃ a, (toBasicOpen R f) a = s

Tactic:
rw [← pow_succ, Ideal.span, Finsupp.mem_span_image_iff_linearCombination] at hn

Result:
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j
s_eq :
  ∀ i ∈ t,
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s =
      const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
hn : ∃ l ∈ Finsupp.supported R R ↑t, (Finsupp.linearCombination R h) l = f ^ (n + 1)
⊢ ∃ a, (toBasicOpen R f) a = s

Proof state:
case h.hcover.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j
s_eq :
  ∀ i ∈ t,
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s =
      const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
i : ι
i_mem : i ∈ ↑t
x_mem : x ∈ ↑(PrimeSpectrum.basicOpen (h i))
⊢ ∃ i, x ∈ PrimeSpectrum.basicOpen (h ↑i)

Tactic:
exact ⟨⟨i, i_mem⟩, x_mem⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j
s_eq :
  ∀ i ∈ t,
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s =
      const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
ht_cover : PrimeSpectrum.zeroLocus (h '' ↑t) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))

Tactic:
apply PrimeSpectrum.vanishingIdeal_anti_mono ht_cover

Result:
case a
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j
s_eq :
  ∀ i ∈ t,
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s =
      const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
ht_cover : PrimeSpectrum.zeroLocus (h '' ↑t) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus {f})

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j
s_eq :
  ∀ i ∈ t,
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s =
      const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)
⊢ ∃ a, (toBasicOpen R f) a = s

Tactic:
use
  IsLocalization.mk' (Localization.Away f) (∑ i ∈ t, b i * a i)
    (⟨f ^ (n + 1), n + 1, rfl⟩ : Submonoid.powers _)

Result:
case h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j
s_eq :
  ∀ i ∈ t,
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s =
      const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)
⊢ (toBasicOpen R f) (IsLocalization.mk' (Localization.Away f) (∑ i ∈ t, b i * a i) ⟨f ^ (n + 1), ⋯⟩) = s

Proof state:
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
a' h' : ↥(PrimeSpectrum.basicOpen f) → R
iDh' : (x : ↥(PrimeSpectrum.basicOpen f)) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : ↥(PrimeSpectrum.basicOpen f)),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh' x).op)) s
x : PrimeSpectrum R
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
⊢ ∃ i, x ∈ ↑(PrimeSpectrum.basicOpen (h' i))

Tactic:
exact ⟨⟨x, hx⟩, hxDh' ⟨x, hx⟩⟩

Result:
no goals

Proof state:
case intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
a' h' : ↥(PrimeSpectrum.basicOpen f) → R
iDh' : (x : ↥(PrimeSpectrum.basicOpen f)) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : ↥(PrimeSpectrum.basicOpen f)),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh' x).op)) s
t : Finset ι
ht_cover' : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h' i))
⊢ ∃ a, (toBasicOpen R f) a = s

Tactic:
simp only [← Opens.coe_iSup, SetLike.coe_subset_coe] at ht_cover'

Result:
case intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
a' h' : ↥(PrimeSpectrum.basicOpen f) → R
iDh' : (x : ↥(PrimeSpectrum.basicOpen f)) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : ↥(PrimeSpectrum.basicOpen f)),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh' x).op)) s
t : Finset ι
ht_cover' : PrimeSpectrum.basicOpen f ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i)
⊢ ∃ a, (toBasicOpen R f) a = s