What are the different notions of equality in Lean?

Stream: general

[nrs]

I'm getting a bit confused about normalization and canonical forms in programming languages in general, so specifically about Lean too. I'm trying to capture when equality also means that there has been computations between the terms that are said to be equal. Concretely, in Lean, can we distinguish:

1. Equality between non-value expressions (by non-value expressions I mean expressions that have at least one more reduction)
2. Equality between values
3. Equality between a value and a non-value?

And are these notions of equality purely internal or do some of these belong to the metatheory of Lean?