Span compatibility imports

The upstream file supplied Submodule.mem_span_image_finset_iff_exists_fun; that declaration is available in current Mathlib from Mathlib.LinearAlgebra.Finsupp.LinearCombination, so this file is kept as an import-compatible shim.