R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} =
    minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ Ideal.minimalPrimes (radical I) = Ideal.minimalPrimes I
rw [Ideal.minimalPrimes, Ideal.minimalPrimes]
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} =
    minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} =
    minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
congr
case h
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} ↔
    p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} =
    minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
ext p
case h.refine'_1.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : radical I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}

case h.refine'_2.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p}
case h
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} ↔
    p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
refine' ⟨_, _⟩ <;> rintro ⟨⟨a, ha⟩, b⟩
case h.refine'_2.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p}
case h.refine'_1.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : radical I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}

case h.refine'_2.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p}
. refine' ⟨⟨a, a.radical_le_iff.1 ha⟩, _⟩
  . simp only [Set.mem_setOf_eq, and_imp] at *
    exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4
no goals
case h.refine'_2.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p}
. refine' ⟨⟨a, a.radical_le_iff.2 ha⟩, _⟩
  . simp only [Set.mem_setOf_eq, and_imp] at *
    exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4
case h.refine'_1.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : radical I ≤ p
⊢ ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
case h.refine'_1.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : radical I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
refine' ⟨⟨a, a.radical_le_iff.1 ha⟩, _⟩
no goals
case h.refine'_1.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : radical I ≤ p
⊢ ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
. simp only [Set.mem_setOf_eq, and_imp] at *
  exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4
case h.refine'_1.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
a : IsPrime p
ha : radical I ≤ p
b : ∀ ⦃b : Ideal R⦄, IsPrime b → radical I ≤ b → b ≤ p → p ≤ b
⊢ ∀ ⦃b : Ideal R⦄, IsPrime b → I ≤ b → b ≤ p → p ≤ b
case h.refine'_1.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : radical I ≤ p
⊢ ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
simp only [Set.mem_setOf_eq, and_imp] at *
no goals
case h.refine'_1.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
a : IsPrime p
ha : radical I ≤ p
b : ∀ ⦃b : Ideal R⦄, IsPrime b → radical I ≤ b → b ≤ p → p ≤ b
⊢ ∀ ⦃b : Ideal R⦄, IsPrime b → I ≤ b → b ≤ p → p ≤ b
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4
case h.refine'_2.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
case h.refine'_2.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p}
refine' ⟨⟨a, a.radical_le_iff.2 ha⟩, _⟩
no goals
case h.refine'_2.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
. simp only [Set.mem_setOf_eq, and_imp] at *
  exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4
case h.refine'_2.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
a : IsPrime p
ha : I ≤ p
b : ∀ ⦃b : Ideal R⦄, IsPrime b → I ≤ b → b ≤ p → p ≤ b
⊢ ∀ ⦃b : Ideal R⦄, IsPrime b → radical I ≤ b → b ≤ p → p ≤ b
case h.refine'_2.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
simp only [Set.mem_setOf_eq, and_imp] at *
no goals
case h.refine'_2.intro.intro
R : Type u_1
S : Type ?u.3948
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
a : IsPrime p
ha : I ≤ p
b : ∀ ⦃b : Ideal R⦄, IsPrime b → I ≤ b → b ≤ p → p ≤ b
⊢ ∀ ⦃b : Ideal R⦄, IsPrime b → radical I ≤ b → b ≤ p → p ≤ b
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4