mathlib3

9dba31df - chore(set_theory/cardinal/basic): missing lemmas about `<`/`≤` and `lift c`/`↑n` (#18752)