mathlib

73ccd02e - refactor(set_theory/cardinal): review API about `#α = 2`/`nat.card α = 2` (#16899)

refactor(set_theory/cardinal): review API about `#α = 2`/`nat.card α = 2` (#16899) * Rename `cardinal.mk_eq_nat_iff_finset` to `cardinal.mk_set_eq_nat_iff_finset`, add a version for types and `cardinal.mk_eq_nat_iff_fintype`. * Add `cardinal.to_nat_eq_iff`, a more general version of `cardinal.to_nat_eq_one`. * Rename `cardinal.exists_not_mem_of_length_le` to `cardinal.exists_not_mem_of_length_lt`. * Add `cardinal.mk_eq_two_iff`, `cardinal.mk_eq_two_iff'`, `nat.card_eq_two_iff`, and `nat.card_eq_two_iff'`.