-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical :
    letI s := {I : Ideal R | I.IsMaximal}
    DiscreteTopology (PrimeSpectrum R) ↔ Finite s ∧ sInf s ≤ nilradical R

Proof state:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
M : Ideal R
hM : M ∈ {I | I.IsMaximal}
hMI : id M ≤ I
⊢ I.IsMaximal

Tactic:
rwa [← hM.eq_of_le hI.1 hMI]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
M : Ideal R
hM : M ∈ fin.toFinset
hMI : id M ≤ I
⊢ I.IsMaximal

Tactic:
rw [fin.mem_toFinset] at hM

Result:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
M : Ideal R
hM : M ∈ {I | I.IsMaximal}
hMI : id M ≤ I
⊢ I.IsMaximal

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ ({x | x.IsPrime}.Finite ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) ↔
    {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R

Tactic:
refine ⟨fun h ↦ ⟨h.1.subset fun _ h ↦ h.isPrime, nilradical_eq_sInf R ▸ sInf_le_sInf h.2⟩,
  fun ⟨fin, le⟩ ↦ ?_⟩

Result:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
le : sInf {I | I.IsMaximal} ≤ nilradical R
⊢ {x | x.IsPrime}.Finite ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Proof state:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : sInf {I | I.IsMaximal} ≤ I
⊢ I.IsMaximal

Tactic:
rw [← fin.coe_toFinset, ← Finset.inf_id_eq_sInf, hI.inf_le'] at le

Result:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
⊢ I.IsMaximal

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ DiscreteTopology (PrimeSpectrum R) ↔ Finite ↑{I | I.IsMaximal} ∧ sInf {I | I.IsMaximal} ≤ nilradical R

Tactic:
rw [discreteTopology_iff_finite_and_krullDimLE_zero, Ring.krullDimLE_zero_iff,
  (equivSubtype R).finite_iff, ← Set.coe_setOf, Set.finite_coe_iff, Set.finite_coe_iff]

Result:
R : Type u
inst✝ : CommSemiring R
⊢ ({x | x.IsPrime}.Finite ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) ↔
    {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R

Proof state:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
⊢ I.IsMaximal

Tactic:
have ⟨M, hM, hMI⟩ := le

Result:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
M : Ideal R
hM : M ∈ fin.toFinset
hMI : id M ≤ I
⊢ I.IsMaximal

Proof state:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
le : sInf {I | I.IsMaximal} ≤ nilradical R
I : Ideal R
hI : I.IsPrime
⊢ I.IsMaximal

Tactic:
replace le := le.trans (nilradical_le_prime I)

Result:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : sInf {I | I.IsMaximal} ≤ I
⊢ I.IsMaximal

Proof state:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
le : sInf {I | I.IsMaximal} ≤ nilradical R
hpm : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
⊢ {x | x.IsPrime}.Finite ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
exact ⟨fin.subset hpm, hpm⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
le : sInf {I | I.IsMaximal} ≤ nilradical R
⊢ {x | x.IsPrime}.Finite ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
have hpm (I : Ideal R) (hI : I.IsPrime): I.IsMaximal := by
  replace le := le.trans (nilradical_le_prime I)
  rw [← fin.coe_toFinset, ← Finset.inf_id_eq_sInf, hI.inf_le'] at le
  have ⟨M, hM, hMI⟩ := le
  rw [fin.mem_toFinset] at hM
  rwa [← hM.eq_of_le hI.1 hMI]

Result:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
le : sInf {I | I.IsMaximal} ≤ nilradical R
hpm : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
⊢ {x | x.IsPrime}.Finite ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal