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 ↑(Submonoid.map (of R M) (closure S))
⊢ m ∈ closure 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 ↑(closure (↑(of R M) '' S))
⊢ m ∈ closure S
rw [← MonoidHom.map_mclosure] 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 : ↑(of R M) m ∈ span R ↑(Submonoid.map (of R M) (closure S))
⊢ m ∈ closure S
simpa using of_mem_span_of_iff.1 h