Simple question: create a new variable inside a proof?

Stream: new members

[Nicholas Dyson]

Sorry about my stupid questions.
Suppose my current state is something like:

x y z: some_type
⊢ (x + y) + (x + y) = z

Is there a way that I can, within my proof and without defining any new functions outside my proof, go to a state like:

x y z a: some_type
definition_of_a : a = (x + y)
⊢ a + a = z

Obviously in that simple example it's not especially useful, but in a more realistic case we might have some very complicated expression that occurs multiple times within the target, ergo folding it down to a single variable (while keeping the definition of that variable so we unfold it later) will make life much easier.

[Eric Wieser]

set a := x + y with definition_of_a

[Nicholas Dyson]

Sick, knew there was probably a straightforward tactic for that but couldn't find it. TY TY.