mathlib

bec3e595 - feat(data/finset): provide the coercion `finset α → Type*` (#7575)

feat(data/finset): provide the coercion `finset α → Type*` (#7575) There doesn't seem to be a good reason that `finset` doesn't have a `coe_to_sort` like `set` does. Before the change in this PR, we had to suffer the inconvenience of writing `(↑s : set _)` whenever we want the subtype of all elements of `s`. Now you can just write `s`. I removed the obvious instances of the `((↑s : set _) : Type*)` pattern, although it definitely remains in some places. I'd rather do those in separate PRs since it does not really do any harm except for being annoying to type. There are also some parts of the API (`polynomial.root_set` stands out to me) that could be designed around the use of `finset`s rather than `set`s that are later proved to be finite, which I again would like to declare out of scope.