no goals
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddZeroClass G
f : AddMonoidAlgebra k G
⊢ f ∈ Submodule.span k (↑(of k G) '' ↑f.support)
erw [of, MonoidHom.coe_mk, ← Finsupp.supported_eq_span_single, Finsupp.mem_supported]