Difficultly applying `monoid_algebra`

Stream: general

[Eric Wieser]

We have a lemma docs#monoid_algebra.mul_apply that suggests there is a suitable coe_to_fun instance - yet I can't actually form a function expression using that type:

 import data.monoid_algebra

open_locale big_operators

def grading_inv_fail1 {X : Type*} [semiring X] (g : monoid_algebra X ℕ) : X :=
  ∑ i in g.support, g i

def grading_inv_fail2 {X : Type*} [semiring X] (g : monoid_algebra X ℕ) : X :=
  ∑ i in g.support, ((g : ℕ → X) i)

def grading_inv_works {X : Type*} [semiring X] (g : monoid_algebra X ℕ) : X :=
  ∑ i in g.support, g.to_fun i

Why is the linked lemma statement even legal? Do I just need to add a missing has_coe_to_fun instance?

instance {R X : Type*} [semiring X] : has_coe_to_fun (monoid_algebra X R) := finsupp.has_coe_to_fun

[Gabriel Ebner]

I believe this might have to do with it:

local attribute [reducible] monoid_algebra

[Gabriel Ebner]

:+1: for adding a has_coe and a has_coe_to_fun instance.

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/0bb5e5d/src/data/monoid_algebra.lean#L61

[Eric Wieser]

Done in #4315