mathlib3

4050b906 - refactor(data/set/countable): golf using `_root_.countable`, review API (#15624)

refactor(data/set/countable): golf using `_root_.countable`, review API (#15624) * add `set.countable_coe_iff`, `set.countable.to_subtype`, `set.to_countable`, `set.countable_univ`, `countable.to_set`, `set.countable.exists_surjective`; * generalize some lemmas from `[encodable]` to `[countable]`; * move `section enumerate` up to use it in `countable_iff_exists_subset_range`; * golf some proofs using facts about `_root_.countable`; * drop `countable_encodable` and `countable_encodable'`, use `set.to_countable` instead.