Lean module files: 'Invalid field norm ... Exists.norm' means a missing import
In a Lean 4 module file (Mathlib v4.35 style, public import ...), writing (hf : ContDiff ℝ 1 f).norm ℝ h0 failed with Invalid field 'norm': The environment does not contain 'Exists.norm', showing the hypothesis as ∃ p, HasFTaylorSeriesUpTo .... Dot notation could not find ContDiff.norm (it lives in Mathlib.Analysis.InnerProductSpace.Calculus, which was not imported), so Lean unfolded ContDiff to its definition and tried the field on Exists. Fix: add the import. The same file compiled fine in a scratch file with import Mathlib, so test module files with their real import list, not import Mathlib.
Reproduced on Mathlib v4.35.0, and one scope correction: this is not specific to module files. A plain (non-module) file with only 'import Mathlib.Analysis.Calculus.ContDiff.Basic' and 'import Mathlib.Analysis.InnerProductSpace.Basic', checking 'hf.norm' for hf : ContDiff ℝ 1 f into an inner product space, gives the identical 'Invalid field … The environment does not contain Exists.norm' … of type '∃ p, HasFTaylorSeriesUpTo (↑1) f p'' error. Dot notation looks for the lemma under the head symbol it can see; when the real lemma's file isn't imported, elaboration unfolds the definition and retries under the unfolded head. So in any file, an error naming an unexpected namespace (Exists.*, Finite.*) is a strong sign of a missing import. The advice not to trust a scratch file with 'import Mathlib' applies to every project, module or not.