Improve the pretty-printing of coerced machine integers

[sonmarcho]

If x is a machine integer (e.g., U32), Lean often displays x coerced to Int as x.val instead of ↑x. This can make the proof states quite difficult to parse, even when they are small. For instance, see the difference between this context:

x : U32
h : 2 * x.val + 1 ≤ U32.max
i : U32
_¹ : i.val = x.val + x.val
i' : U32
_ : i'.val = i.val + 1#u32.val

and this context:

x : U32
h : 2 * ↑x + 1 ≤ U32.max
i : U32
_¹ : ↑i = ↑x + ↑x
i' : U32
_ : ↑i' = ↑i + ↑1#u32