-- Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
theorem Ideal.sInf_minimalPrimes : sInf I.minimalPrimes = I.radical

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : x ∈ sInf I.minimalPrimes
⊢ x ∈ sInf {J | I ≤ J ∧ J.IsPrime}

Tactic:
rw [Ideal.mem_sInf] at hx ⊢

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsPrime} → x ∈ I_1

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf {J | I ≤ J ∧ J.IsPrime} ≤ sInf I.minimalPrimes

Tactic:
apply sInf_le_sInf _

Result:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes ⊆ {J | I ≤ J ∧ J.IsPrime}

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I✝ I : Ideal R
hI : I ∈ I✝.minimalPrimes
⊢ I ∈ {J | I✝ ≤ J ∧ J.IsPrime}

Tactic:
exact hI.1.symm

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes = sInf {J | I ≤ J ∧ J.IsPrime}

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes ≤ sInf {J | I ≤ J ∧ J.IsPrime}

case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf {J | I ≤ J ∧ J.IsPrime} ≤ sInf I.minimalPrimes

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes = I.radical

Tactic:
rw [I.radical_eq_sInf]

Result:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes = sInf {J | I ≤ J ∧ J.IsPrime}

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes ≤ sInf {J | I ≤ J ∧ J.IsPrime}

Tactic:
intro x hx

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : x ∈ sInf I.minimalPrimes
⊢ x ∈ sInf {J | I ≤ J ∧ J.IsPrime}

Proof state:
case a.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : J.IsPrime
p : Ideal R
hp : p ∈ I.minimalPrimes
hp' : p ≤ J
⊢ x ∈ J

Tactic:
exact hp' (hx hp)

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsPrime} → x ∈ I_1

Tactic:
rintro J ⟨e, hJ⟩

Result:
case a.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : J.IsPrime
⊢ x ∈ J

Proof state:
case a.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : J.IsPrime
⊢ x ∈ J

Tactic:
obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le e

Result:
case a.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : J.IsPrime
p : Ideal R
hp : p ∈ I.minimalPrimes
hp' : p ≤ J
⊢ x ∈ J

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes ⊆ {J | I ≤ J ∧ J.IsPrime}

Tactic:
intro I hI

Result:
R : Type u_1
inst✝ : CommSemiring R
I✝ I : Ideal R
hI : I ∈ I✝.minimalPrimes
⊢ I ∈ {J | I✝ ≤ J ∧ J.IsPrime}