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