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

Proof state:
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

Tactic:
rintro ⟨p, ⟨⟨hp₁, hp₂⟩, hp₃⟩, hxp⟩

Result:
case h.mp.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
⊢ ∃ 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 : (algebraMap R (Localization.AtPrime p)) x ^ n ∈ map (algebraMap R (Localization.AtPrime p)) I
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
rw [IsLocalization.mem_map_algebraMap_iff (M := p.primeCompl)] at hn

Result:
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

Proof state:
case 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
⊢ map (algebraMap R (Localization.AtPrime p)) p ≤ q

Tactic:
obtain ⟨h₁, h₂⟩ := ((IsLocalization.AtPrime.orderIsoOfPrime _ p) ⟨q, hq⟩).2

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' : 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

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
⊢ ∃ i ∈ I.minimalPrimes, x ∈ i

Tactic:
refine ⟨p, hp, (hp.1.1.mem_or_mem ?_).resolve_right hyp⟩

Result:
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

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 * (x ^ n * ↑b))

Tactic:
ring

Result:
no goals

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

Tactic:
obtain ⟨p, hp, hyp⟩ : ∃ p ∈ I.minimalPrimes, y ∉ p := by
  simpa [← Ideal.sInf_minimalPrimes] using hy

Result:
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
⊢ ∃ i ∈ I.minimalPrimes, x ∈ i

Proof state:
case h.mp.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
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
obtain ⟨n, hn⟩ := this (Ideal.mem_map_of_mem _ hxp)

Result:
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 : (algebraMap R (Localization.AtPrime p)) x ^ n ∈ map (algebraMap R (Localization.AtPrime p)) I
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Proof state:
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

Tactic:
rintro ⟨y, hy, hx⟩

Result:
case h.mpr.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
⊢ ∃ i ∈ I.minimalPrimes, x ∈ i

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
this : (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * ↑t * ↑a
⊢ ↑t ^ n * ↑b ^ n * x * ↑t * ↑a ∈ I

Tactic:
exact I.mul_mem_left _ a.2

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
⊢ ∀ b ∈ {J | map (algebraMap R (Localization.AtPrime p)) I ≤ J ∧ J.IsPrime},
    map (algebraMap R (Localization.AtPrime p)) p ≤ b

Tactic:
rintro q ⟨hq', hq⟩

Result:
case 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
⊢ map (algebraMap R (Localization.AtPrime p)) p ≤ q

Proof state:
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 : ∃ c, ↑c * (x ^ n * ↑(a, b).2) = ↑c * ↑(a, b).1
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
obtain ⟨t, ht⟩ := hn

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 * ↑(a, b).2) = ↑t * ↑(a, b).1
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical