Commit 2022-07-06 21:58 a54e63da

feat(set_theory/ordinal/basic): basic lemmas on ordinal.lift (#15146) We add some missing instances for preimages, and missing theorems for ordinal.lift. We remove ordinal.lift_type, as it was just a worse way of stating ordinal.type_ulift. We also tweak some spacing and golf a few theorems. This conflicts with (and is inspired by) some of the changes of #15137.