-- Mathlib/RingTheory/Spectrum/Prime/Jacobson.lean
lemma isJacobsonRing_iff_jacobsonSpace :
    IsJacobsonRing R ↔ JacobsonSpace (PrimeSpectrum R)

Proof state:
case h.intro
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
x : PrimeSpectrum R
hx : I ≤ x.asIdeal
hx' : x ∈ closedPoints (PrimeSpectrum R)
⊢ x ∈ zeroLocus ↑I.jacobson

Tactic:
show jacobson I ≤ x.asIdeal

Result:
case h.intro
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
x : PrimeSpectrum R
hx : I ≤ x.asIdeal
hx' : x ∈ closedPoints (PrimeSpectrum R)
⊢ I.jacobson ≤ x.asIdeal

Proof state:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson.radical ≤ I.radical

Tactic:
simp_rw [← vanishingIdeal_zeroLocus_eq_radical]

Result:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ vanishingIdeal (zeroLocus ↑I.jacobson) ≤ vanishingIdeal (zeroLocus ↑I)

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ zeroLocus ↑I ∩ closedPoints (PrimeSpectrum R) ⊆ zeroLocus ↑I.jacobson

Tactic:
rintro x ⟨hx : I ≤ x.asIdeal, hx'⟩

Result:
case h.intro
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
x : PrimeSpectrum R
hx : I ≤ x.asIdeal
hx' : x ∈ closedPoints (PrimeSpectrum R)
⊢ x ∈ zeroLocus ↑I.jacobson

Proof state:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson ≤ I

Tactic:
rw [← I.isRadical_jacobson.radical]

Result:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson.radical ≤ I

Proof state:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ vanishingIdeal (zeroLocus ↑I.jacobson) ≤ vanishingIdeal (zeroLocus ↑I)

Tactic:
apply vanishingIdeal_anti_mono

Result:
case h
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ zeroLocus ↑I ⊆ zeroLocus ↑I.jacobson

Proof state:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson.radical ≤ I

Tactic:
conv_rhs => rw [← hI.radical]

Result:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson.radical ≤ I.radical

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ zeroLocus ↑I ⊆ zeroLocus ↑I.jacobson

Tactic:
rw [← H.1 (isClosed_zeroLocus I), (isClosed_zeroLocus _).closure_subset_iff]

Result:
case h
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ zeroLocus ↑I ∩ closedPoints (PrimeSpectrum R) ⊆ zeroLocus ↑I.jacobson

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ IsJacobsonRing R ↔ JacobsonSpace (PrimeSpectrum R)

Tactic:
refine ⟨fun _ ↦ inferInstance, fun H ↦ ⟨fun I hI ↦ le_antisymm ?_ Ideal.le_jacobson⟩⟩

Result:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson ≤ I

Proof state:
case h.intro
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
x : PrimeSpectrum R
hx : I ≤ x.asIdeal
hx' : x ∈ closedPoints (PrimeSpectrum R)
⊢ I.jacobson ≤ x.asIdeal

Tactic:
exact sInf_le ⟨hx, (isClosed_singleton_iff_isMaximal _).mp hx'⟩

Result:
no goals