mathlib3

2c4e66f7 - split(data/finset/*): Split `data.finset.card` and `data.finset.fin` off `data.finset.basic` (#10796)

split(data/finset/*): Split `data.finset.card` and `data.finset.fin` off `data.finset.basic` (#10796) This moves stuff from `data.finset.basic` in two new files: * Stuff about `finset.card` goes into `data.finset.card` * Stuff about `finset.fin_range` and `finset.attach_fin` goes into `data.finset.fin`. I expect this file to be shortlived as I'm planning on killing `fin_range`. I reordered lemmas thematically and it appeared that there were two pairs of duplicated lemmas: * `finset.one_lt_card`, `finset.one_lt_card_iff`. They differ only for binder order. * `finset.card_union_eq`, `finset.card_disjoint_union`. They are literally the same. All are used so I will clean up in a later PR. I'm crediting: * Microsoft Corporation, Leonardo, Jeremy for 8dbee5b1ca9680a22ffe90751654f51d6852d7f0 * Chris Hughes for #231 * Scott for #3319