R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) = sInf {J | I ≤ J ∧ IsPrime J}
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) = radical I
rw [I.radical_eq_sInf]
case a
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) ≤ sInf {J | I ≤ J ∧ IsPrime J}

case a
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf {J | I ≤ J ∧ IsPrime J} ≤ sInf (Ideal.minimalPrimes I)
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) = sInf {J | I ≤ J ∧ IsPrime J}
apply le_antisymm
case a
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
hx : x ∈ sInf (Ideal.minimalPrimes I)
⊢ x ∈ sInf {J | I ≤ J ∧ IsPrime J}
case a
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) ≤ sInf {J | I ≤ J ∧ IsPrime J}
intro x hx
case a
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsPrime J} → x ∈ I_1
case a
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
hx : x ∈ sInf (Ideal.minimalPrimes I)
⊢ x ∈ sInf {J | I ≤ J ∧ IsPrime J}
rw [Ideal.mem_sInf] at hx⊢
case a.intro
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : IsPrime J
⊢ x ∈ J
case a
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsPrime J} → x ∈ I_1
rintro J ⟨e, hJ⟩
case a.intro.intro.intro
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : IsPrime J
p : Ideal R
hp : p ∈ Ideal.minimalPrimes I
hp' : p ≤ J
⊢ x ∈ J
case a.intro
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : IsPrime J
⊢ x ∈ J
obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le e
no goals
case a.intro.intro.intro
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : IsPrime J
p : Ideal R
hp : p ∈ Ideal.minimalPrimes I
hp' : p ≤ J
⊢ x ∈ J
exact hp' (hx hp)
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ Ideal.minimalPrimes I ⊆ {J | I ≤ J ∧ IsPrime J}
case a
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf {J | I ≤ J ∧ IsPrime J} ≤ sInf (Ideal.minimalPrimes I)
apply sInf_le_sInf _
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J I : Ideal R
hI : I ∈ Ideal.minimalPrimes I✝
⊢ I ∈ {J | I✝ ≤ J ∧ IsPrime J}
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ Ideal.minimalPrimes I ⊆ {J | I ≤ J ∧ IsPrime J}
intro I hI
no goals
R : Type u_1
S : Type ?u.5834
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J I : Ideal R
hI : I ∈ Ideal.minimalPrimes I✝
⊢ I ∈ {J | I✝ ≤ J ∧ IsPrime J}
exact hI.1.symm