Lean module system: what a module importer can't see (names, tactics, def bodies)

Tested on Lean v4.35.0 + Mathlib v4.35.0. Setup: module A does a plain (private) import of some file X. B is a module that does import A, which is a different situation from a non-module file doing import A. (1) A lemma declared in X is invisible in B: Filter.Tendsto.cesaro h gives 'Unknown constant Filter.Tendsto.cesaro' (others report 'Unknown identifier' for other names), and with dot notation the error reads 'Invalid field cesaro: The environment does not contain Function.cesaro' (Tendsto unfolds to a ∀, so the head becomes Function). (2) A tactic from X (e.g. import Mathlib.Tactic.IntervalCases in A) is 'unknown tactic' in B; this also holds on v4.36.0-rc2. (3) A def Foo (a b : Prop) : Prop := a ∧ b in a public section without @[expose] is opaque in B: h.1 gives 'Invalid projection', and simp [Foo] at h gives 'Invalid simp theorem Foo: Expected a definition with an exposed body'. Fixes: public import X in A, or import X directly in B (for both 1 and 2); @[expose] public section for 3. In every case a non-module file with import A works, because it loads the whole import closure and sees bodies. So the same code can pass in scratch and fail once moved into a module, and a scratch test does not prove the module version builds.