toLex in decreasing_by

Stream: mathlib4

[Violeta Hernández]

This code snippet is behaving a bit weirdly:

import Mathlib.Order.Synonym

def foo : ℕ → ℕ → ℕ
  | 0, _ => 0
  | m + 1, n => foo m n
termination_by m n => toLex (m, n)
decreasing_by sorry

[Violeta Hernández]

Putting the cursor right after decreasing_by reveals the goal to be

sizeOf (toLex (m, n)) < sizeOf (toLex (a✝¹, a✝))

rather than the expected toLex (m, n) < toLex (m + 1, n)

[Violeta Hernández]

Is there no WellFoundedRelation instance on Lex (α × β)?

[Violeta Hernández]

By the way, I get that in this example I can just use termination_by m n => (m, n) to the same effect, but in my actual use case that doesn't quite work

[Violeta Hernández]

Apparently no, there isn't, and yes, adding one fixes the issue