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