mathlib

2287b1c9 - chore(data/fintype): rework `fintype.equiv_fin` and dependencies

chore(data/fintype): rework `fintype.equiv_fin` and dependencies These changes should make the declarations `fintype.equiv_fin`, `fintype.card_eq` and `fintype.equiv_of_card_eq` more convenient to use. Renamed: * `fintype.equiv_fin` -> `fintype.trunc_equiv_fin` Deleted: * `fintype.nonempty_equiv_of_card_eq` (use `fintype.equiv_of_card_eq` instead) Added: * `fintype.equiv_fin`: noncomputable, non-`trunc` version of `fintype.equiv_fin` * `fintype.equiv_of_card_eq`: noncomputable, non-`trunc` version of `fintype.trunc_equiv_of_card_eq` * `fintype.(trunc_)equiv_fin_of_card_eq` (intermediate result/specialization of `fintype.(trunc_)equiv_of_card_eq`