Commit 2022-07-20 16:22 309f7594

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.