mathlib

d136cd55 - chore(data/pi/lex): turn `pi.lex.linear_order` into an instance (#14389)

chore(data/pi/lex): turn `pi.lex.linear_order` into an instance (#14389) * Use `[is_well_order ι (<)]` instead of `(wf : well_founded ((<) : ι → ι → Prop))`. This way `pi.lex.linear_order` can be an instance. * Add `pi.lex.order_bot`/`pi.lex.order_top`/`pi.lex.bounded_order`.