-- Mathlib/RingTheory/Spectrum/Prime/Jacobson.lean
lemma exists_isClosed_singleton_of_isJacobsonRing [IsJacobsonRing R]
    (s : (Set (PrimeSpectrum R))) (hs : IsOpen s) (hs' : s.Nonempty) :
    ∃ x ∈ s, IsClosed {x}

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ ∀ b ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}, I.jacobson ≤ b

Tactic:
rintro x ⟨-, hx⟩

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
x : Ideal R
hx : x.IsMaximal
⊢ I.jacobson ≤ x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
⊢ ∃ x ∈ s, x.asIdeal.IsMaximal

Tactic:
obtain ⟨I, hI'⟩ := (isClosed_iff_zeroLocus_ideal _).mp hs.isClosed_compl

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
⊢ ∃ x ∈ s, x.asIdeal.IsMaximal

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), ¬↑I ⊆ ↑x.asIdeal → ¬x.asIdeal.IsMaximal
⊢ s = ∅

Tactic:
simp_rw [not_imp_not] at this

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ s = ∅

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : s ≠ ∅
⊢ ∃ x, ¬↑I ⊆ ↑x.asIdeal ∧ x.asIdeal.IsMaximal

Tactic:
contrapose! this

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), ¬↑I ⊆ ↑x.asIdeal → ¬x.asIdeal.IsMaximal
⊢ s = ∅

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
⊢ ∃ x ∈ s, x.asIdeal.IsMaximal

Tactic:
simp_rw [← @Set.not_mem_compl_iff _ s, hI', mem_zeroLocus]

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
⊢ ∃ x, ¬↑I ⊆ ↑x.asIdeal ∧ x.asIdeal.IsMaximal

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ I.jacobson = ⊥.jacobson

Tactic:
refine le_antisymm (le_sInf ?_) (Ideal.jacobson_mono bot_le)

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ ∀ b ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}, I.jacobson ≤ b

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
⊢ ∃ x, ¬↑I ⊆ ↑x.asIdeal ∧ x.asIdeal.IsMaximal

Tactic:
have := hs'.ne_empty

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : s ≠ ∅
⊢ ∃ x, ¬↑I ⊆ ↑x.asIdeal ∧ x.asIdeal.IsMaximal

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ s = ∅

Tactic:
rw [← Set.compl_univ, eq_compl_comm, hI', eq_comm, ← zeroLocus_bot,
  zeroLocus_eq_iff, Ideal.radical_eq_jacobson, Ideal.radical_eq_jacobson]

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ I.jacobson = ⊥.jacobson

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
⊢ ∃ x ∈ s, IsClosed {x}

Tactic:
simp_rw [isClosed_singleton_iff_isMaximal]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
⊢ ∃ x ∈ s, x.asIdeal.IsMaximal

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
x : Ideal R
hx : x.IsMaximal
⊢ I.jacobson ≤ x

Tactic:
exact sInf_le ⟨this ⟨x, hx.isPrime⟩ hx, hx⟩

Result:
no goals