feat(data/fintype/basic): add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. (#15080)
feat(data/fintype/basic): add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. (#15080)

As `s.card` is not defeq to `fintype.card s`, it is convenient to have these definitions in addition to `fintype.equiv_fin` and others (though we omit the computable ones).


Co-authored-by: Wrenna Robson <58db46417c18ed5414020ce20e6ff4c1ce6ca8ed@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib