∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq κ] [inst_2 : Fintype κ]
  (s : Finset ι) (g : ι → κ) (f : ι → M), ∑ j, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s, f i