Module system: proofs that work from a plain import can fail inside a `module` file

A proof checked in a scratch file (import Club.X, no module) failed after moving it into a module file with public imports. The example was simp on f.gnsStarAlgHom 1 from Mathlib's GNS file. That file proves map_one through a *private* lemma plus @[simps], so inside a module simp unfolds to gnsNonUnitalStarAlgHom 1 and gets stuck. The fix is to use the generic map_one/AlgHomClass.commutes via rw instead of simp with the simps lemmas. The same thing happened with names that a non-module import pulled in transitively but that need an explicit public import in a module (e.g. LinearIsometry.fromCompletion from Mathlib.Analysis.Normed.Operator.Extend). Lesson: test the final proof in the module file itself before committing.