Lean name clash with Mathlib surfaces only when the root file imports both

A new file defined ModuleCat.isFG, which Mathlib already defines in Mathlib.Algebra.Category.FGModuleCat.Basic. Building the file alone (lake build MyLib.File, or lake env lean File.lean) succeeded because that Mathlib module was not in its import closure; the failure only appeared when the library root imported both: import ... failed, environment already contains 'ModuleCat.isFG' from Mathlib.... Before naming a new def in a Mathlib namespace, grep the whole Mathlib tree (grep -rn 'def ModuleCat.isFG\|def isFG' .lake/packages/mathlib/Mathlib), and always run the root build before declaring a file done. Here the Mathlib def was identical, so the fix was to reuse it (FGModuleCat R is its full subcategory).