diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 32bfaea30a7b..4b305273a223 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -1357,11 +1357,9 @@ def asyncMayModify (ext : EnvExtension σ) (env : Environment) (asyncDecl : Name
     -- common case of confusing `mainEnv` and `asyncEnv`.
     | .async .mainEnv => ctx.mayContain asyncDecl && ctx.declPrefix != asyncDecl
     -- The async env's async context should either be `asyncDecl` itself or `asyncDecl` is a nested
-    -- declaration that is not itself async. Note: we use `.all` rather than `.any` to also allow
-    -- modifying state for nested declarations that haven't been added to `asyncConsts` yet (e.g.,
-    -- `let rec` declarations with docstrings within `where` clauses).
+    -- declaration that is not itself async.
     | .async .asyncEnv => ctx.declPrefix == asyncDecl ||
-      (ctx.mayContain asyncDecl && (env.findAsyncConst? asyncDecl).all (·.exts?.isNone))
+      (ctx.mayContain asyncDecl && (env.findAsyncConst? asyncDecl).any (·.exts?.isNone))
     | _ => true
 
 /--
diff --git a/tests/lean/run/issue11799.lean b/tests/lean/run/issue11799.lean
deleted file mode 100644
index 362e507b5575..000000000000
--- a/tests/lean/run/issue11799.lean
+++ /dev/null
@@ -1,28 +0,0 @@
--- Reproducer for issue #11799
--- Panic in async elaboration for theorems with a docstring within `where`
-import Lean
-
--- Main reproducer: theorem with docstring on where-bound auxiliary
-theorem foo : True := aux where /-- doc -/ aux := True.intro
-
--- Variant: def with docstring (this always worked)
-def bar : True := aux where /-- doc -/ aux := True.intro
-
--- Variant: multiple where-bound auxiliaries with docstrings
-theorem baz : True ∧ True := ⟨aux1, aux2⟩ where
-  /-- first aux -/ aux1 := True.intro
-  /-- second aux -/ aux2 := True.intro
-
--- Verify the docstrings are actually attached
-open Lean in
-#eval show MetaM Unit from do
-  let env ← getEnv
-  let check (name : Name) (expected : String) : MetaM Unit := do
-    let some doc ← findDocString? env name
-      | throwError "no docstring found for {name}"
-    unless doc.trimAscii == expected do
-      throwError "docstring mismatch for {name}: expected {repr expected}, got {repr doc}"
-  check ``foo.aux "doc"
-  check ``bar.aux "doc"
-  check ``baz.aux1 "first aux"
-  check ``baz.aux2 "second aux"