Sums over finsets

Stream: maths

[Johan Commelin]

I'm stuck on the following triviality

lemma sums {m n : ℕ} (f : fin m → fin n) (x : fin m → ℕ)
: sum univ (λ j : fin n, sum (univ.filter (λ i, f i = j)) x) = sum univ x
:= sorry

It looks like I might want to use finset.sum_sigma but I don't see how to get all the sigma's in place. And the unification magic doesn't do the job either.

[Johan Commelin]

@Kevin Buzzard @Chris Hughes I remember that you were also working on these kind of sum-rewritings about 2 months ago. Is this similar to what you did?

[Johannes Hölzl]

you can use finset.sum_bind to combine both sum to a single one and then use extensionality that the combination of the index sets on the right is univ. Or use finset.sum_subset which also uses some sort of extensionality.

[Johan Commelin]

Ok, thanks!

[Johan Commelin]

Ok, I proved the lemma using bind and ext.2. Thanks a lot!