Application of `add_monoid_hom` distributes over `sum`

Stream: Is there code for X?

[Eric Wieser]

This goal is frustrating me:

import data.finsupp.basic

variables {α β M N P : Type*}

@[simp]
lemma add_monoid_hom.finsupp_sum_apply [has_zero β] [add_comm_monoid N] [add_comm_monoid P]
  (f : α →₀ β) (g : α → β → N →+ P) (x : N) :
  f.sum g x = f.sum (λ i fi, g i fi x) :=
begin
  let app := (add_monoid_hom.apply (λ _ : N, P) x),
  dsimp at app,
  change app (f.sum g : N →+ P) = _,
  convert add_monoid_hom.map_finsupp_sum _ f g,
  -- oops
end

[Eric Wieser]

Do we have this?

namespace add_monoid_hom

def apply_hom [add_comm_monoid N] [add_comm_monoid P] (x : N) : (N →+ P) →+ P :=
{ to_fun := λ f, f x,
  map_add' := λ f g, add_apply _ _ x,
  map_zero' := zero_apply x }

end add_monoid_hom

We have docs#add_monoid_hom.apply, but that doesn't seem to help here

[Eric Wieser]

Ah, it's docs#add_monoid_hom.eval