mathlib

6eeb941c - refactor(set_theory/cardinal/basic): migrate from `fintype` to `finite` (#15175)

refactor(set_theory/cardinal/basic): migrate from `fintype` to `finite` (#15175) * add `finite_iff_exists_equiv_fin`; * add `cardinal.mk_eq_nat_iff` and `cardinal.lt_aleph_0_iff_finite`; * rename the old `cardinal.lt_aleph_0_iff_finite` to `cardinal.lt_aleph_0_iff_finite_set`; * rename `cardinal.lt_aleph_0_of_fintype` to `cardinal.lt_aleph_0_of_finite`, assume `[finite]` instead of `[fintype]`; * add an alias `set.finite.lt_aleph_0`; * rename `W_type.cardinal_mk_le_max_aleph_0_of_fintype` to `W_type.cardinal_mk_le_max_aleph_0_of_finite`, fix assumption.