## Stream: maths

#### Chris Hughes (Oct 12 2019 at 17:14):

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 (Oct 12 2019 at 18:08):

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];

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)