R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
R : Type u
inst✝ : CommRing R
f : R
⊢ Function.Surjective ↑(toBasicOpen R f)
intro s
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
⊢ ∃ a, ↑(toBasicOpen R f) a = s
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
let ι : Type u := PrimeSpectrum.basicOpen f
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
⊢ ∃ a, ↑(toBasicOpen R f) a = s
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
⊢ ∃ a, ↑(toBasicOpen R f) a = s
choose a' h' iDh' hxDh' s_eq' using locally_const_basicOpen R (PrimeSpectrum.basicOpen f) s
case intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
t : Finset ι
ht_cover' : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h' i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
⊢ ∃ a, ↑(toBasicOpen R f) a = s
obtain ⟨t, ht_cover'⟩ :=
  (PrimeSpectrum.isCompact_basicOpen f).elim_finite_subcover
    (fun i : ι => PrimeSpectrum.basicOpen (h' i)) (fun i => PrimeSpectrum.isOpen_basicOpen)
    fun x hx => by rw [Set.mem_iUnion]; exact ⟨⟨x, hx⟩, hxDh' ⟨x, hx⟩⟩
case intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
t : Finset ι
ht_cover' :
  PrimeSpectrum.basicOpen f ≤ ⨆ (i : { x // x ∈ PrimeSpectrum.basicOpen f }) (_ : i ∈ t), PrimeSpectrum.basicOpen (h' i)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
t : Finset ι
ht_cover' : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h' i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
simp only [← Opens.coe_iSup, SetLike.coe_subset_coe] at ht_cover'
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
t : Finset ι
ht_cover' :
  PrimeSpectrum.basicOpen f ≤ ⨆ (i : { x // x ∈ 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 : ι) (_ : i ∈ t), PrimeSpectrum.basicOpen (h i)
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
t : Finset ι
ht_cover' :
  PrimeSpectrum.basicOpen f ≤ ⨆ (i : { x // x ∈ PrimeSpectrum.basicOpen f }) (_ : i ∈ t), PrimeSpectrum.basicOpen (h' i)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
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'
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : PrimeSpectrum.basicOpen f ≤ ⨆ (i : ι) (_ : i ∈ t), PrimeSpectrum.basicOpen (h i)
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
t : Finset ι
ht_cover' :
  PrimeSpectrum.basicOpen f ≤ ⨆ (i : { x // x ∈ 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 : ι) (_ : i ∈ t), PrimeSpectrum.basicOpen (h i)
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
clear s_eq' iDh' hxDh' ht_cover' a' h'
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι), ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : PrimeSpectrum.basicOpen f ≤ ⨆ (i : ι) (_ : i ∈ t), PrimeSpectrum.basicOpen (h i)
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
rw [← SetLike.coe_subset_coe, Opens.coe_iSup] at ht_cover
case ht_cover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι), ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))

case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι), ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
replace ht_cover : (PrimeSpectrum.basicOpen f : Set <| PrimeSpectrum R) ⊆
  ⋃ (i : ι) (x : i ∈ t), (PrimeSpectrum.basicOpen (h i) : Set _)
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case ht_cover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι), ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))

case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
. convert ht_cover using 2
  exact funext fun j => by rw [Opens.coe_iSup]
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
hn : f ^ n ∈ Ideal.span (h '' ↑t)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ ∃ a, ↑(toBasicOpen R f) a = s
obtain ⟨n, hn⟩ : f ∈ (Ideal.span (h '' ↑t)).radical := by
  rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.zeroLocus_span]
  replace ht_cover : (PrimeSpectrum.zeroLocus {f})ᶜ ⊆
    ⋃ (i : ι) (x : i ∈ t), (PrimeSpectrum.zeroLocus {h i})ᶜ
  . convert ht_cover
    . rw [PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
    . simp only [Opens.iSup_mk, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
  rw [Set.compl_subset_comm] at ht_cover
  simp_rw [Set.compl_iUnion, compl_compl, ← PrimeSpectrum.zeroLocus_iUnion,
    ← Finset.set_biUnion_coe, ← Set.image_eq_iUnion] at ht_cover
  apply PrimeSpectrum.vanishingIdeal_anti_mono ht_cover
  exact PrimeSpectrum.subset_vanishingIdeal_zeroLocus {f} (Set.mem_singleton f)
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
hn : f * f ^ n ∈ Ideal.span (h '' ↑t)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
hn : f ^ n ∈ Ideal.span (h '' ↑t)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
replace hn := Ideal.mul_mem_left _ f hn
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
hn : ∃ l, l ∈ Finsupp.supported R R ↑t ∧ ↑(Finsupp.total ι R R h) l = f ^ (n + 1)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
hn : f * f ^ n ∈ Ideal.span (h '' ↑t)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
erw [← pow_succ, Finsupp.mem_span_image_iff_total] at hn
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ↑(Finsupp.total ι R R h) b = f ^ (n + 1)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
hn : ∃ l, l ∈ Finsupp.supported R R ↑t ∧ ↑(Finsupp.total ι R R h) l = f ^ (n + 1)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
rcases hn with ⟨b, b_supp, hb⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i • h i = f ^ (n + 1)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ↑(Finsupp.total ι R R h) b = f ^ (n + 1)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
rw [Finsupp.total_apply_of_mem_supported R b_supp] at hb
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i • h i = f ^ (n + 1)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
dsimp at hb
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
⊢ ↑(toBasicOpen R f)
      (IsLocalization.mk' (Localization.Away f) (∑ i in t, ↑b i * a i)
        { val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) }) =
    s
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
⊢ ∃ a, ↑(toBasicOpen R f) a = s
use
  IsLocalization.mk' (Localization.Away f) (∑ i : ι in t, b i * a i)
    (⟨f ^ (n + 1), n + 1, rfl⟩ : Submonoid.powers _)
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
⊢ const R (∑ i in t, ↑b i * a i)
      (↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) })
      (PrimeSpectrum.basicOpen f)
      (_ :
        ∀ (x : ↑(PrimeSpectrum.Top R)),
          x ∈ PrimeSpectrum.basicOpen f →
            ↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) } ∈
              Ideal.primeCompl x.asIdeal) =
    s
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
⊢ ↑(toBasicOpen R f)
      (IsLocalization.mk' (Localization.Away f) (∑ i in t, ↑b i * a i)
        { val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) }) =
    s
