R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this : DecidableEq (Ideal A)
⊢ I = P ^ i
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
⊢ I = P ^ i
have := Classical.decEq (Ideal A)
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this : DecidableEq (Ideal A)
⊢ P ^ i ≤ I
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this : DecidableEq (Ideal A)
⊢ I = P ^ i
refine le_antisymm hle ?_
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this : DecidableEq (Ideal A)
P_prime' : Prime P
⊢ P ^ i ≤ I
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this : DecidableEq (Ideal A)
⊢ P ^ i ≤ I
have P_prime' := Ideal.prime_of_isPrime hP P_prime
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this : DecidableEq (Ideal A)
P_prime' : Prime P
h1 : I ≠ ⊥
⊢ P ^ i ≤ I
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this : DecidableEq (Ideal A)
P_prime' : Prime P
⊢ P ^ i ≤ I
have h1 : I ≠ ⊥ := (lt_of_le_of_lt bot_le hlt).ne'
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
⊢ P ^ i ≤ I
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this : DecidableEq (Ideal A)
P_prime' : Prime P
h1 : I ≠ ⊥
⊢ P ^ i ≤ I
have := pow_ne_zero i hP
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
⊢ P ^ i ≤ I
have h3 := pow_ne_zero (i + 1) hP
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt✝ : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
hlt : normalizedFactors I ≤ Multiset.replicate i (↑normalize P)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I
rw [← Ideal.dvdNotUnit_iff_lt, dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors h1 h3,
  normalizedFactors_pow, normalizedFactors_irreducible P_prime'.irreducible,
  Multiset.nsmul_singleton, Multiset.lt_replicate_succ] at hlt
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt✝ : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
hlt : normalizedFactors I ≤ Multiset.replicate i (↑normalize P)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ normalizedFactors I ≤ Multiset.replicate i (↑normalize P)

case hx
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt✝ : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
hlt : normalizedFactors I ≤ Multiset.replicate i (↑normalize P)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ I ≠ 0

case hy
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt✝ : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
hlt : normalizedFactors I ≤ Multiset.replicate i (↑normalize P)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≠ 0
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt✝ : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
hlt : normalizedFactors I ≤ Multiset.replicate i (↑normalize P)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I
rw [← Ideal.dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors, normalizedFactors_pow,
  normalizedFactors_irreducible P_prime'.irreducible, Multiset.nsmul_singleton]
no goals
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt✝ : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
hlt : normalizedFactors I ≤ Multiset.replicate i (↑normalize P)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ normalizedFactors I ≤ Multiset.replicate i (↑normalize P)

case hx
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt✝ : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
hlt : normalizedFactors I ≤ Multiset.replicate i (↑normalize P)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ I ≠ 0

case hy
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt✝ : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
hlt : normalizedFactors I ≤ Multiset.replicate i (↑normalize P)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≠ 0
all_goals assumption
no goals
case hy
R : Type ?u.810058
A : Type u_1
K : Type ?u.810064
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P I : Ideal A
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
hlt✝ : P ^ (i + 1) < I
hle : I ≤ P ^ i
this✝ : DecidableEq (Ideal A)
hlt : normalizedFactors I ≤ Multiset.replicate i (↑normalize P)
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≠ 0
assumption