Understanding Set and finset better

Stream: new members

[ROCKY KAMEN-RUBIO]

Has anyone written any tutorials on sets and finsets/fintypes/nodeup/card? I'm having trouble understanding what's going on just from the documentation.

[Patrick Massot]

we have https://leanprover-community.github.io/theories/sets.html

[Bhavik Mehta]

If your goal is to use finsets, fintype and card, I'd suggest looking at the theorem statements in data.finset and data.fintype, and totally ignoring nodup

[Bhavik Mehta]

There's a very thorough finset API (albeit not the best documented) but at no point should you need to worry about how a finset is actually implemented

[ROCKY KAMEN-RUBIO]

Bhavik Mehta said:

There's a very thorough finset API (albeit not the best documented) but at no point should you need to worry about how a finset is actually implemented

That's good to know. A lot of my confusion was coming from the implementation so I'll try ignoring that and see if I can make better sense of it.