rw [toBasicOpen_mk']
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
⊢ const R (∑ i in t, ↑b i * a i)
      (↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) })
      (PrimeSpectrum.basicOpen f)
      (_ :
        ∀ (x : ↑(PrimeSpectrum.Top R)),
          x ∈ PrimeSpectrum.basicOpen f →
            ↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) } ∈
              Ideal.primeCompl x.asIdeal) =
    s
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
⊢ const R (∑ i in t, ↑b i * a i)
      (↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) })
      (PrimeSpectrum.basicOpen f)
      (_ :
        ∀ (x : ↑(PrimeSpectrum.Top R)),
          x ∈ PrimeSpectrum.basicOpen f →
            ↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) } ∈
              Ideal.primeCompl x.asIdeal) =
    s
let tt := ((t : Set (PrimeSpectrum.basicOpen f)) : Type u)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
⊢ PrimeSpectrum.basicOpen f ≤ ⨆ (i : tt), PrimeSpectrum.basicOpen (h ↑i)

case intro.intro.intro.intro.intro.intro.intro.intro.intro.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
⊢ ∀ (i : tt),
    (forget CommRingCat).map ((structureSheaf R).val.map (iDh ↑i).op)
        (const R (∑ i in t, ↑b i * a i)
          (↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) })
          (PrimeSpectrum.basicOpen f)
          (_ :
            ∀ (x : ↑(PrimeSpectrum.Top R)),
              x ∈ PrimeSpectrum.basicOpen f →
                ↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) } ∈
                  Ideal.primeCompl x.asIdeal)) =
      (forget CommRingCat).map ((structureSheaf R).val.map (iDh ↑i).op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
⊢ const R (∑ i in t, ↑b i * a i)
      (↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) })
      (PrimeSpectrum.basicOpen f)
      (_ :
        ∀ (x : ↑(PrimeSpectrum.Top R)),
          x ∈ PrimeSpectrum.basicOpen f →
            ↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) } ∈
              Ideal.primeCompl x.asIdeal) =
    s
