feat: unexpand Vector.mk #[...] _ to #v[...]

[Rob23oba]

This PR adds an unexpander for Vector.mk that unexpands Vector.mk #[...] _ to #v[...].

-- previously:
#check #v[1, 2, 3] -- { toArray := #[1, 2, 3], size_toArray := ⋯ } : Vector Nat 3
-- now:
#check #v[1, 2, 3] -- #v[1, 2, 3] : Vector Nat 3

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 528fe0b0ed673accd37d986d80a7c49f876a3087 --onto c8290bd94221f41ae49899f0f7de71b52724ad7e. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-18 10:21:32)

[eric-wieser]

Any reason for this to be in the root namespace?

Suggested change

	def _root_.unexpandVectorMk : Lean.PrettyPrinter.Unexpander
	def unexpandMk : Lean.PrettyPrinter.Unexpander

[Rob23oba]

Because all the other ones are (e.g. unexpandListCons is not in the List namespace)