mathlib

e0b153b2 - refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4762)

refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4762) The main non-bc change in Lean 3.22.0 is leanprover-community/lean#484 which merges `linear_order` with `decidable_linear_order`. This is the `mathlib` part of this PR. ## List of API changes * All `*linear_order*` typeclasses now imply decidability of `(≤)`, `(<)`, and `(=)`. * Drop `classical.DLO`. * Drop `discrete_linear_ordered_field`, use `linear_ordered_field` instead. * Drop `decidable_linear_ordered_semiring`, use `linear_ordered_semiring` instead. * Drop `decidable_linear_ordered_comm_ring`, use `linear_ordered_comm_ring` instead; * Rename `decidable_linear_ordered_cancel_add_comm_monoid` to `linear_ordered_cancel_add_comm_monoid`. * Rename `decidable_linear_ordered_add_comm_group` to `linear_ordered_add_comm_group`. * Modify some lemmas to use weaker typeclass assumptions. * Add more lemmas about `ordering.compares`, including `linear_order_of_compares` which constructs a `linear_order` instance from `cmp` function. Co-authored-by: Johan Commelin <johan@commelin.net>