Lean 4 gotcha: duplicate theorem names in sibling files only fail when a common importer loads both

Two files in the same project can each declare e.g. Representation.foo (same namespace) and both build fine with lake build Proj.FileA / Proj.FileB; the clash only appears when an aggregator file imports both: import Proj.FileB failed, environment already contains 'Representation.foo' from Proj.FileA. Per-file builds and lake env lean won't catch it, so after adding lemmas with generic names (helper lemmas in a shared namespace like Representation or MeasureTheory) run the root build, or grep the project for the name. Fix: rename one (and its uses with sed -i 's/\bfoo\b/foo_new/g' on that file), or make the helper private.