apply
  (structureSheaf R).eq_of_locally_eq' (fun i : tt => PrimeSpectrum.basicOpen (h i))
    (PrimeSpectrum.basicOpen f) fun i : tt => iDh i
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ (forget CommRingCat).map ((structureSheaf R).val.map (iDh ↑{ val := i, property := hi }).op)
      (const R (∑ i in t, ↑b i * a i)
        (↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) })
        (PrimeSpectrum.basicOpen f)
        (_ :
          ∀ (x : ↑(PrimeSpectrum.Top R)),
            x ∈ PrimeSpectrum.basicOpen f →
              ↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) } ∈
                Ideal.primeCompl x.asIdeal)) =
    (forget CommRingCat).map ((structureSheaf R).val.map (iDh ↑{ val := i, property := hi }).op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
⊢ ∀ (i : tt),
    (forget CommRingCat).map ((structureSheaf R).val.map (iDh ↑i).op)
        (const R (∑ i in t, ↑b i * a i)
          (↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) })
          (PrimeSpectrum.basicOpen f)
          (_ :
            ∀ (x : ↑(PrimeSpectrum.Top R)),
              x ∈ PrimeSpectrum.basicOpen f →
                ↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) } ∈
                  Ideal.primeCompl x.asIdeal)) =
      (forget CommRingCat).map ((structureSheaf R).val.map (iDh ↑i).op) s
rintro ⟨i, hi⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ↑((structureSheaf R).val.map (iDh i).op)
      (const R (∑ i in t, ↑b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen f)
        (_ :
          ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen f → f ^ (n + 1) ∈ Ideal.primeCompl x.asIdeal)) =
    ↑((structureSheaf R).val.map (iDh i).op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ (forget CommRingCat).map ((structureSheaf R).val.map (iDh ↑{ val := i, property := hi }).op)
      (const R (∑ i in t, ↑b i * a i)
        (↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) })
        (PrimeSpectrum.basicOpen f)
        (_ :
          ∀ (x : ↑(PrimeSpectrum.Top R)),
            x ∈ PrimeSpectrum.basicOpen f →
              ↑{ val := f ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = f ^ (n + 1)) } ∈
                Ideal.primeCompl x.asIdeal)) =
    (forget CommRingCat).map ((structureSheaf R).val.map (iDh ↑{ val := i, property := hi }).op) s
dsimp
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ↑((structureSheaf R).val.map (iDh i).op)
      (const R (∑ i in t, ↑b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen f)
        (_ :
          ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen f → f ^ (n + 1) ∈ Ideal.primeCompl x.asIdeal)) =
    ↑((structureSheaf R).val.map (iDh i).op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ↑((structureSheaf R).val.map (iDh i).op)
      (const R (∑ i in t, ↑b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen f)
        (_ :
          ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen f → f ^ (n + 1) ∈ Ideal.primeCompl x.asIdeal)) =
    ↑((structureSheaf R).val.map (iDh i).op) s
change (structureSheaf R).1.map _ _ = (structureSheaf R).1.map _ _
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ const R (∑ i in t, ↑b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen (h i))
      ?intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv =
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
      (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))

case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen (h i) → f ^ (n + 1) ∈ Ideal.primeCompl x.asIdeal
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ↑((structureSheaf R).val.map (iDh i).op)
      (const R (∑ i in t, ↑b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen f)
        (_ :
          ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen f → f ^ (n + 1) ∈ Ideal.primeCompl x.asIdeal)) =
    ↑((structureSheaf R).val.map (iDh i).op) s
