R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : CommMonoid 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✝¹ : CommMonoid 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✝¹ : CommMonoid 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✝¹ : CommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑(of R M) m ∈ span R (↑(of R M) '' S)
⊢ m ∈ S
erw [of, MonoidHom.coe_mk, ← 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✝¹ : CommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑{m} ⊆ S
⊢ m ∈ S
simpa using h