mathlib3

67dad976 - chore(data/fintype): rework `fintype.equiv_fin` and dependencies (#7136)

chore(data/fintype): rework `fintype.equiv_fin` and dependencies (#7136) 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) * `fintype.exists_equiv_fin` (use `fintype.card` and `fintype.(trunc_)equiv_fin` 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` [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60fintype.2Eequiv_fin.60.20.2B.20.60fin.2Ecast.60) Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>