R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R (of' R M '' S)
⊢ m ∈ S
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
⊢ of' R M m ∈ span R (of' R M '' S) ↔ m ∈ S
refine' ⟨fun h => _, fun h => Submodule.subset_span <| Set.mem_image_of_mem (of R M) h⟩
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑{m} ⊆ S
⊢ m ∈ S
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R (of' R M '' S)
⊢ m ∈ S
erw [of', ← Finsupp.supported_eq_span_single, Finsupp.mem_supported,
  Finsupp.support_single_ne_zero _ (one_ne_zero' R)] at h
no goals
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑{m} ⊆ S
⊢ m ∈ S
simpa using h