-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.IsPrime.mul_mem_pow (I : Ideal R) [hI : I.IsPrime] {a b : R} {n : ℕ}
    (h : a * b ∈ I ^ n) : a ∈ I ∨ b ∈ I ^ n

Proof state:
case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)

Tactic:
by_cases hI0 : I = ⊥

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
hI0 : I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
hI0 : ¬I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)

Proof state:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
h : a * b ∈ I ^ 0
⊢ a ∈ I ∨ b ∈ I ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ (n✝ + 1) ∣ span {a} * span {b}
ha : I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}

Tactic:
exact Or.inl ha

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
hI0 : I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)

Tactic:
simpa [pow_succ, hI0] using h

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ (n✝ + 1) ∣ span {a} * span {b}
⊢ I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}

Tactic:
by_cases ha : I ∣ span {a}

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ (n✝ + 1) ∣ span {a} * span {b}
ha : I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ (n✝ + 1) ∣ span {a} * span {b}
ha : ¬I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ (n✝ + 1) ∣ span {a} * span {b}
ha : ¬I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}

Tactic:
rw [mul_comm] at h

Result:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ (n✝ + 1) ∣ span {b} * span {a}
ha : ¬I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
hI0 : ¬I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)

Tactic:
simp only [← Submodule.span_singleton_le_iff_mem, Ideal.submodule_span_eq, ← Ideal.dvd_iff_le, ←
  Ideal.span_singleton_mul_span_singleton] at h ⊢

Result:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ (n✝ + 1) ∣ span {a} * span {b}
⊢ I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ (n✝ + 1) ∣ span {b} * span {a}
ha : ¬I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}

Tactic:
exact Or.inr (Prime.pow_dvd_of_dvd_mul_right ((Ideal.prime_iff_isPrime hI0).mpr hI) _ ha h)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ∨ b ∈ I ^ n

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
h : a * b ∈ I ^ 0
⊢ a ∈ I ∨ b ∈ I ^ 0

case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)