no goals
R : Type ?u.817526
A : Type u_1
K : Type ?u.817532
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
n : ℕ
I : Ideal A
⊢ Associates.mk I ^ n ≤ Associates.mk (span {x}) ↔ x ∈ I ^ n
simp_rw [← Associates.dvd_eq_le, ← Associates.mk_pow, Associates.mk_dvd_mk,
  Ideal.dvd_span_singleton]