no goals
R : Type u
ι : Type ?u.306186
inst✝ : CommSemiring R
I J K L : Ideal R
w x y z : R
⊢ span {w, x} * span {y, z} = span {w * y, w * z, x * y, x * z}
simp_rw [span_insert, sup_mul, mul_sup, span_singleton_mul_span_singleton, sup_assoc]