fix: pretty-printing of unification hints

[grunweg]

This PR ensures that pretty-printing of unification hints inserts a space after |- resp. ⊢.

All uses in Lean core and mathlib add a space after the |- or ⊢ symbol; this makes the output match usage in practice.
This was discovered in leanprover-community/mathlib4#30658, adding a formatting linter using pretty-printing as initial guide.

[grunweg]

awaiting-review

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-12-23 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-23 11:40:15)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-23 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-23 11:40:17)