∀ {α : Type u_1} {R : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring R] (s : Finset α) (f : α → R) (n : ℕ),
  (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(Nat.multinomial s k) * ∏ i ∈ s, f i ^ k i