no goals
R : Type u
ι : Type ?u.246088
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) ∧ ∀ (zJ : R), zJ ∈ J → ∃ zI, zI ∈ I ∧ x * zI = y * zJ
simp only [le_antisymm_iff, span_singleton_mul_le_span_singleton_mul, eq_comm]