mathlib3

1c4e1843 - refactor(set_theory/basic): match `x < ℵ₀` lemmas with `x ≤ ℵ₀` lemmas (#15662)

refactor(set_theory/basic): match `x < ℵ₀` lemmas with `x ≤ ℵ₀` lemmas (#15662) * Mark `cardinal.lt_aleph_0_iff_set_finite` as `@[simp]` lemma. * Add `cardinal.lt_aleph_0_iff_subtype_finite` and `cardinal.mk_le_aleph_0_iff`; drop `cardinal.encodable_iff`. * Rename `cardinal.mk_set_le_aleph_0` to `cardinal.le_aleph_0_iff_set_countable`. * Rename `cardinal.mk_subtype_le_aleph_0` to `cardinal.le_aleph_0_iff_subtype_countable`. * Make `first_order.language.countable` protected. * Use `[countable _]` instead of `[encodable _]` or `[nonempty (encodable _)]` here and there. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>