Renaming terms for calc proof

Stream: new members

[Adrian Wüthrich]

Is there a way of renaming terms in a calc proof in order to increase readability and make lines shorter? For example if I had a goal containing SimpleGraph.lapMatrix G R I'd like to denote this term by just L.

[Kevin Buzzard]

What happens if you just write let L := SimpleGraph.lapMatrix G R before the calc block?

[Adrian Wüthrich]

That does indeed work. It adds L to the context and then it can be used in calc, thanks!

[Kevin Buzzard]

If you need the definition of L in your local context (for example, for rewriting) you can use set L := ... with hL.

[Adrian Wüthrich]

This is even better, exactly what I was looking for.