case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
obtain ⟨V, hxV : x.1 ∈ V.1, iVU, f, g, hVDg : V ≤ PrimeSpectrum.basicOpen g, s_eq⟩ :=
  exists_const R U s x.1 x.2
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
obtain ⟨_, ⟨h, rfl⟩, hxDh, hDhV : PrimeSpectrum.basicOpen h ≤ V⟩ :=
  PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open hxV V.2
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
hn : h ^ n ∈ Ideal.span {g}
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
cases' (PrimeSpectrum.basicOpen_le_basicOpen_iff h g).mp (Set.Subset.trans hDhV hVDg) with n hn
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
hn : h * h ^ n ∈ Ideal.span {g}
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
hn : h ^ n ∈ Ideal.span {g}
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
replace hn := Ideal.mul_mem_left (Ideal.span {g}) h hn
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
hn : ∃ a, a * g = h ^ (n + 1)
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
hn : h * h ^ n ∈ Ideal.span {g}
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
rw [← pow_succ, Ideal.mem_span_singleton'] at hn
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
hn : ∃ a, a * g = h ^ (n + 1)
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
cases' hn with c hc
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
have basic_opens_eq := PrimeSpectrum.basicOpen_pow h (n + 1) (by linarith)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
have i_basic_open := eqToHom basic_opens_eq ≫ homOfLE hDhV
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)),
          y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))) =
    ↑((structureSheaf R).val.map (i_basic_open ≫ iVU).op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g)
          (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen g → y ∈ PrimeSpectrum.basicOpen g) =
        ↑((structureSheaf R).val.map i.op) s
use f * c, h ^ (n + 1), i_basic_open ≫ iVU, (basic_opens_eq.symm.le : _) hxDh
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)),
          y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))) =
    ↑((structureSheaf R).val.map iVU.op ≫ (structureSheaf R).val.map i_basic_open.op) s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)),
          y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))) =
    ↑((structureSheaf R).val.map (i_basic_open ≫ iVU).op) s
rw [op_comp, Functor.map_comp]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)),
          y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))) =
    ↑((structureSheaf R).val.map i_basic_open.op) (↑((structureSheaf R).val.map iVU.op) s)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)),
          y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))) =
    ↑((structureSheaf R).val.map iVU.op ≫ (structureSheaf R).val.map i_basic_open.op) s
change const R _ _ _ _ = (structureSheaf R).1.map i_basic_open.op
  ((structureSheaf R).1.map iVU.op s)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)),
          y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))) =
    const R f g (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      ?intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → g ∈ Ideal.primeCompl x.asIdeal
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)),
          y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))) =
    ↑((structureSheaf R).val.map i_basic_open.op) (↑((structureSheaf R).val.map iVU.op) s)
rw [← s_eq, res_const]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → g ∈ Ideal.primeCompl x.asIdeal

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)),
          y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))) =
    const R f g (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      ?intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)),
          y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))) =
    const R f g (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      ?intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → g ∈ Ideal.primeCompl x.asIdeal
swap
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ f * c * g = f * h ^ (n + 1)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ :
        ∀ (y : ↑(PrimeSpectrum.Top R)),
          y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))) =
    const R f g (PrimeSpectrum.basicOpen (h ^ (n + 1)))
      (_ : ∀ (y : ↑(PrimeSpectrum.Top R)), y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → y ∈ ↑(PrimeSpectrum.basicOpen g))
apply const_ext
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ f * c * g = f * h ^ (n + 1)
rw [mul_assoc f c g, hc]
no goals
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
⊢ 0 < n + 1
linarith
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))
⊢ g ∈ Ideal.primeCompl y.asIdeal
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)) → g ∈ Ideal.primeCompl x.asIdeal
intro y hy
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen h
⊢ g ∈ Ideal.primeCompl y.asIdeal
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h ^ (n + 1))
⊢ g ∈ Ideal.primeCompl y.asIdeal
rw [basic_opens_eq] at hy
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
x : { x // x ∈ U }
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = ↑((structureSheaf R).val.map iVU.op) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen h
⊢ g ∈ Ideal.primeCompl y.asIdeal
exact (Set.Subset.trans hDhV hVDg : _) hy