chore: remove redundant imports in core

[Kha]

No description provided.

[Kha]

!bench

[leanprover-radar]

Benchmark results for 9c2fda2 against 316859e are in! @Kha

[leanprover-bot]

Here are the benchmark results for commit 9c2fda2.
There were significant changes against commit 316859e:

  Benchmark      Metric          Change
  ===============================================
+ channel.lean   boundedn_seq     -1.1%
- channel.lean   unbounded_seq     2.2%
+ lake env       instructions     -2.3% (-28.9 σ)

[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 316859e87167dcb8a7f7ada18b241ab7c0135f43 --onto 0dc862e3eda618869c80d4e559e6be3ce7fc8c85. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-12 12:34:27)

[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 316859e87167dcb8a7f7ada18b241ab7c0135f43 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-12 12:34:28)