no goals
R : Type u
ι : Type ?u.234437
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x y : R
I J : Ideal R
⊢ span {x} * I ≤ span {y} * J ↔ ∀ (zI : R), zI ∈ I → ∃ zJ, zJ ∈ J ∧ x * zI = y * zJ
simp only [span_singleton_mul_le_iff, mem_span_singleton_mul, eq_comm]