R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
⊢ ∀ (x : PrimeSpectrum R), ¬x ∈ zeroLocus s
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
⊢ zeroLocus s = ∅
rw [Set.eq_empty_iff_forall_not_mem]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : x ∈ zeroLocus s
⊢ False
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
⊢ ∀ (x : PrimeSpectrum R), ¬x ∈ zeroLocus s
intro x hx
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ False
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : x ∈ zeroLocus s
⊢ False
rw [mem_zeroLocus] at hx
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
⊢ False
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ False
have x_prime : x.asIdeal.IsPrime := by infer_instance
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
eq_top : x.asIdeal = ⊤
⊢ False
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
⊢ False
have eq_top : x.asIdeal = ⊤ := by
  rw [Ideal.eq_top_iff_one]
  exact hx h
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
eq_top : x.asIdeal = ⊤
⊢ False
apply x_prime.ne_top eq_top
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ Ideal.IsPrime x.asIdeal
infer_instance
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
⊢ 1 ∈ x.asIdeal
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
⊢ x.asIdeal = ⊤
rw [Ideal.eq_top_iff_one]
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
⊢ 1 ∈ x.asIdeal
exact hx h