-- 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 ∈ Ideal.span (h '' ↑t)
⊢ ∃ a, (toBasicOpen R f) a = s

Tactic:
replace hn := Ideal.mul_mem_right f _ 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 : f ^ n * f ∈ Ideal.span (h '' ↑t)
⊢ ∃ a, (toBasicOpen R f) a = s

Proof state:
case h.h.mk.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)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
j : ι
hj : j ∈ t
⊢ b j * (h j * a i) = a i * (b j * h j)

Tactic:
ring

Result:
no goals

Proof state:
case h.h.mk.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)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ∑ i_1 ∈ t, b i_1 * a i_1 * h i = ∑ i_1 ∈ t, a i * (b i_1 * h i_1)

Tactic:
apply Finset.sum_congr rfl

Result:
case h.h.mk.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)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ∀ x ∈ t, b x * a x * h i = a i * (b x * h x)

Proof state:
case h.h.mk.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)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
j : ι
hj : j ∈ t
⊢ b j * a j * h i = a i * (b j * h j)

Tactic:
rw [mul_assoc, ah_ha j hj i hi]

Result:
case h.h.mk.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)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
j : ι
hj : j ∈ t
⊢ b j * (h j * a i) = a i * (b j * h j)

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:
obtain ⟨a, h, iDh, ht_cover, ah_ha, s_eq⟩ :=
  normalize_finite_fraction_representation R (PrimeSpectrum.basicOpen f)
    s t a' h' iDh' ht_cover' s_eq'

Result:
case 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)
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 h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : PrimeSpectrum.basicOpen f ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)
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)) ⋯
⊢ ∃ a, (toBasicOpen R f) a = s