Help proving with a sum over a subtype

Stream: new members

[Robert Shlyakhtenko]

I would like to prove the following statement:

∑' (i : { x // x ∈ l.permutations }), 1 = (l.permutations.toFinset.card : ENNReal)

However, I'm having a hard time finding any theorems with Moogle/Loogle that would be helpful, and I haven't found a clean way to prove this myself. Does anyone have any suggestions?

[Kevin Buzzard]

My suggestion is to write a #mwe so that people can understand the question you're asking.

[Aaron Liu]

@loogle tsum, Finset.sum, |- _ = _

[Aaron Liu]

@loogle tsum, Finset.sum, |- _ = _

[loogle]

:search: tsum_fintype, sum_eq_tsum_indicator, and 36 more

[Aaron Liu]

@loogle Finset.sum, 1, Finset.card

[loogle]

:search: Finset.card_eq_sum_ones, Finset.eq_of_card_le_one_of_sum_eq, and 49 more

[Aaron Liu]

Try using docs#tsum_fintype and the reverse of docs#Finset.card_eq_sum_ones

[Aaron Liu]

This will get rid of the sum