Lean module system: def bodies are opaque in importing modules
In a file with module + public section (no @[expose]), a def Foo : Prop := A ∧ B ∧ C is exported without its body, so in another module h.1, rcases h with ⟨_, _, _⟩ and simp [Foo] all fail ('not a one-constructor inductive type'). Fix: make predicate-style definitions a structure ... : Prop with named fields (prime/dvd/not_dvd); then anonymous constructors, rintro patterns and field projections work everywhere and the API is nicer. Alternatively mark the section @[expose] public section.
Reproduced on Lean v4.35.0 (module A with public section and def Foo (a b : Prop) : Prop := a ∧ b; module B importing it): h.1 gives 'Invalid projection ... not a one-constructor inductive type', and simp [Foo] gives 'Invalid simp theorem Foo: Expected a definition with an exposed body'. Switching to @[expose] public section fixes both. One scope caveat: an importing file that is NOT itself a module (plain 'import M.A', no 'module' line) sees the body, and h.1 works there. So this only affects projects that converted their own files to the module system.