-- Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
theorem Ideal.exists_mul_mem_of_mem_minimalPrimes
    {p : Ideal R} (hp : p ∈ I.minimalPrimes) {x : R} (hx : x ∈ p) :
    ∃ y ∉ I, x * y ∈ I

Proof state:
case intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
this : Nat.find H ≠ 0
⊢ x * (x ^ (Nat.find H - 1) * y ^ n) ∈ I

Tactic:
rw [← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.mpr this)]

Result:
case intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
this : Nat.find H ≠ 0
⊢ x ^ Nat.find H * y ^ n ∈ I

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
h : Nat.find H = 0
⊢ y ^ n ∈ I

Tactic:
simpa only [h, pow_zero, one_mul] using Nat.find_spec H

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
⊢ ∃ y ∉ I, x * y ∈ I

Tactic:
have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩

Result:
case intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
⊢ ∃ y ∉ I, x * y ∈ I

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

Tactic:
classical
obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)
have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩
have : Nat.find H ≠ 0 :=
  fun h ↦ hy ⟨n, by simpa only [h, pow_zero, one_mul] using Nat.find_spec H⟩
refine ⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩
rw [← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.mpr this)]
exact Nat.find_spec H

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
this : Nat.find H ≠ 0
⊢ ∃ y ∉ I, x * y ∈ I

Tactic:
refine ⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩

Result:
case intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
this : Nat.find H ≠ 0
⊢ x * (x ^ (Nat.find H - 1) * y ^ n) ∈ I

Proof state:
case intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
⊢ ∃ y ∉ I, x * y ∈ I

Tactic:
have : Nat.find H ≠ 0 :=
  fun h ↦ hy ⟨n, by simpa only [h, pow_zero, one_mul] using Nat.find_spec H⟩

Result:
case intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
this : Nat.find H ≠ 0
⊢ ∃ y ∉ I, x * y ∈ I

Proof state:
case intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
this : Nat.find H ≠ 0
⊢ x ^ Nat.find H * y ^ n ∈ I

Tactic:
exact Nat.find_spec H

Result:
no goals

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

Tactic:
obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)

Result:
case intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
⊢ ∃ y ∉ I, x * y ∈ I