case pos
R : Type ?u.918814
A : Type ?u.918817
K : Type ?u.918820
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ multiplicity J I
hI : I = ⊥
⊢ J ^ n ⊔ I = J ^ n

case neg
R : Type ?u.918814
A : Type ?u.918817
K : Type ?u.918820
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ multiplicity J I
hI : ¬I = ⊥
⊢ J ^ n ⊔ I = J ^ n
R : Type ?u.918814
A : Type ?u.918817
K : Type ?u.918820
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ multiplicity J I
⊢ J ^ n ⊔ I = J ^ n
by_cases hI : I = ⊥
case neg
R : Type ?u.918814
A : Type ?u.918817
K : Type ?u.918820
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ multiplicity J I
hI : ¬I = ⊥
⊢ n ≤ count J (normalizedFactors I)
case neg
R : Type ?u.918814
A : Type ?u.918817
K : Type ?u.918820
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ multiplicity J I
hI : ¬I = ⊥
⊢ J ^ n ⊔ I = J ^ n
rw [irreducible_pow_sup hI hJ, min_eq_right]
no goals
case neg
R : Type ?u.918814
A : Type ?u.918817
K : Type ?u.918820
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ multiplicity J I
hI : ¬I = ⊥
⊢ n ≤ count J (normalizedFactors I)
rwa [multiplicity_eq_count_normalizedFactors hJ hI, PartENat.coe_le_coe, normalize_eq J] at hn
no goals
case pos
R : Type ?u.918814
A : Type ?u.918817
K : Type ?u.918820
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ multiplicity J I
hI : I = ⊥
⊢ J ^ n ⊔ I = J ^ n
simp_all