R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | Ideal.IsMaximal x.asIdeal}
R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | IsClosed {x}}
simp only [isClosed_singleton_iff_isMaximal]
case h.mk
R : Type u
inst✝ : CommRing R
x : Ideal R
IsPrime✝ : Ideal.IsPrime x
⊢ { asIdeal := x, IsPrime := IsPrime✝ } ∈ range toPrimeSpectrum ↔
    { asIdeal := x, IsPrime := IsPrime✝ } ∈ {x | Ideal.IsMaximal x.asIdeal}
R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | Ideal.IsMaximal x.asIdeal}
ext ⟨x, _⟩
no goals
case h.mk
R : Type u
inst✝ : CommRing R
x : Ideal R
IsPrime✝ : Ideal.IsPrime x
⊢ { asIdeal := x, IsPrime := IsPrime✝ } ∈ range toPrimeSpectrum ↔
    { asIdeal := x, IsPrime := IsPrime✝ } ∈ {x | Ideal.IsMaximal x.asIdeal}
exact ⟨fun ⟨y, hy⟩ => hy ▸ y.IsMaximal, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