rw [s_eq i hi, res_const]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen (h i) → f ^ (n + 1) ∈ Ideal.primeCompl x.asIdeal

case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ const R (∑ i in t, ↑b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen (h i))
      ?intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv =
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
      (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ const R (∑ i in t, ↑b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen (h i))
      ?intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv =
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
      (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))

case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen (h i) → f ^ (n + 1) ∈ Ideal.primeCompl x.asIdeal
swap
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ (∑ i in t, ↑b i * a i) * h i = a i * f ^ (n + 1)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ const R (∑ i in t, ↑b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen (h i))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (f ^ (n + 1))) =
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
      (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
apply const_ext
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ∑ x in t, ↑b x * a x * h i = ∑ x in t, a i * (↑b x * h x)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ (∑ i in t, ↑b i * a i) * h i = a i * f ^ (n + 1)
rw [← hb, Finset.sum_mul, Finset.mul_sum]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), x ∈ t → ↑b x * a x * h i = a i * (↑b x * h x)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ∑ x in t, ↑b x * a x * h i = ∑ x in t, a i * (↑b x * h x)
apply Finset.sum_congr rfl
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
j : { x // x ∈ PrimeSpectrum.basicOpen f }
hj : j ∈ t
⊢ ↑b j * a j * h i = a i * (↑b j * h j)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), x ∈ t → ↑b x * a x * h i = a i * (↑b x * h x)
intro j hj
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
j : { x // x ∈ PrimeSpectrum.basicOpen f }
hj : j ∈ t
⊢ ↑b j * (h j * a i) = a i * (↑b j * h j)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
j : { x // x ∈ PrimeSpectrum.basicOpen f }
hj : j ∈ t
⊢ ↑b j * a j * h i = a i * (↑b j * h j)
rw [mul_assoc, ah_ha j hj i hi]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
j : { x // x ∈ PrimeSpectrum.basicOpen f }
hj : j ∈ t
⊢ ↑b j * (h j * a i) = a i * (↑b j * h j)
ring
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
x : PrimeSpectrum R
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
⊢ ∃ i, x ∈ (fun i => ↑(PrimeSpectrum.basicOpen (h' i))) i
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
x : PrimeSpectrum R
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
⊢ x ∈ ⋃ (i : ι), (fun i => ↑(PrimeSpectrum.basicOpen (h' i))) i
rw [Set.mem_iUnion]
no goals
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
a' h' : { x // x ∈ PrimeSpectrum.basicOpen f } → R
iDh' : (x : { x // x ∈ PrimeSpectrum.basicOpen f }) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f
hxDh' : ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }), ↑x ∈ PrimeSpectrum.basicOpen (h' x)
s_eq' :
  ∀ (x : { x // x ∈ PrimeSpectrum.basicOpen f }),
    const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x))
        (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h' x) → y ∈ PrimeSpectrum.basicOpen (h' x)) =
      ↑((structureSheaf R).val.map (iDh' x).op) s
x : PrimeSpectrum R
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
⊢ ∃ i, x ∈ (fun i => ↑(PrimeSpectrum.basicOpen (h' i))) i
exact ⟨⟨x, hx⟩, hxDh' ⟨x, hx⟩⟩
case h.e'_4.h.h.e'_3.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι), ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
e_1✝¹ : Set (PrimeSpectrum R) = Set ↑(PrimeSpectrum.Top R)
e_1✝ : PrimeSpectrum R = ↑(PrimeSpectrum.Top R)
⊢ (fun i => ⋃ (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))) = fun i => ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))
case ht_cover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι), ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
convert ht_cover using 2
no goals
case h.e'_4.h.h.e'_3.h
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι), ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
e_1✝¹ : Set (PrimeSpectrum R) = Set ↑(PrimeSpectrum.Top R)
e_1✝ : PrimeSpectrum R = ↑(PrimeSpectrum.Top R)
⊢ (fun i => ⋃ (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))) = fun i => ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))
exact funext fun j => by rw [Opens.coe_iSup]
no goals
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι), ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
e_1✝¹ : Set (PrimeSpectrum R) = Set ↑(PrimeSpectrum.Top R)
e_1✝ : PrimeSpectrum R = ↑(PrimeSpectrum.Top R)
j : ι
⊢ (⋃ (_ : j ∈ t), ↑(PrimeSpectrum.basicOpen (h j))) = ↑(⨆ (_ : j ∈ t), PrimeSpectrum.basicOpen (h j))
rw [Opens.coe_iSup]
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ f ∈ Ideal.radical (Ideal.span (h '' ↑t))
rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.zeroLocus_span]
case ht_cover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ PrimeSpectrum.zeroLocus {f}ᶜ ⊆ ⋃ (i : ι) (_ : i ∈ t), PrimeSpectrum.zeroLocus {h i}ᶜ

R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : PrimeSpectrum.zeroLocus {f}ᶜ ⊆ ⋃ (i : ι) (_ : i ∈ t), PrimeSpectrum.zeroLocus {h i}ᶜ
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))
replace ht_cover : (PrimeSpectrum.zeroLocus {f})ᶜ ⊆
  ⋃ (i : ι) (x : i ∈ t), (PrimeSpectrum.zeroLocus {h i})ᶜ
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : PrimeSpectrum.zeroLocus {f}ᶜ ⊆ ⋃ (i : ι) (_ : i ∈ t), PrimeSpectrum.zeroLocus {h i}ᶜ
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))
case ht_cover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ PrimeSpectrum.zeroLocus {f}ᶜ ⊆ ⋃ (i : ι) (_ : i ∈ t), PrimeSpectrum.zeroLocus {h i}ᶜ

