feat(logic/is_empty): Add is_empty typeclass (#7606)
* Refactor some equivalences that use `empty` or `pempty`.
* Replace `α → false` with `is_empty α` in various places (but not everywhere, we can do that in follow-up PRs).
* `infinite` is proven equivalent to `is_empty (fintype α)`. The old `not_fintype` is renamed to `fintype.false` (to allow projection notation), and there are two useful variants `infinite.false` and `not_fintype` added with different arguments explicit.
* add instance `unique true`.
* Changed the type of `fin_one_equiv` from `fin 1 ≃ punit` to `fin 1 ≃ unit` (it was used only once, where the former formulation required giving an explicit universe level).
* renamings:
`equiv.subsingleton_iff` -> `equiv.subsingleton_congr`
`finprod_of_empty` -> `finprod_of_is_empty`
