Indexing over finite sets?

Stream: new members

[Kristaps John Balodis]

I have a couple related questions.
First, I'm trying to prove a theorem for an arbitrary amount of finite numbers $a_1, ..., a_n$. I figured I could do this by considering a finite sequence. In other words, having $a$ just be a function $S\to\mathbb{N}$ for some finite subset $S\subseteq\mathbb{N}$.
However, I'm unsure of how to get a finite set. I tried looking at something like

 constant S : finset \nat

but them Lean wasn't liking

constant a : S \to S

(but I don't have this problem with set \nat) So my first question is,
1) Why isn't this working?
also
2) What is the best way to grab an arbitrary index set/arbitrary finite set of naturals?
Finally,
3) How does one form a repeated sum over these? Say I want to get $a_1+... +a_n$?

[Johan Commelin]

@Kristaps John Balodis you can use something like

variables {X : Type*} [fintype X] (a : X \to nat)

[Johan Commelin]

You can sum over those by

import algebra.big_operators

open_locale big_operators

example : \sum i : X, a i = 0 := sorry

[Kristaps John Balodis]

Thanks!