case pos
R : Type u_1
A : Type ?u.1186416
K : Type ?u.1186419
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I P : Ideal R
hP : IsPrime P
n : ℕ
h : I ^ n ≤ P
hP0 : P = ⊥
⊢ I ≤ P

case neg
R : Type u_1
A : Type ?u.1186416
K : Type ?u.1186419
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I P : Ideal R
hP : IsPrime P
n : ℕ
h : I ^ n ≤ P
hP0 : ¬P = ⊥
⊢ I ≤ P
R : Type u_1
A : Type ?u.1186416
K : Type ?u.1186419
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I P : Ideal R
hP : IsPrime P
n : ℕ
h : I ^ n ≤ P
⊢ I ≤ P
by_cases hP0 : P = ⊥
case neg
R : Type u_1
A : Type ?u.1186416
K : Type ?u.1186419
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I P : Ideal R
hP : IsPrime P
n : ℕ
h : P ∣ I ^ n
hP0 : ¬P = ⊥
⊢ P ∣ I
case neg
R : Type u_1
A : Type ?u.1186416
K : Type ?u.1186419
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I P : Ideal R
hP : IsPrime P
n : ℕ
h : I ^ n ≤ P
hP0 : ¬P = ⊥
⊢ I ≤ P
rw [← Ideal.dvd_iff_le] at h ⊢
no goals
case neg
R : Type u_1
A : Type ?u.1186416
K : Type ?u.1186419
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I P : Ideal R
hP : IsPrime P
n : ℕ
h : P ∣ I ^ n
hP0 : ¬P = ⊥
⊢ P ∣ I
exact ((Ideal.prime_iff_isPrime hP0).mpr hP).dvd_of_dvd_pow h
case pos
R : Type u_1
A : Type ?u.1186416
K : Type ?u.1186419
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I P : Ideal R
hP : IsPrime P
n : ℕ
hP0 : P = ⊥
h : I ^ n = ⊥
⊢ I = ⊥
case pos
R : Type u_1
A : Type ?u.1186416
K : Type ?u.1186419
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I P : Ideal R
hP : IsPrime P
n : ℕ
h : I ^ n ≤ P
hP0 : P = ⊥
⊢ I ≤ P
simp only [hP0, le_bot_iff] at h ⊢
no goals
case pos
R : Type u_1
A : Type ?u.1186416
K : Type ?u.1186419
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I P : Ideal R
hP : IsPrime P
n : ℕ
hP0 : P = ⊥
h : I ^ n = ⊥
⊢ I = ⊥
exact pow_eq_zero h