finset.univ.sum

Stream: new members

[Tianchen Zhao]

I am trying to prove this statement about finset.univ.sum which should be easy but I have no ideas how to do this in Lean. I tried unfolding some defitions but it looked even more complicated. Is there a tactic or lemma I can use?

import data.real.basic

example (f : (fin 2) → ℝ) :
finset.univ.sum (λ (x : fin 2), f x) = f 0 + f 1 :=
begin
  sorry,
end

[Eric Wieser]

docs#fin.sum_univ_succ

[Scott Morrison]

It would be nice to have a tactic to handle this, along the lines of fin_cases: explode of sum over a finite set.

[Eric Wieser]

What order would it expand the sum into?

[Eric Wieser]

Maybe that doesn't matter; I suppose meta code has docs#quot.unquot to pick an arbitrary order

[Scott Morrison]

I guess whatever order fin_cases hands you the cases in!

[Eric Wieser]

Well, fin_cases only works on fin; I thought you meant for any finite type

[Scott Morrison]

Really? I remember it working more generally. tactic#fin_cases

[Eric Wieser]

Oh, I didn't know that

[Scott Morrison]

No, it works on anything where fintype is available.

[Eric Wieser]

The tests are insightful: https://github.com/leanprover-community/mathlib/blob/0591c276d560de91873adabc939a656bf9d0b827/test/fin_cases.lean