Commit 2022-11-29 20:45 463b024d

feat(Data.Prod.Lex): port file (#783) mathlib3 SHA: 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a porting notes: there are several issues here that should probably be fixed before this gets merged

1. Prod.Lex is not protect in core, so when you have this namespace open and try to refer to Lex, Lean finds Prod.Lex instead of _root_.Lex. This is not a huge deal since we have notation α ×ₗ β, but we should probably ask for it to be protected in core. See https://github.com/leanprover/lean4/pull/1895
2. on the declarations toLex_mono and toLex_strictMono, Lean sees right through the type synonym α ×ₗ β to α × β and uses the wrong Preorder instance, which is why I had to provide them manually. I think this is a bug and should be fixed, otherwise it will cause loads of other issues down the road (for other type synonyms) and the errors will be hard to diagnose. EDIT: Hopefully https://github.com/leanprover/lean4/issues/1891 will provide a fix.
3. I had to provide the definitions of min and max for the LinearOrder instance manually because in Lean 4 we have the classes Min and Max which have no counterpart in Lean 3. In this case it's a bit annoying because ite requires decidability, so I effectively had to provide that three times in this instance declaration. Surely there should be a better way?