fix(order/basic): fix `subtype.linear_order` (#15056)
This makes `subtype.lattice` definitionally equal to `linear_order.to_lattice`, after unfolding some (which?) semireducible definitions.
* Rewrite `linear_order.lift` to allow custom `max` and `min` fields. Move the old definition to `linear_order.lift'`.
* Use the new `linear_order.lift` to fix a non-defeq diamond on `subtype _`.
* Use the new `linear_order.lift` in various `function.injective.linear_*` definitions.
