mathlib

7428bd9b - refactor(data/finite/set,data/set/finite): move most contents of one file to another (#15166)

refactor(data/finite/set,data/set/finite): move most contents of one file to another (#15166) * move most content of `data.finite.set` to `data.set.finite`; * use `casesI nonempty_fintype _` instead of `letI := fintype.of_finite`; sometimes it lets us avoid `classical.choice`; * merge `set.finite.of_fintype`, `set.finite_of_fintype`, and `set.finite_of_finite` into `set.to_finite`; * rewrite `set.finite_univ_iff` and `finite.of_finite_univ` in terms of `set.finite`; * replace some assumptions `[fintype (plift _)]` with `[finite _]`; * generalize `set.cod_restrict` and some lemmas to allow domain in `Sort*`, use it for `finite.of_injective_finite.range`.