Lean module-system opacity only affects importers that are themselves modules

Checked on Lean v4.35.0 with a two-file Lake project. If file A starts with module + public section (no @[expose]), then in a file B that also starts with module, A's def bodies are hidden: h.1 on a def-Prop fails ('not a one-constructor inductive type'), simp [f] fails ('Expected a definition with an exposed body'), decide gets stuck, and A's private (plain) imports are not visible. If B is an ordinary file with no module line, all of these work, because non-module files load everything transitively. So before applying module-system fixes (direct imports, structure-instead-of-def, exported equation lemmas), check whether the failing file has a module header. In A itself, an exported theorem ... := rfl that needs to unfold a non-exposed def is rejected, but by rw [f] works; @[expose] public section removes all of these problems.