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

Proof state:
case h.refine_1.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
a : p.IsPrime
ha : I.radical ≤ p
b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y

Tactic:
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4

Result:
no goals

Proof state:
case h.refine_1.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ p ∈ {p | Minimal (fun q => q.IsPrime ∧ I ≤ q) p}

Tactic:
refine ⟨⟨a, a.radical_le_iff.1 ha⟩, ?_⟩

Result:
case h.refine_1.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ {p | Minimal (fun q => q.IsPrime ∧ I.radical ≤ q) p} = {p | Minimal (fun q => q.IsPrime ∧ I ≤ q) p}

Tactic:
ext p

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
⊢ p ∈ {p | Minimal (fun q => q.IsPrime ∧ I.radical ≤ q) p} ↔ p ∈ {p | Minimal (fun q => q.IsPrime ∧ I ≤ q) p}

Proof state:
case h.refine_2.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y

Tactic:
simp only [Set.mem_setOf_eq, and_imp] at *

Result:
case h.refine_2.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
a : p.IsPrime
ha : I ≤ p
b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
⊢ p ∈ {p | Minimal (fun q => q.IsPrime ∧ I.radical ≤ q) p} ↔ p ∈ {p | Minimal (fun q => q.IsPrime ∧ I ≤ q) p}

Tactic:
refine ⟨?_, ?_⟩ <;> rintro ⟨⟨a, ha⟩, b⟩

Result:
case h.refine_1.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ p ∈ {p | Minimal (fun q => q.IsPrime ∧ I ≤ q) p}

case h.refine_2.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ p ∈ {p | Minimal (fun q => q.IsPrime ∧ I.radical ≤ q) p}

Proof state:
case h.refine_2.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
a : p.IsPrime
ha : I ≤ p
b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y

Tactic:
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4

Result:
no goals

Proof state:
case h.refine_2.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ p ∈ {p | Minimal (fun q => q.IsPrime ∧ I.radical ≤ q) p}

Tactic:
refine ⟨⟨a, a.radical_le_iff.2 ha⟩, ?_⟩

Result:
case h.refine_2.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y

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

Tactic:
rw [Ideal.minimalPrimes, Ideal.minimalPrimes]

Result:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ {p | Minimal (fun q => q.IsPrime ∧ I.radical ≤ q) p} = {p | Minimal (fun q => q.IsPrime ∧ I ≤ q) p}

Proof state:
case h.refine_1.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y

Tactic:
simp only [Set.mem_setOf_eq, and_imp] at *

Result:
case h.refine_1.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
a : p.IsPrime
ha : I.radical ≤ p
b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y