chore: basic ExtraModUses

[Kha]

Part of #10575 landed early for regression bisecting

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit dd478a6.
The entire run failed.
Found no significant differences.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 641ea91.
There were significant changes against commit 69c8f13:

  Benchmark      Metric         Change
  ====================================
- channel.lean   boundedn_seq     1.1%

[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 69c8f13bf21a4a86000ca9f3f7288fad579de45b --onto ac0b82933f6eac9914011ca2caf38d0e4e991160. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-27 17:14:59)

[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 69c8f13bf21a4a86000ca9f3f7288fad579de45b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-27 17:15:01)