feat(data/finset): finset lemmas from combinatorics (#2149)
The beginnings of moving results from my combinatorics project
Make sure you have:
* [x] reviewed and applied the coding style: [coding](https://github.com/leanprover/mathlib/blob/master/docs/contribute/style.md), [naming](https://github.com/leanprover/mathlib/blob/master/docs/contribute/naming.md)
* [x] reviewed and applied [the documentation requirements](https://github.com/leanprover/mathlib/blob/master/docs/contribute/doc.md)
* [x] make sure definitions and lemmas are put in the right files
* [x] make sure definitions and lemmas are not redundant
For reviewers: [code review check list](https://github.com/leanprover/mathlib/blob/master/docs/contribute/code-review.md)
