mathlib3

b6395b3a - refactor(set_theory/*): change `omega` to `aleph_0` + golf (#14467)

refactor(set_theory/*): change `omega` to `aleph_0` + golf (#14467) This PR does two things: - we change `cardinal.omega` to `cardinal.aleph_0` and introduce the notation `ℵ₀`. - we golf many proofs throughout