case zero
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
h : a * b ∈ I ^ Nat.zero
⊢ a ∈ I ∨ b ∈ I ^ Nat.zero

case succ
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
h : a * b ∈ I ^ Nat.succ n✝
⊢ a ∈ I ∨ b ∈ I ^ Nat.succ n✝
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ∨ b ∈ I ^ n
cases n
case pos
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
h : a * b ∈ I ^ Nat.succ n✝
hI0 : I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ Nat.succ n✝

case neg
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
h : a * b ∈ I ^ Nat.succ n✝
hI0 : ¬I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ Nat.succ n✝
case succ
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
h : a * b ∈ I ^ Nat.succ n✝
⊢ a ∈ I ∨ b ∈ I ^ Nat.succ n✝
by_cases hI0 : I = ⊥
case neg
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ Nat.succ n✝ ∣ span {a} * span {b}
⊢ I ∣ span {a} ∨ I ^ Nat.succ n✝ ∣ span {b}
case neg
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
h : a * b ∈ I ^ Nat.succ n✝
hI0 : ¬I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ Nat.succ n✝
simp only [← Submodule.span_singleton_le_iff_mem, Ideal.submodule_span_eq, ← Ideal.dvd_iff_le, ←
  Ideal.span_singleton_mul_span_singleton] at h ⊢
case pos
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ Nat.succ n✝ ∣ span {a} * span {b}
ha : I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ Nat.succ n✝ ∣ span {b}

case neg
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ Nat.succ n✝ ∣ span {a} * span {b}
ha : ¬I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ Nat.succ n✝ ∣ span {b}
case neg
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ Nat.succ n✝ ∣ span {a} * span {b}
⊢ I ∣ span {a} ∨ I ^ Nat.succ n✝ ∣ span {b}
by_cases ha : I ∣ span {a}
case neg
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ Nat.succ n✝ ∣ span {b} * span {a}
ha : ¬I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ Nat.succ n✝ ∣ span {b}
case neg
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ Nat.succ n✝ ∣ span {a} * span {b}
ha : ¬I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ Nat.succ n✝ ∣ span {b}
rw [mul_comm] at h
no goals
case neg
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ Nat.succ n✝ ∣ span {b} * span {a}
ha : ¬I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ Nat.succ n✝ ∣ span {b}
exact Or.inr (Prime.pow_dvd_of_dvd_mul_right ((Ideal.prime_iff_isPrime hI0).mpr hI) _ ha h)
no goals
case zero
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
h : a * b ∈ I ^ Nat.zero
⊢ a ∈ I ∨ b ∈ I ^ Nat.zero
simp
no goals
case pos
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
h : a * b ∈ I ^ Nat.succ n✝
hI0 : I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ Nat.succ n✝
simpa [pow_succ, hI0] using h
no goals
case pos
R : Type u_1
A : Type ?u.1174042
K : Type ?u.1174045
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : IsPrime I
a b : R
n✝ : ℕ
hI0 : ¬I = ⊥
h : I ^ Nat.succ n✝ ∣ span {a} * span {b}
ha : I ∣ span {a}
⊢ I ∣ span {a} ∨ I ^ Nat.succ n✝ ∣ span {b}
exact Or.inl ha