Commit 2024-11-04 23:57 b1a98054

chore(SetTheory/Ordinal/Basic): group typein and enum theorems together (#16963) We previously had two separate sections with lemmas about typein and enum, since we defined the linear order instance relatively late in the file. Thanks to #16401, we can group almost all of these lemmas together. The remaining ones will be deprecated in a separate PR, for separate reasons.