∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_8}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (s : Set M) (t : Set M'),
  Submodule.span R (s ×ˢ t) ≤ (Submodule.span R s).prod (Submodule.span R t)