Replace variable with its definition

Stream: lean4

[Op From The Start]

I have a goal of:

⊢ (birthday x).nadd (birthday (yRS yr)) < (birthday (PreNo.mk xL xR xLS xRS)).nadd (birthday (PreNo.mk yL yR yLS yRS))

and I know that x=PreNo.mk xL xR xLS xRS because the latter was made by matching on x. How can I use the definition of x to simplify the inequality?

[Aaron Liu]

I don't think you can

[Aaron Liu]

maybe with match hx : x with

[Aaron Liu]

that will give you a hypothesis called hx saying that x is equal to the match pattern

[Op From The Start]

That worked, thank you.