Is there a way to use equality of pattern in the case?

Stream: lean4

[James Browning]

Suppose I have:

match n with
| 0 => expr1
| m+1 => expr2

Is it possible to somehow capture the fact that m+1 = n and use it in expr2? (Specifically I want m < n, but this is trivial with the equality and ▸)

[Calvin Lee]

Yes, if I recall the syntax correctly then

match h : n with
| 0 => expr1 -- h : n = 0
| m+1 => expr2 -- h : n = m + 1

[James Browning]

Awesome, exactly what I wanted thanks