[Merged by Bors] - feat: port Order.BoundedOrder

[Ruben-VandeVelde]

• depends on: [Merged by Bors] - feat: port Order.Lattice #642
• depends on: [Merged by Bors] - chore(order/bounded_order): split mathlib#17730

Tracking mathlib commit: e50b8c261b0a000b806ec0e1356b41945eda61f7

[Ruben-VandeVelde]

Also todo: fix the Prop → PropCat translations

[kbuzzard]

Note that the mathlib3 splitting PR is now in the process of being merged. I think the next thing to do (which I'm happy to do) is to wait for mathlib3port to run on the now much shorter file and then to merge the results with the partial porting we have here.

[semorrison]

This PR/issue depends on:

• [Merged by Bors] - feat: port Order.Lattice #642
• [Merged by Bors] - chore(order/bounded_order): split mathlib#17730
  By Dependent Issues (🤖). Happy coding!

[Ruben-VandeVelde]

The remaining lint errors are these, which sound concerning:

/- The `synTaut` linter reports:
THE FOLLOWING DECLARATIONS ARE SYNTACTIC TAUTOLOGIES. This usually means that they are of the form `∀ a b ... z, e₁ = e₂` where `e₁` and `e₂` are identical expressions. We call declarations of this form syntactic tautologies. Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving basic facts using `rfl`, when elaboration results in a different term than the user intended. You should check that the declaration really says what you think it does. -/
-- Mathlib.Order.BoundedOrder
#check OrderTop.ext_top.{u_1} /- LHS equals RHS syntactically -/
#check OrderBot.ext_bot.{u_1} /- LHS equals RHS syntactically -/

/- The `unusedArguments` linter reports:
UNUSED ARGUMENTS. -/
-- Mathlib.Order.BoundedOrder
#check OrderTop.ext_top.{u_1} /- argument 3 A : OrderTop α -/
#check OrderBot.ext_bot.{u_1} /- argument 3 A : OrderBot α -/

[semorrison]

Great, thanks!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style