theorem Submodule.fg_span_iff_fg_span_finset_subset (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : (span R s).FG ↔ ∃ (s' : Finset M), ↑s' ⊆ s ∧ span R s = span R ↑s'

theorem Submodule.mem_of_mem_of_le (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s t : Submodule R M} (hx : x ∈ s) (h : s ≤ t) : x ∈ t

theorem Submodule.mem_span_of_mem (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} (hx : x ∈ s) : x ∈ span R s