fix: avoid panic in async elaboration for theorems with docstrings in where (#11896)

This PR fixes a panic that occurred when a theorem had a docstring on an
auxiliary definition within a `where` clause.

Reproducer:
```lean
theorem foo : True := aux where /-- -/ aux := True.intro
```

The issue was that `asyncMayModify` used `.any` to check if a nested
declaration could have its extension state modified, which returned
`false` when the declaration wasn't yet in `asyncConsts`. Using `.all`
instead returns `true` for `none` (vacuously true), allowing
modification
of extension state for nested declarations that haven't been added to
`asyncConsts` yet.

Closes #11799

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

src/Lean/Environment.lean

@@ -1357,9 +1357,11 @@ 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.
+    -- 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).
     | .async .asyncEnv => ctx.declPrefix == asyncDecl ||
-      (ctx.mayContain asyncDecl && (env.findAsyncConst? asyncDecl).any (·.exts?.isNone))
+      (ctx.mayContain asyncDecl && (env.findAsyncConst? asyncDecl).all (·.exts?.isNone))
     | _ => true
 
 /--

tests/lean/run/issue11799.lean

@@ -0,0 +1,28 @@
+-- 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"