refactor(order): order_{top,bot} as mixin (#10097)
This changes `order_top α` / `order_bot α` to _require_ `has_le α` instead of _extending_ `partial_order α`.
As a result, `order_top` can be combined with other lattice typeclasses. This lends itself to more refactors downstream, such as phrasing lemmas that currently require orders/semilattices and top/bot to provide them as separate TC inference, instead of "bundled" classes like `semilattice_inf_top`.
This refactor also provides the basis for making more consistent the "extended" algebraic classes, like "e(nn)real", "enat", etc. Some proof terms for lemmas about `nnreal` and `ennreal` have been switched to rely on more direct coercions from the underlying non-extended type or other (semi)rings.
Modify `semilattice_{inf,sup}_{top,bot}` to not directly inherit from
`order_{top,bot}`. Instead, they are now extending from `has_{top,bot}`. Extending `order_{top,bot}` is now only possible is `has_le` is provided to the TC cache at `extends` declaration time, when using `old_structure_cmd true`. That is,
```
set_option old_structure_cmd true
class mnwe (α : Type u) extends semilattice_inf α, order_top α.
```
errors with
```
type mismatch at application
@semilattice_inf.to_partial_order α top
term
top
has type
α
but is expected to have type
semilattice_inf α
```
One can make this work through one of three ways:
No `old_structure_cmd`, which is unfriendly to the rest of the class hierarchy
Require `has_le` in `class mwe (α : Type u) [has_le α] extends semilattice_inf α, order_top α.`, which is unfriendly to the existing hierarchy and how lemmas are stated.
Provide an additional axiom on top of a "data-only" TC and have a low-priority instance:
```
class semilattice_inf_top (α : Type u) extends semilattice_inf α, has_top α :=
(le_top : ∀ a : α, a ≤ ⊤)
@[priority 100]
instance semilattice_inf_top.to_order_top : order_top α :=
{ top := ⊤, le_top := semilattice_inf_top.le_top }
```
The third option is chosen in this refactor.
Pulled out from #9891, without the semilattice refactor.
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
