mathlib

aed4c494 - refactor(data/{finite,fintype}): move some lemmas to `data.fintype.basic` (#15626)

refactor(data/{finite,fintype}): move some lemmas to `data.fintype.basic` (#15626) We should have lemmas like `nonempty_fintype` in `fintype.basic` to replace `[fintype _]` by `[finite _]` in the assumptions. This PR doesn't fix any assumptions to keep it small.