∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I J : Ideal T},
  I ≠ ⊥ →
    Irreducible J → ∀ (n : ℕ), J ^ n ⊔ I = J ^ min (Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)) n