chore(fintype): add @[simp] to card_univ

[ericrbg]

---

This feels like a simp lemma, which makes me fear that there's a good reason that it's not done yet. Please don't merge instantly - if compile doesn't scream at me (and others agree it seems like a good idea) I'll just make one more pass removing any explicit card_univs from other files

[bryangingechen]

It's not obvious to me that this should be a simp lemma in this direction; isn't fintype.card defined in terms of finset.univ.card? (It could potentially be a good idea, if fintype.card has a more extensive API, but that seems unlikely to me.)

Regarding the PR title, I think we usually use "feat" for new theorems (stuff with at least some recognizable "mathematical" content) or tactics; in my opinion, adding attributes & other general code cleanup falls under "refactor", "fix" or "chore".

[ericrbg]

yes, fintype.card is finset.univ.card; however, fintype has results such as |α → β| = |β| ^ |α|, |α ⊕ β| = |α| + |β|, whilst it seems to me that most finset results about card are about subsets, insertions, maps and such like; however, not sure if this is just me as I'm working with a fair few pigeonhole/cardinality arguments right now.

[ericrbg]

I'll fix the title! I wasn't sure about what to title it when I first added it

[ericrbg]

close as not a good idea