R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : PrimeSpectrum.zeroLocus {f}ᶜ ⊆ ⋃ (i : ι) (_ : i ∈ t), PrimeSpectrum.zeroLocus {h i}ᶜ
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))
. convert ht_cover
  . rw [PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
  . simp only [Opens.iSup_mk, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : (⋃ (i : ι) (_ : i ∈ t), PrimeSpectrum.zeroLocus {h i}ᶜ)ᶜ ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : PrimeSpectrum.zeroLocus {f}ᶜ ⊆ ⋃ (i : ι) (_ : i ∈ t), PrimeSpectrum.zeroLocus {h i}ᶜ
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))
rw [Set.compl_subset_comm] at ht_cover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : PrimeSpectrum.zeroLocus ((fun i => h i) '' ↑t) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : (⋃ (i : ι) (_ : i ∈ t), PrimeSpectrum.zeroLocus {h i}ᶜ)ᶜ ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))
simp_rw [Set.compl_iUnion, compl_compl, ← PrimeSpectrum.zeroLocus_iUnion,
  ← Finset.set_biUnion_coe, ← Set.image_eq_iUnion] at ht_cover
case a
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : PrimeSpectrum.zeroLocus ((fun i => h i) '' ↑t) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus {f})
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : PrimeSpectrum.zeroLocus ((fun i => h i) '' ↑t) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (h '' ↑t))
apply PrimeSpectrum.vanishingIdeal_anti_mono ht_cover
no goals
case a
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : PrimeSpectrum.zeroLocus ((fun i => h i) '' ↑t) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus {f})
exact PrimeSpectrum.subset_vanishingIdeal_zeroLocus {f} (Set.mem_singleton f)
case h.e'_3
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ PrimeSpectrum.zeroLocus {f}ᶜ = ↑(PrimeSpectrum.basicOpen f)

case h.e'_4.h.e'_3.h.f
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ PrimeSpectrum.zeroLocus {h x✝¹}ᶜ = ↑(PrimeSpectrum.basicOpen (h x✝¹))
case ht_cover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ PrimeSpectrum.zeroLocus {f}ᶜ ⊆ ⋃ (i : ι) (_ : i ∈ t), PrimeSpectrum.zeroLocus {h i}ᶜ
convert ht_cover
case h.e'_4.h.e'_3.h.f
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ PrimeSpectrum.zeroLocus {h x✝¹}ᶜ = ↑(PrimeSpectrum.basicOpen (h x✝¹))
case h.e'_3
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ PrimeSpectrum.zeroLocus {f}ᶜ = ↑(PrimeSpectrum.basicOpen f)

