case h
R : Type u_1
S : Type ?u.121108
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I ↔ J ∈ {radical I}
R : Type u_1
S : Type ?u.121108
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
hI : IsPrimary I
⊢ Ideal.minimalPrimes I = {radical I}
ext J
case h.mp
R : Type u_1
S : Type ?u.121108
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I → J ∈ {radical I}

case h.mpr
R : Type u_1
S : Type ?u.121108
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ {radical I} → J ∈ Ideal.minimalPrimes I
case h
R : Type u_1
S : Type ?u.121108
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I ↔ J ∈ {radical I}
constructor
no goals
case h.mp
R : Type u_1
S : Type ?u.121108
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I → J ∈ {radical I}
exact fun H =>
  let e := H.1.1.radical_le_iff.mpr H.1.2
  (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ e).antisymm e
case h.mpr
R : Type u_1
S : Type ?u.121108
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
hI : IsPrimary I
⊢ radical I ∈ Ideal.minimalPrimes I
case h.mpr
R : Type u_1
S : Type ?u.121108
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ {radical I} → J ∈ Ideal.minimalPrimes I
rintro (rfl : J = I.radical)
no goals
case h.mpr
R : Type u_1
S : Type ?u.121108
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
hI : IsPrimary I
⊢ radical I ∈ Ideal.minimalPrimes I
exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