mathlib

309f7594 - feat(set_theory/ordinal/basic): dot notation lemmas + golf (#15348)

feat(set_theory/ordinal/basic): dot notation lemmas + golf (#15348) We introduce dot notation lemmas for proving something of the form `type r < type s` or `type r ≤ type s` by providing a principal segment, an initial segment, or a relation embedding. We rename `type_le` and `type_le'` to `type_le_iff` and `type_le_iff'` for consistency with `type_lt_iff` (which can't be renamed to `type_lt`, as this is an existing theorem about `type (<)`). We could introduce `lift` variants of these, but I'd rather wait until #15041 is merged, at which point I can do the analogous refactor on ordinals.