mathlib3

61df9c66 - feat(set_theory/ordinal/basic): tweak `type_def` + golf `type_lt` (#14611)

feat(set_theory/ordinal/basic): tweak `type_def` + golf `type_lt` (#14611) We replace the original, redundant `type_def'` with a new more general lemma. We keep `type_def` as it enables `dsimp`, unlike `type_def'`. We golf `type_lt` using this new lemma.