case refine'_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : ∃ s, {x} = zeroLocus s
⊢ Ideal.IsMaximal x.asIdeal

case refine'_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : Ideal.IsMaximal x.asIdeal
⊢ ∃ s, {x} = zeroLocus s
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
⊢ IsClosed {x} ↔ Ideal.IsMaximal x.asIdeal
refine' (isClosed_iff_zeroLocus _).trans ⟨fun h => _, fun h => _⟩
case refine'_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
s : Set R
hs : {x} = zeroLocus s
⊢ Ideal.IsMaximal x.asIdeal
case refine'_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : ∃ s, {x} = zeroLocus s
⊢ Ideal.IsMaximal x.asIdeal
obtain ⟨s, hs⟩ := h
case refine'_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
s : Set R
hs : x ∈ zeroLocus s ∧ ∀ (x_1 : PrimeSpectrum R), x_1 ∈ zeroLocus s → x_1 = x
⊢ Ideal.IsMaximal x.asIdeal
case refine'_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
s : Set R
hs : {x} = zeroLocus s
⊢ Ideal.IsMaximal x.asIdeal
rw [eq_comm, Set.eq_singleton_iff_unique_mem] at hs
case refine'_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
s : Set R
hs : x ∈ zeroLocus s ∧ ∀ (x_1 : PrimeSpectrum R), x_1 ∈ zeroLocus s → x_1 = x
I : Ideal R
hI : x.asIdeal < I
J : Ideal R
hJ : Ideal.IsMaximal J
hIJ : I ≤ J
⊢ False
case refine'_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
s : Set R
hs : x ∈ zeroLocus s ∧ ∀ (x_1 : PrimeSpectrum R), x_1 ∈ zeroLocus s → x_1 = x
⊢ Ideal.IsMaximal x.asIdeal
refine'
  ⟨⟨x.2.1, fun I hI =>
      Classical.not_not.1
        (mt (Ideal.exists_le_maximal I) <| not_exists.2 fun J => not_and.2 fun hJ hIJ => _)⟩⟩
no goals
case refine'_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
s : Set R
hs : x ∈ zeroLocus s ∧ ∀ (x_1 : PrimeSpectrum R), x_1 ∈ zeroLocus s → x_1 = x
I : Ideal R
hI : x.asIdeal < I
J : Ideal R
hJ : Ideal.IsMaximal J
hIJ : I ≤ J
⊢ False
exact
  ne_of_lt (lt_of_lt_of_le hI hIJ)
    (symm <|
      congr_arg PrimeSpectrum.asIdeal
        (hs.2 ⟨J, hJ.isPrime⟩ fun r hr => hIJ (le_of_lt hI <| hs.1 hr)))
case refine'_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : Ideal.IsMaximal x.asIdeal
⊢ {x} = zeroLocus ↑x.asIdeal.toAddSubmonoid
case refine'_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : Ideal.IsMaximal x.asIdeal
⊢ ∃ s, {x} = zeroLocus s
refine' ⟨x.asIdeal.1, _⟩
case refine'_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : Ideal.IsMaximal x.asIdeal
⊢ x ∈ zeroLocus ↑x.asIdeal.toAddSubmonoid ∧
    ∀ (x_1 : PrimeSpectrum R), x_1 ∈ zeroLocus ↑x.asIdeal.toAddSubmonoid → x_1 = x
case refine'_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : Ideal.IsMaximal x.asIdeal
⊢ {x} = zeroLocus ↑x.asIdeal.toAddSubmonoid
rw [eq_comm, Set.eq_singleton_iff_unique_mem]
no goals
case refine'_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : Ideal.IsMaximal x.asIdeal
⊢ x ∈ zeroLocus ↑x.asIdeal.toAddSubmonoid ∧
    ∀ (x_1 : PrimeSpectrum R), x_1 ∈ zeroLocus ↑x.asIdeal.toAddSubmonoid → x_1 = x
refine' ⟨fun _ h => h, fun y hy => PrimeSpectrum.ext _ _ (h.eq_of_le y.2.ne_top hy).symm⟩