-- Mathlib/RingTheory/Ideal/AssociatedPrime.lean
theorem associatedPrimes.eq_singleton_of_isPrimary [IsNoetherianRing R] (hI : I.IsPrimary) :
    associatedPrimes R (R ⧸ I) = {I.radical}

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J ∈ {I.radical}

Tactic:
rw [Set.mem_singleton_iff]

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J = I.radical

Proof state:
case h.intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
this : Nontrivial (R ⧸ I)
a : Ideal R
ha : a ∈ associatedPrimes R (R ⧸ I)
⊢ I.radical ∈ associatedPrimes R (R ⧸ I)

Tactic:
exact ha.eq_radical hI ▸ ha

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
this : Nontrivial (R ⧸ I)
⊢ I.radical ∈ associatedPrimes R (R ⧸ I)

Tactic:
obtain ⟨a, ha⟩ := associatedPrimes.nonempty R (R ⧸ I)

Result:
case h.intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
this : Nontrivial (R ⧸ I)
a : Ideal R
ha : a ∈ associatedPrimes R (R ⧸ I)
⊢ I.radical ∈ associatedPrimes R (R ⧸ I)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
⊢ ¬I = ⊤

Tactic:
exact hI.1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
⊢ Nontrivial (R ⧸ I)

Tactic:
refine ⟨(Ideal.Quotient.mk I :) 1, (Ideal.Quotient.mk I :) 0, ?_⟩

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
⊢ (Ideal.Quotient.mk I) 1 ≠ (Ideal.Quotient.mk I) 0

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
⊢ I.radical ∈ associatedPrimes R (R ⧸ I)

Tactic:
haveI : Nontrivial (R ⧸ I) := by
  refine ⟨(Ideal.Quotient.mk I :) 1, (Ideal.Quotient.mk I :) 0, ?_⟩
  rw [Ne, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]
  exact hI.1

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
this : Nontrivial (R ⧸ I)
⊢ I.radical ∈ associatedPrimes R (R ⧸ I)

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J = I.radical

Tactic:
refine ⟨IsAssociatedPrime.eq_radical hI, ?_⟩

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ J = I.radical → J ∈ associatedPrimes R (R ⧸ I)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
⊢ (Ideal.Quotient.mk I) 1 ≠ (Ideal.Quotient.mk I) 0

Tactic:
rw [Ne, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
⊢ ¬I = ⊤

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
⊢ associatedPrimes R (R ⧸ I) = {I.radical}

Tactic:
ext J

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J ∈ {I.radical}

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ J = I.radical → J ∈ associatedPrimes R (R ⧸ I)

Tactic:
rintro rfl

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
⊢ I.radical ∈ associatedPrimes R (R ⧸ I)