no goals
R : Type ?u.914699
A : Type ?u.914702
K : Type ?u.914705
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
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
⊢ J ^ n ⊔ I = J ^ min (count J (normalizedFactors I)) n
rw [sup_eq_prod_inf_factors (pow_ne_zero n hJ.ne_zero) hI, min_comm,
  normalizedFactors_of_irreducible_pow hJ, normalize_eq J, replicate_inter, prod_replicate]