Member of a set is a member of its span

Stream: Is there code for X?

[Ashvni Narayanan]

I have a feeling the following lemma should exist somewhere :

import ring_theory.fractional_ideal

open_locale classical

variables (B : Type*) [semiring B]
variables (M : Type*) [add_comm_monoid M] [semimodule B M]

open submodule

lemma mem_span_set (x : M) (S : set M) (hx : x ∈ S) : x ∈ span B S :=
begin
  suffices f : S ⊆ span B S,
  apply iff.rfl.1 f hx,
  apply submodule.subset_span,
end

Any help is appreciated, thank you!

[Kenny Lau]

This is just submodule.subset_span

[Kenny Lau]

lemma mem_span_set (x : M) (S : set M) (hx : x ∈ S) : x ∈ span B S :=
submodule.subset_span hx

[Patrick Massot]

Ashvni, the proof of your suffices is iff.rfl, so you don't need it.

[Ashvni Narayanan]

I see, thank you!

[Kevin Buzzard]

The point is that $A\subseteq B$ is definitionally equal to $\forall x, x\in A \implies x\in B$

[Ashvni Narayanan]

I get it now, thank you!