finset/fintype

Stream: new members

[Alex Zhang]

How can I prove the following?

import algebra.big_operators
import data.fintype.card
import data.finset.basic

open_locale big_operators

variables {α β: Type*} {s : finset α} {f g : α → β} [add_comm_monoid β] (a : α) (b : β)

variables {I : Type*} [fintype I] [decidable_eq I]

example (i : I) (f : I → β):
∑ (x : I) in finset.filter (λ (x : I), x = i) (@finset.univ I _), f x = f i :=
begin

end

[Yakov Pechersky]

docs#finset.filter_eq' and docs#finset.sum_ite like we did above

[Alex Zhang]

Great! I will try them. I forgot docs#finset.filter_eq' . I was searching for things like finset.sum_filter... and didn't find anything relavant.

[Alex Zhang]

It turns out simp [finset.filter_eq'] closes the goal in one step!