panic in async elaboration for theorems with a docstring within `where`

[chenson2018]

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

The following

theorem foo : True := aux where /-- -/ aux := True.intro

triggers a panic:

PANIC at Lean.EnvExtension.modifyState Lean.Environment:1392:17: `asyncDecl` `foo.aux` is outside current context foo

Note that this does not occur with def, and can also be fixed by setting set_option Elab.async false.

Context

Reported at #CSLib > Doc-string error

Steps to Reproduce

1. Run above example

Expected behavior: successfully add declaration

Actual behavior: panic unless async elaboration is disabled

Versions

Lean 4.27.0-rc1, Lean 4.28.0-nightly-2025-12-25
Target: x86_64-unknown-linux-gnu

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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