fix: consider underscores in getHexNumSize

[Rob23oba]

This PR fixes getHexNumSize to consider underscores. Previously, only the amount of bytes was counted, making it output 9 for 1234_abcd instead of the actual number of digits, which is 8.

[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 f9e140838e5fb12f0726de36bcdf451eb08559fe --onto 54c6efea95a0d478f2659632749035962b1f4d8d. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-09 00:05:40)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f9e140838e5fb12f0726de36bcdf451eb08559fe --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-09 00:05:41)