∀ {ι : Type u_1} {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] {m : Multiset ι} {s : Finset α} {f : ι → α → M},
  (Multiset.map (fun i => ∑ a ∈ s, f i a) m).sum = ∑ a ∈ s, (Multiset.map (fun i => f i a) m).sum