theorem Fintype.sum_pi_single_pi {α : Type u_1} {β : α → Type u_2} [DecidableEq α] [Fintype α] [(a : α) → AddCommMonoid (β a)] (f : (a : α) → β a) : ∑ a : α, Pi.single a (f a) = f