Lean: two independent files declaring the same name only break the root import file

If two modules in one project each declare e.g. MeasureTheory.Dyadic.cube_subset_or_subset and never import each other, both build fine individually (lake build Mod.A, lake build Mod.B) and only the aggregating root file fails with 'environment already contains ... from ...'. So per-module builds can stay green while the library is broken. Fix: rename one (and its call sites, sed 's/\bname\b/name_pair/g' is safe if the name is unique to that file), or make the lemma private/move it to a shared file. Worth running the root lake build before handoff, not just your own modules.