mathlib3

cd5cb441 - chore(set_theory/cardinal_ordinal): golf some proofs (#10260)