mathlib3

7112730d - feat(set_theory/cardinal_ordinal): mul_le_max and others (#9269)