Commit 2026-01-09 20:29 b8e3880e

chore: run the new shake tool (#32731) This is a first candidate run of the new module-aware Shake on Mathlib. It has been run manually on nightly-testing-green and then rebased onto master as some Lean-side changes to be released in the next RC are needed. Known limitations:

• If a command attribute [attr] decl is imported, the import will be preserved if decl is referenced in any way in the file. This is a conservative approximation that avoids having to extend every single attribute implementation with precise tracking but may lead to redundant imports especially if often-used declarations such as id are tagged.