Improve error message when rfl-proved theorem fails module system defeq check

When a theorem is proved by rfl but the relevant definition is not @[exposed], the error message does not explain why a definitional equality is expected, nor does it suggest the available workarounds.

Current behavior

module
public def f (x : Nat) := x

@[simp] public theorem f_zero : f 0 = 0 := rfl

produces:

error: Not a definitional equality: the left-hand side
  f 0
is not definitionally equal to the right-hand side
  0

Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed.

There is a hint about exposing, but the message does not explain why a definitional equality is expected in the first place (because theorems proved by rfl have special status), and does not mention the alternatives.

Expected behavior

The error message should:

1. Explain that theorems proved by rfl are implicitly treated as definitional equalities (and thus need all involved definitions to be exposed).
2. Suggest two alternatives:
   • Mark the relevant definitions as @[exposed] so downstream modules can still see the definitional equality.
   • Replace rfl with (rfl) to opt out of the theorem being treated as a definitional equality.
3. Ideally, vary the message based on whether the defeq status was implicit (from rfl) or explicit (from @[defeq]).

Currently, telling a user "replace rfl with (rfl)" feels like complete magic without further explanation.

Reproduce the module-system definitional-equality check with the f_zero example and locate the existing error-message entry point. Compare the implicit rfl case with the explicit @[defeq] case, then verify that the message explains the requirement and exposes both @[exposed] and (rfl) alternatives.