feat: add simp_digits tactic

[dwrensha]

With the introduction of the simprocs reduceLE, reduceMod, reduceDiv etc. in Lean v4.6.0, now simp
can fully normalize typical Nat.digits calls that have concrete arguments. The situation is still a bit delicate
however, as we want to avoid invoking kernel reduction on Nat.digits, because the Acc-based ("well founded")
recursion in digitsAux can get bogged down.

This PR introduces a new tactic simp_digits tactic that contains only the simp lemmas and simprocs needed
to reduce Nat.digits. This allows proofs involving Nat.digits to be cleanly factored into two steps:

1. reduce Nat.digits via simp_digits,
2. do things that require kernel reduction such as simp_arith, decide, or rfl.

---

[dwrensha]

It would be nicer to make this a proper simp set via register_simp_attr, but as far as I can tell simprocs (like reduceLE, reduceMod...) cannot be added to simp sets (they seem to just get silently ignored).

[dwrensha]

Maybe norm_num by itself is good enough: #10429