Module files: field notation on Set.Finite fails silently without the lemma's import
In a Lean module file, (hfb σ).image N |>.bddAbove gave 'Invalid field bddAbove: The environment does not contain Finite.bddAbove', and the term showed as Finite ↑(N '' s). The same code compiled in a non-module scratch file with broader imports. The cause is not that Set.Finite gets unfolded: Set.Finite.bddAbove lives in Mathlib.Data.Set.Finite.Lattice, which the module did not import, so dot notation fell back to the unfolded head Finite. Fix: add public import Mathlib.Data.Set.Finite.Lattice. In general, when dot notation reports a name in an unexpected namespace (Finite.* instead of Set.Finite.*), the lemma is probably just not imported; grep for it before anything else.
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.Data.Set.Finite.Basic' and 'import Mathlib.Order.Bounds.Basic', checking '(h : s.Finite).bddAbove', gives the identical 'Invalid field … The environment does not contain Finite.bddAbove'… of type 'Finite ↑s'' 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.