proof about sums

Stream: maths

[Chris Hughes]

What is the correct proof of this? It can be done in short way using definitional unfolding, but this isn't very stable.

example {α : Type*} [add_comm_monoid α] (f : fin 4 → α) :
  univ.sum f = f 0 + f 1 + f 2 + f 3

[Kenny Lau]

import data.fintype

open finset

example {α : Type*} [add_comm_monoid α] (f : fin 4 → α) :
  univ.sum f = f 0 + f 1 + f 2 + f 3 :=
have huniv : (univ : finset (fin 4)).val = 0::1::2::3::0, from dec_trivial,
show multiset.sum _ = _,
by rw huniv; simp only [multiset.map_cons, multiset.map_zero, multiset.sum_cons, multiset.sum_zero];
rw add_zero; iterate 2 { rw ← add_assoc }

[Kenny Lau]

I mean, the f 0 + f 1 + f 2 + f 3 part isn't very clearly generalizable. (clearly it isn't list.sum (list.range 4) f)