Replacing common subexpression

Stream: Is there code for X?

[Ayhon]

If I have a common subexpression which appears in many different places in my proof, how can I substitute it with a common variable? For instance, if I have (a+b)/2 in different areas of my codebase, I would like to do let mid := (a+b)/2 and have all appearances of (a+b)/2 substituted with mid. I have "loogled" for substitute, rename and fold (since it's opposite of unfold), but they don't seem to fit my usecase.

[Adomas Baliuka]

Use the tactic set

[Ayhon]

I feel like I should have found this sooner. Is there a glosary of tactics or a proper way to search for them? Because I couldn't find it at all, and it now seems to be pretty basic

[Ruben Van de Velde]

Not yet

[Ayhon]

And what is the opposite of set? Because unfold doesn't seem to be working for me, it says unknown constant 'mid'

[Daniel Weber]

You can use unfold_let

[Ruben Van de Velde]

Or use set x := .. with hx and rewrite with hx