Difficulty synthesizing `LE (α ×ₗ β)`

Stream: mathlib4

[Scott Carnahan]

I see an explicit instance in docs#Prod.Lex.instLE but I am unable to make it fire. (I don't mind assuming [Preorder α] for my work but this seems strange to me)

import Mathlib.Data.Prod.Lex

variable {α β : Type*} [LE α] [LE β] -- change [LE α] to [Preorder α] to succeed.

#synth LE (α ×ₗ β)

[Yakov Pechersky]

Note that the first type needs an LT

[Yakov Pechersky]

That's why Preorder works, because you get a LT as well.

[Scott Carnahan]

Oh, I see it now! Thank you!

[Yakov Pechersky]

BTW if you're working with Lex, you might like #22420

[Yakov Pechersky]

It has
def Prod.Lex.orderHom {α β : Type*} [PartialOrder α] [Preorder β] :
α × β →o α ×ₗ β where