case h.e'_4.h.e'_3.h.f
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ PrimeSpectrum.zeroLocus {h x✝¹}ᶜ = ↑(PrimeSpectrum.basicOpen (h x✝¹))
. rw [PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
no goals
case h.e'_4.h.e'_3.h.f
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ PrimeSpectrum.zeroLocus {h x✝¹}ᶜ = ↑(PrimeSpectrum.basicOpen (h x✝¹))
. simp only [Opens.iSup_mk, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
no goals
case h.e'_3
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ PrimeSpectrum.zeroLocus {f}ᶜ = ↑(PrimeSpectrum.basicOpen f)
rw [PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
no goals
case h.e'_4.h.e'_3.h.f
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ PrimeSpectrum.zeroLocus {h x✝¹}ᶜ = ↑(PrimeSpectrum.basicOpen (h x✝¹))
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
⊢ x ∈ ↑(⨆ (i : tt), PrimeSpectrum.basicOpen (h ↑i))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
⊢ PrimeSpectrum.basicOpen f ≤ ⨆ (i : tt), PrimeSpectrum.basicOpen (h ↑i)
intro x hx
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in 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)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
⊢ x ∈ ↑(⨆ (i : tt), PrimeSpectrum.basicOpen (h ↑i))
erw [TopologicalSpace.Opens.mem_iSup]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
this : x ∈ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ ∃ i, x ∈ PrimeSpectrum.basicOpen (h ↑i)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in 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)
have := ht_cover hx
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
this : ∃ i j, x ∈ ↑(PrimeSpectrum.basicOpen (h i))
⊢ ∃ i, x ∈ PrimeSpectrum.basicOpen (h ↑i)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
this : x ∈ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
⊢ ∃ i, x ∈ PrimeSpectrum.basicOpen (h ↑i)
rw [← Finset.set_biUnion_coe, Set.mem_iUnion₂] at this
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in 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)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ ↑(PrimeSpectrum.basicOpen f)
this : ∃ i j, x ∈ ↑(PrimeSpectrum.basicOpen (h i))
⊢ ∃ i, x ∈ PrimeSpectrum.basicOpen (h ↑i)
rcases this with ⟨i, i_mem, x_mem⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.hcover.intro.intro
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in 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)
refine ⟨⟨i, i_mem⟩, x_mem⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h i)
⊢ f ^ (n + 1) ∈ Ideal.primeCompl y.asIdeal
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
⊢ ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen (h i) → f ^ (n + 1) ∈ Ideal.primeCompl x.asIdeal
intro y hy
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h i)
⊢ y ∈ PrimeSpectrum.basicOpen (f ^ (n + 1))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h i)
⊢ f ^ (n + 1) ∈ Ideal.primeCompl y.asIdeal
change y ∈ PrimeSpectrum.basicOpen (f ^ (n + 1))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h i)
⊢ y ∈ PrimeSpectrum.basicOpen f
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h i)
⊢ y ∈ PrimeSpectrum.basicOpen (f ^ (n + 1))
rw [PrimeSpectrum.basicOpen_pow f (n + 1) (by linarith)]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h i)
⊢ y ∈ PrimeSpectrum.basicOpen f
exact (leOfHom (iDh i) : _) hy
no goals
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (PrimeSpectrum.basicOpen f).op)
ι : Type u := { x // x ∈ PrimeSpectrum.basicOpen f }
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → a i * h j = h i * a j
s_eq :
  ∀ (i : ι),
    i ∈ t →
      ↑((structureSheaf R).val.map (iDh i).op) s =
        const R (a i) (h i) (PrimeSpectrum.basicOpen (h i))
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h i) → y ∈ PrimeSpectrum.basicOpen (h i))
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i in t, ↑b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h i)
⊢ 0 < n + 1
linarith