feat(set_theory/ordinal/basic): improve docs on `lift`, add `simp` lemmas (#14599)
feat(set_theory/ordinal/basic): improve docs on `lift`, add `simp` lemmas (#14599)

This is pretty much the same thing as #14596, just on `ordinal.lift` instead of `cardinal.lift`.





leanprover-community/mathlib,leanprover-community/mathlib