-- Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
theorem Ideal.iUnion_minimalPrimes :
    ⋃ p ∈ I.minimalPrimes, p = { x | ∃ y ∉ I.radical, x * y ∈ I.radical }

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
⊢ ∃ p ∈ I.minimalPrimes, y ∉ p

Tactic:
simpa [← Ideal.sInf_minimalPrimes] using hy

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ i ∈ I.minimalPrimes, x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
constructor

Result:
case h.mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ i ∈ I.minimalPrimes, x ∈ i) → ∃ y ∉ I.radical, x * y ∈ I.radical

case h.mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ y ∉ I.radical, x * y ∈ I.radical) → ∃ i ∈ I.minimalPrimes, x ∈ i

Proof state:
case h.mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
p : Ideal R
hp : p ∈ I.minimalPrimes
hyp : y ∉ p
⊢ x * y ∈ p

Tactic:
exact hp.1.1.radical_le_iff.mpr hp.1.2 hx

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
⊢ map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical

Tactic:
rw [Ideal.radical_eq_sInf, le_sInf_iff]

Result:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
⊢ ∀ b ∈ {J | map (algebraMap R (Localization.AtPrime p)) I ≤ J ∧ J.IsPrime},
    map (algebraMap R (Localization.AtPrime p)) p ≤ b

Proof state:
case h.mp.intro.intro.intro.intro.intro.intro.mk.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) ∈ I

Tactic:
have : (x * (t.1 * b.1)) ^ (n + 1) = (t.1 ^ n * b.1 ^ n * x * t.1) * a := by
  rw [mul_assoc, ← ht]; ring

Result:
case h.mp.intro.intro.intro.intro.intro.intro.mk.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this✝ : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
this : (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) ∈ I

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ ⋃ p ∈ I.minimalPrimes, ↑p = {x | ∃ y ∉ I.radical, x * y ∈ I.radical}

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ x ∈ ⋃ p ∈ I.minimalPrimes, ↑p ↔ x ∈ {x | ∃ y ∉ I.radical, x * y ∈ I.radical}

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * ↑t * ↑a

Tactic:
rw [mul_assoc, ← ht]

Result:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * (↑t * (x ^ n * ↑b))

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ x ∈ ⋃ p ∈ I.minimalPrimes, ↑p ↔ x ∈ {x | ∃ y ∉ I.radical, x * y ∈ I.radical}

Tactic:
simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop, Set.mem_setOf_eq]

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ i ∈ I.minimalPrimes, x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical

Proof state:
case h.mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
hn :
  ∃ x_1,
    (algebraMap R (Localization.AtPrime p)) x ^ n * (algebraMap R (Localization.AtPrime p)) ↑x_1.2 =
      (algebraMap R (Localization.AtPrime p)) ↑x_1.1
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
obtain ⟨⟨a, b⟩, hn⟩ := hn

Result:
case h.mp.intro.intro.intro.intro.intro.intro.mk
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b : ↥p.primeCompl
hn :
  (algebraMap R (Localization.AtPrime p)) x ^ n * (algebraMap R (Localization.AtPrime p)) ↑(a, b).2 =
    (algebraMap R (Localization.AtPrime p)) ↑(a, b).1
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Proof state:
case h.mp.intro.intro.intro.intro.intro.intro.mk.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑(a, b).2) = ↑t * ↑(a, b).1
⊢ (x * (↑t * ↑b)) ^ (n + 1) ∈ I

Tactic:
simp only at ht

Result:
case h.mp.intro.intro.intro.intro.intro.intro.mk.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) ∈ I

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : map (algebraMap R (Localization.AtPrime p)) I ≤ q
hq : q.IsPrime
h₁ : (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p) ⟨q, hq⟩)).IsPrime
h₂ : ↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p) ⟨q, hq⟩) ≤ p
⊢ map (algebraMap R (Localization.AtPrime p)) p ≤ q

Tactic:
rw [Ideal.map_le_iff_le_comap] at hq' ⊢

Result:
case intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q => q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : I ≤ comap (algebraMap R (Localization.AtPrime p)) q
hq : q.IsPrime
h₁ : (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p) ⟨q, hq⟩)).IsPrime
h₂ : ↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p) ⟨q, hq⟩) ≤ p
⊢ p ≤ comap (algebraMap R (Localization.AtPrime p)) q