`local elab` cannot use privately imported meta defs

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

A local elab command cannot use privately imported meta definitions, in contrast to local elab_rules and local macro.

A.lean:

module
public import Lean

public meta def myZeroExpr : Lean.Expr := Lean.mkNatLit 0

B.lean:

module
public import Lean
import MyNightlyTesting.A -- NO `public`

/- Invalid public `meta` definition
`_aux_MyNightlyTesting_B___elabRules__private_MyNightlyTesting_B_0_termMyZero_1`,
`myZeroExpr` is not accessible here; consider adding `public import MyNightlyTesting.A` -/
local elab "myZero" : term => pure myZeroExpr

Context

This issue prevents modulizing Mathlib tests in leanprover-community/mathlib4#34466.

Versions

Lean 4.31.0-nightly-2026-04-08
Ubuntu 24.04.4

Additional Information

The fix for this issue is easy, I will create the PR soon.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal reproduction in A.lean and B.lean, focusing on the local elab command, private import, and meta definition. Run the example against the specified Lean nightly and confirm that local elab can use the privately imported meta definition without the invalid-public error.