R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ span R (↑(of R M) '' ↑f.support) ≤ ↑Subalgebra.toSubmodule (adjoin R (↑(of R M) '' ↑f.support))
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ f ∈ adjoin R (↑(of R M) '' ↑f.support)
suffices span R (of R M '' f.support) ≤ Subalgebra.toSubmodule (adjoin R (of R M '' f.support)) by
  exact this (mem_span_support f)
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ ↑(of R M) '' ↑f.support ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R (↑(of R M) '' ↑f.support)))
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ span R (↑(of R M) '' ↑f.support) ≤ ↑Subalgebra.toSubmodule (adjoin R (↑(of R M) '' ↑f.support))
rw [Submodule.span_le]
no goals
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ ↑(of R M) '' ↑f.support ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R (↑(of R M) '' ↑f.support)))
exact subset_adjoin
no goals
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
this : span R (↑(of R M) '' ↑f.support) ≤ ↑Subalgebra.toSubmodule (adjoin R (↑(of R M) '' ↑f.support))
⊢ f ∈ adjoin R (↑(of R M) '' ↑f.support)
exact this (mem_span_support f)