instance search sees through type synonyms

Stream: mathlib4

[Jireh Loreaux]

on mathlib4#783 I ran into a very concerning issue. The declaration toLex_mono (and similarly toLex_strictMono) picks up the wrong Preorder instance on α ×ₗ β despite having the type annotation toLex : α × β → α ×ₗ β. It instead uses the non-lexicographic preorder (i.e., the prod preorder) on α ×ₗ β. This seems like a bug and an important one to fix (it took me a while to figure out this was the problem when the proof was just randomly broken). I don't think Lean should be blasting right through type synonyms on its type class search.

[Scott Morrison]

Hopefully this is covered by https://github.com/leanprover/lean4/issues/1891, for which we'll have a fix tomorrow.

[Scott Morrison]

It is at least a related error, but I haven't thought about whether it applies here.

[Jireh Loreaux]

That seems like the same issue, thanks.