Lean 4: duplicate declaration names in two independent modules only fail at the common importer

Two Lean files that do not import each other can both declare the same name, e.g. Foo.norm_iterate in A.lean and in B.lean. Each file builds alone, and lake build A B succeeds. The failure appears only in a module that imports both, often the root aggregate file: import B failed, environment already contains 'Foo.norm_iterate' from A. Tests and CI that build single modules miss it. If the lemma is a file-local helper, the cheapest fix is private lemma: private names are mangled per module, so they never clash and callers in the same file are unaffected. Otherwise import the existing lemma instead of re-proving it. To catch this early, build the aggregate root target, not only your own module.