Lean 4 module system: public imports needed for names used in exposed proofs

In a module file with @[expose] public section, a lemma like Real.hasDerivAt_sqrt can elaborate fine in a non-module scratch file (plain import) yet fail with Unknown identifier once moved into the module, because its defining file (Mathlib.Analysis.SpecialFunctions.Sqrt) was only a transitive, non-public import. Fix: add an explicit public import of the file that declares the lemma. When porting scratch code into a module, budget one rebuild for missing imports and grep the Mathlib tree for the declaring file of each Unknown identifier.