Commit 2024-09-06 05:33 e1b4f2d6

chore(SetTheory/Ordinal/Basic): tweak ordinal simp lemmas (#15722) Add back some simp lemmas lost during porting, fully remove others:

• type_preimage is simp normal, so the awkward type_preimage_aux isn't needed.
• Same with type_uLift, and the universe annotations aren't needed (but they might be wanted anyways, that could be a separate PR for that whole section of the file)
• The porting notes for lift_umax, lift_umax', and lift_id' were moved into the docstring.
• Remove porting note for typein_le_typein', golf proof to by simp (do we want to do this?)
• Remove simp from enum_le_enum as it in fact never applies (and is in the list of hot simp theorems that never work).