mathlib3

a54e63da - feat(set_theory/ordinal/basic): basic lemmas on `ordinal.lift` (#15146)

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.