Range of a map out of Finsupp

Stream: Is there code for X?

[Robin Carlier]

import Mathlib.LinearAlgebra.Finsupp

universe u v w

lemma span_map (α : Type u) (R : Type v) (M : Type w) [Semiring R] [AddCommMonoid M] [Module R M]
    (f : (α →₀ R) →ₗ[R] M) : LinearMap.range f =
    ⨆ (a : α), Submodule.span R {f (Finsupp.lsingle (R := R) (M := R) a 1)} := by
  sorry

Is this already somewhere? This looks doable by combining Finsupp.iSup_lsingle_range and Submodule.span_singlenton_eq_rangeas far as I can see