Commit 2022-08-18 18:40 3bfa4496

feat(Mathlib/Order/Basic): port most of data/order/basic.lean (#348) Ports most of data/order/basic.lean from mathlib3, leaving a few TODOs. This file lives near the base of the file-import dependency graph; having it ported should enable more experimentation with higher-level parts of the algebraic hierarchy. Some challenges that came up:

• Lean 4 defines max and min in the prelude, while Lean 3 (as of https://github.com/leanprover-community/lean/pull/609) defines them differently as part of linear_order. We will need to figure out how to resolve this conflict.
• In Lean 3, the lexicographic order on products uses a wrapper type lex α β. In Lean 4, the prelude instance instLTProd defines the lexicographic order directly on α × β. In this PR, I needed to verbosely disambiguate which instance to use.