case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ zeroLocus ↑I = ∅ → I = ⊤

case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ I = ⊤ → zeroLocus ↑I = ∅
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ zeroLocus ↑I = ∅ ↔ I = ⊤
constructor
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ I ≠ ⊤ → zeroLocus ↑I ≠ ∅
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ zeroLocus ↑I = ∅ → I = ⊤
contrapose!
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
h : I ≠ ⊤
⊢ zeroLocus ↑I ≠ ∅
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ I ≠ ⊤ → zeroLocus ↑I ≠ ∅
intro h
case mp.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
h : I ≠ ⊤
M : Ideal R
hM : Ideal.IsMaximal M
hIM : I ≤ M
⊢ zeroLocus ↑I ≠ ∅
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
h : I ≠ ⊤
⊢ zeroLocus ↑I ≠ ∅
rcases Ideal.exists_le_maximal I h with ⟨M, hM, hIM⟩
no goals
case mp.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
h : I ≠ ⊤
M : Ideal R
hM : Ideal.IsMaximal M
hIM : I ≤ M
⊢ zeroLocus ↑I ≠ ∅
exact Set.Nonempty.ne_empty ⟨⟨M, hM.isPrime⟩, hIM⟩
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ zeroLocus ↑⊤ = ∅
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ I = ⊤ → zeroLocus ↑I = ∅
rintro rfl
case mpr.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 1 ∈ ↑⊤
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ zeroLocus ↑⊤ = ∅
apply zeroLocus_empty_of_one_mem
no goals
case mpr.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 1 ∈ ↑⊤
trivial