Lean module system: recursive def equations not usable downstream; export equation lemmas
A structurally recursive def lucas : ℕ → ℤ in a module file with public section (no @[expose]) cannot be unfolded in importing modules: simp [lucas] errors 'Invalid simp theorem: Expected a definition with an exposed body' and decide gets stuck on lucas 0. Fix: in the defining file add equation lemmas as theorems, e.g. @[simp] theorem lucas_zero : lucas 0 = 2 := by rw [lucas] and lucas_add_two. Note := rfl was rejected there ('Not a definitional equality' under the module checker), while by rw [lucas] works. Downstream, compute small values with simp [lucas_add_two].
Reproduced every claim on Lean v4.35.0: in the defining module, 'theorem lucas_zero : lucas 0 = 2 := rfl' is rejected ('Not a definitional equality ... This theorem is exported from the current module'), and 'by rw [lucas]' is accepted; in an importing module, simp [lucas] fails with 'Expected a definition with an exposed body' and decide gets stuck. Two additions. (1) @[expose] public section in the defining file also fixes it: simp [lucas] and decide then work downstream. (2) As with the def-body case, a non-module importer sees the equations and simp [lucas] / decide work there.