refactor(data/set/finite): use a custom inductive type (#9164)
Currently Lean treats local assumptions `h : finite s` as local instances, so one needs to do something like
```lean
unfreezingI { lift s to finset α using hs },
```
I change the definition of `set.finite` to an inductive predicate that replicates the definition of `nonempty` and remove `unfreezingI` here and there. Equivalence to the old definition is given by `set.finite_def`.
