Hypotheses in branches

Stream: new members

[Graham Leach-Krouse]

When defining a function, is there a way to propagate the fact that a match occurred into a certain branch of a match ... with, in something like the way we can write if h : decidablefact then ... else ..., and use h for something like False.elim in the branches of the if?

[Eric Wieser]

match h : x with?

[Graham Leach-Krouse]

wonderful, thank you!

[Benjamin Jones]

Eric Wieser said:

match h : x with?

This is very helpful when providing have theorems inline in a match branch to later use in a termination proof. I was banging my head against the wall for a long time until I found this answer! Thank you.