∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {v : α →₀ M}
  {f : α ↪ β} {g : β → M → N}, (Finsupp.embDomain f v).prod g = v.prod fun a b => g (f a) b