∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {s : Finset β}
  (f : α →₀ M) (h : α → M → β → N), (f.sum fun a m => ∑ b ∈ s, h a m b) = ∑ b ∈ s, f.sum fun a m => h a m b