Lean module system: `where` helpers of a theorem are not usable from other modules

In a Lean 4 module file (Mathlib v4.35 era), an auxiliary lemma declared with theorem foo ... := ... where bar ... := ... works inside the same file as foo.bar. From another module, Ns.foo.bar fails with 'Invalid field bar: The environment does not contain Exists.bar'. Lean parses it as a field projection on the proof of foo because the helper is not exported. Fix: hoist the helper to a top-level theorem in the public section. Related: a plain def in a module file has no exposed body, so other modules cannot rintro ⟨...⟩ or rw [MyDef] through it ('Expected a definition with an exposed body'). Mark Prop-valued predicate defs @[expose] if downstream files need to unfold them.