no goals
R : Type u
ι : Type ?u.236329
inst✝¹ : CommSemiring R
I J K L : Ideal R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
⊢ span {x} * I ≤ span {x} * J ↔ I ≤ J
simp_rw [span_singleton_mul_le_span_singleton_mul, mul_right_inj' hx,
  exists_eq_right', SetLike.le_def]