Lemmas for action of ideals on submodules of Finsupp

theorem Finsupp.submodule_smul (R : Type u_1) [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (ι : Type u_3) (p : ι → Submodule R M) (I : Ideal R) : (submodule fun (i : ι) => I • p i) = I • submodule p