-- Mathlib/RingTheory/Spectrum/Prime/Jacobson.lean
/--
If `R` is both noetherian and jacobson, then the following are equivalent for `x : Spec R`:
1. `{x}` is open (i.e. `x` is an isolated point)
2. `{x}` is clopen
3. `{x}` is both closed and stable under generalization
  (i.e. `x` is both a minimal prime and a maximal ideal)
-/
lemma isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing
    [IsNoetherianRing R] [IsJacobsonRing R] (x : PrimeSpectrum R) :
    List.TFAE [IsOpen {x}, IsClopen {x}, IsClosed {x} ∧ StableUnderGeneralization {x}]

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
⊢ [IsOpen {x}, IsClopen {x}, IsClosed {x} ∧ StableUnderGeneralization {x}].TFAE

Tactic:
tfae_have 2 → 3
| h => ⟨h.isClosed, h.isOpen.stableUnderGeneralization⟩

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
⊢ [IsOpen {x}, IsClopen {x}, IsClosed {x} ∧ StableUnderGeneralization {x}].TFAE

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
this : {x} = (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})ᶜ
⊢ {p | IsMin p ∧ p ≠ x}.Finite

Tactic:
exact (finite_setOf_isMin R).subset fun x h ↦ h.1

Result:
no goals

Proof state:
case h.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
p : PrimeSpectrum R
⊢ p = x → ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x

Tactic:
rintro rfl _ _

Result:
case h.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
p : PrimeSpectrum R
tfae_1_to_2 : IsOpen {p} → IsClopen {p}
tfae_2_to_3 : IsClopen {p} → IsClosed {p} ∧ StableUnderGeneralization {p}
h₁ : IsMax p
h₂ : StableUnderGeneralization {p}
i✝ : PrimeSpectrum R
a✝ : IsMin i✝
⊢ i✝ ≤ p → i✝ = p

Proof state:
case h.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
p : PrimeSpectrum R
tfae_1_to_2 : IsOpen {p} → IsClopen {p}
tfae_2_to_3 : IsClopen {p} → IsClosed {p} ∧ StableUnderGeneralization {p}
h₁ : IsMax p
h₂ : StableUnderGeneralization {p}
i✝ : PrimeSpectrum R
a✝ : IsMin i✝
⊢ i✝ ≤ p → i✝ = p

Tactic:
rw [stableUnderGeneralization_singleton, ← isMin_iff] at h₂

Result:
case h.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
p : PrimeSpectrum R
tfae_1_to_2 : IsOpen {p} → IsClopen {p}
tfae_2_to_3 : IsClopen {p} → IsClosed {p} ∧ StableUnderGeneralization {p}
h₁ : IsMax p
h₂ : IsMin p
i✝ : PrimeSpectrum R
a✝ : IsMin i✝
⊢ i✝ ≤ p → i✝ = p

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
y : PrimeSpectrum R
h' : IsClosed {y}
x✝ : IsOpen {y}
h : IsOpen {y} := x✝
⊢ IsClopen {y}

Tactic:
exact ⟨h', h⟩

Result:
no goals

Proof state:
case h.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
p : PrimeSpectrum R
tfae_1_to_2 : IsOpen {p} → IsClopen {p}
tfae_2_to_3 : IsClopen {p} → IsClosed {p} ∧ StableUnderGeneralization {p}
h₁ : IsMax p
h₂ : IsMin p
i✝ : PrimeSpectrum R
a✝ : IsMin i✝
⊢ i✝ ≤ p → i✝ = p

Tactic:
exact h₂.eq_of_le

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
this : {x} = (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})ᶜ
⊢ IsClosed (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})

Tactic:
refine Set.Finite.isClosed_biUnion ?_ (fun _ _ ↦ isClosed_closure)

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
this : {x} = (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})ᶜ
⊢ {p | IsMin p ∧ p ≠ x}.Finite

Proof state:
case h.mpr.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
p : PrimeSpectrum R
hp : ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
q : Ideal R
hq : q ∈ ⊥.minimalPrimes
hq' : q ≤ p.asIdeal
⊢ x ≤ p

Tactic:
exact (hp ⟨q, hq.1.1⟩ (isMin_iff.mpr hq) hq').ge.trans hq'

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
tfae_3_to_1 : IsClosed {x} ∧ StableUnderGeneralization {x} → IsOpen {x}
⊢ [IsOpen {x}, IsClopen {x}, IsClosed {x} ∧ StableUnderGeneralization {x}].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
case h.mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
p : PrimeSpectrum R
⊢ (∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x) → p = x

Tactic:
intros hp

Result:
case h.mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
p : PrimeSpectrum R
hp : ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
⊢ p = x

Proof state:
case h.mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
p : PrimeSpectrum R
hp : ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
⊢ x ≤ p

Tactic:
obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le

Result:
case h.mpr.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
p : PrimeSpectrum R
hp : ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
q : Ideal R
hq : q ∈ ⊥.minimalPrimes
hq' : q ≤ p.asIdeal
⊢ x ≤ p

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
this : {x} = (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})ᶜ
⊢ IsOpen {x}

Tactic:
rw [this, isOpen_compl_iff]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
this : {x} = (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})ᶜ
⊢ IsClosed (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})