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

Proof state:
case h.h.mk
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
i : ι
hi : i ∈ ↑t
⊢ (ConcreteCategory.hom ((structureSheaf R).val.map (iDh ↑⟨i, hi⟩).op))
      (const R (∑ i ∈ t, b i * a i) (↑⟨f ^ (n + 1), ⋯⟩) (PrimeSpectrum.basicOpen f) ⋯) =
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh ↑⟨i, hi⟩).op)) s

Tactic:
dsimp

Result:
case h.h.mk
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
i : ι
hi : i ∈ ↑t
⊢ (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op))
      (const R (∑ i ∈ t, b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen f) ⋯) =
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) 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)
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))
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))

Tactic:
simp [PrimeSpectrum.basicOpen_eq_zeroLocus_compl] at ht_cover

Result:
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 {f})ᶜ ⊆ ⋃ i ∈ t, (PrimeSpectrum.zeroLocus {h i})ᶜ
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))

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 : (Finsupp.linearCombination R h) b = f ^ (n + 1)
⊢ ∃ a, (toBasicOpen R f) a = s

Tactic:
rw [Finsupp.linearCombination_apply_of_mem_supported R b_supp] at hb

Result:
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

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, (toBasicOpen R f) a = s

Tactic:
choose a' h' iDh' hxDh' s_eq' using locally_const_basicOpen R (PrimeSpectrum.basicOpen f) s

Result:
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
⊢ ∃ a, (toBasicOpen R f) a = s

Proof state:
case h.hcover
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)
⊢ x ∈ ↑(⨆ i, PrimeSpectrum.basicOpen (h ↑i))

Tactic:
rw [SetLike.mem_coe, TopologicalSpace.Opens.mem_iSup]

Result:
case h.hcover
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, x ∈ PrimeSpectrum.basicOpen (h ↑i)

Proof state:
R : Type u
inst✝ : CommRing R
f : R
⊢ Function.Surjective ⇑(toBasicOpen R f)

Tactic:
intro s

Result:
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
⊢ ∃ a, (toBasicOpen R f) a = s