Commit 2022-06-08 18:51 61df9c66
View on Github →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.