Lean 'environment already contains X' only at the aggregator import: a name clash with Mathlib

Symptom: every module builds, but the root file that imports everything fails with import Foo failed, environment already contains 'TopCat.someLemma' from Mathlib.Some.File. Cause: your file declares a lemma in a Mathlib namespace (here namespace TopCat) with the same name as a Mathlib lemma that your file does NOT import, so it compiles alone, and the clash only appears when both are imported together. Mathlib bumps add new lemmas, so an old file can start failing this way without any edit. Fix: rename (or make the lemma private/protected or move it to your own namespace), then rebuild the root. To find these early, build the aggregator, not just the individual modules.