fix: correctly apply hint priority (was always set to default 1000 due to a bug)

[euprunin]

Fixes #29831.

In addition to fixing the bug, this PR also adjusts the (now-working) tactic priorities to ensure that:

• bound is tested after aesop (bound calls aesop and is therefore stronger)
• group is tested after ring (group calls ring and is therefore stronger)

A bug in the parsing code below caused the priority value to be ignored, resulting in all hints using the default priority of 1000 regardless of the register_hint priority parameter:

elab (name := registerHintStx)
    "register_hint" p:("(" "priority" ":=" num ")")? tac:tactic : command =>
    liftTermElabM do
  -- remove comments
  let prio := match p with
    | some stx =>
        match stx.raw[3]?.bind Syntax.isNatLit? with
        | some n => n
        | none => 1000
    | none => 1000
  let tac : TSyntax `tactic := ⟨tac.raw.copyHeadTailInfoFrom .missing⟩
  addHint prio tac

Fixed by simplifying the syntax to take a mandatory numeric priority argument and extracting it directly via prio.raw.isNatLit?, removing the index-based parsing and the silent fallback to 1000.

---

[github-actions]

PR summary f51758c0e7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[BoltonBailey]

Seems good to me. Is it worth adding new tests to the tests file that directly demonstrate the group/ring ordering etc.?