The tactic bundle

Mathlib is a library of Lean modules, and a module re-exports only what it imports with public import; Mathlib imports the tactic modules it uses in proofs privately wherever it can. A non-module file saw every tactic in its transitive closure; a module of this repository sees a tactic only along a public path, and norm_num reached Foundations/Halting/Descriptions.lean along none (2026-09-28, the module-system PR of planning/palomar.md). So every module that imports part of Mathlib, rather than the Mathlib umbrella, also imports this bundle, which re-exports the common tactics and the heavy ones the library uses; scripts/modularize.py inserts the line and --check (CI) reports a file without it.