diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index e83c3f4d1e..5e2d598a1a 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -467,7 +467,12 @@ open Language in
 instance : ToSnapshotTree MacroExpandedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, s.next.map (·.map (sync := true) toSnapshotTree)⟩
 
-partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
+partial def elabCommand (stx : Syntax) : CommandElabM Unit :=
+  try
+    go
+  finally
+    addTraceAsMessages
+where go := do
   withLogging <| withRef stx <| withIncRecDepth <| withFreshMacroScope do
     match stx with
     | Syntax.node _ k args =>
@@ -593,7 +598,6 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
       messages := initMsgs ++ msgs
       infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }
     }
-    addTraceAsMessages
 
 /-- Adapt a syntax transformation to a regular, command-producing elaborator. -/
 def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab := fun stx => do
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index fc022a777a..3058fa9241 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -135,12 +135,10 @@ private def cleanupOfNat (type : Expr) : MetaM Expr := do
 Elaborates only the declaration view headers. We have to elaborate the headers first because we
 support mutually recursive declarations in Lean 4.
 -/
-private def elabHeaders (views : Array DefView)
+private def elabHeaders (views : Array DefView) (expandedDeclIds : Array ExpandDeclIdResult)
     (bodyPromises : Array (IO.Promise (Option BodyProcessedSnapshot)))
     (tacPromises : Array (IO.Promise Tactic.TacticParsedSnapshot)) :
     TermElabM (Array DefViewElabHeader) := do
-  let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do
-    Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
   withAutoBoundImplicitForbiddenPred (fun n => expandedDeclIds.any (·.shortName == n)) do
     let mut headers := #[]
     -- Can we reuse the result for a body? For starters, all headers (even those below the body)
@@ -1019,6 +1017,9 @@ private def checkAllDeclNamesDistinct (preDefs : Array PreDefinition) : TermElab
       throwErrorAt preDef.ref errorMsg
     names := names.insert userName preDef.ref
 
+structure AsyncBodyInfo where
+deriving TypeName
+
 def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
@@ -1031,44 +1032,107 @@ where
   go := do
     let bodyPromises ← views.mapM fun _ => IO.Promise.new
     let tacPromises ← views.mapM fun _ => IO.Promise.new
-    let scopeLevelNames ← getLevelNames
-    let headers ← elabHeaders views bodyPromises tacPromises
+    let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do
+      Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
+    let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises
     let headers ← levelMVarToParamHeaders views headers
-    let allUserLevelNames := getAllUserLevelNames headers
-    withFunLocalDecls headers fun funFVars => do
-      for view in views, funFVar in funFVars do
-        addLocalVarInfo view.declId funFVar
-      let values ←
-        try
-          let values ← elabFunValues headers vars sc
-          Term.synthesizeSyntheticMVarsNoPostponing
-          values.mapM (instantiateMVarsProfiling ·)
-        catch ex =>
-          logException ex
-          headers.mapM fun header => withRef header.declId <| mkLabeledSorry header.type (synthetic := true) (unique := true)
-      let headers ← headers.mapM instantiateMVarsAtHeader
-      let letRecsToLift ← getLetRecsToLift
-      let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
-      checkLetRecsToLiftTypes funFVars letRecsToLift
-      (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc headers else withUsed vars headers values letRecsToLift) fun vars => do
-        let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
-        checkAllDeclNamesDistinct preDefs
-        for preDef in preDefs do
-          trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
-        let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamTypesPreDecls preDefs
-        let preDefs ← instantiateMVarsAtPreDecls preDefs
-        let preDefs ← shareCommonPreDefs preDefs
-        let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
-        for preDef in preDefs do
-          trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
-        addPreDefinitions preDefs
-        processDeriving headers
-    for view in views, header in headers do
+    -- elaborate body in parallel when all stars align
+    if let (#[view], #[declId]) := (views, expandedDeclIds) then
+      if Elab.async.get (← getOptions) && view.kind.isTheorem &&
+          !deprecated.oldSectionVars.get (← getOptions) &&
+          -- holes in theorem types is not a fatal error, but it does make parallelism impossible
+          !headers[0]!.type.hasMVar then
+        elabAsync headers[0]! view declId
+      else elabSync headers
+    else elabSync headers
+    for view in views, declId in expandedDeclIds do
       -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
       -- that depends only on a part of the ref
-      addDeclarationRangesForBuiltin header.declName view.modifiers.stx view.ref
+      addDeclarationRangesForBuiltin declId.declName view.modifiers.stx view.ref
+  elabSync headers := do
+    finishElab headers
+    processDeriving headers
+  elabAsync header view declId := do
+    let env ← getEnv
+    let async ← env.addConstAsync declId.declName .thm
+    setEnv async.mainEnv
 
+    -- TODO: parallelize header elaboration as well? Would have to refactor auto implicits catch,
+    -- makes `@[simp]` etc harder?
+    let type ← withHeaderSecVars vars sc #[header] fun vars => do
+      mkForallFVars vars header.type >>= instantiateMVars
+    let allUserLevelNames := getAllUserLevelNames #[header]
+    let type ← withLevelNames allUserLevelNames <| levelMVarToParam type
 
+    -- in the case of theorems, the decl level params are those of the header
+    let mut s : CollectLevelParams.State := {}
+    s := collectLevelParams s type
+    let scopeLevelNames ← getLevelNames
+    let levelParams ← IO.ofExcept <| sortDeclLevelParams scopeLevelNames allUserLevelNames s.params
+    async.commitSignature { name := header.declName, levelParams, type }
+
+    -- attributes should be applied on the main thread; see below
+    let header := { header with modifiers.attrs := #[] }
+
+    -- insert a hole for the proof info trees in the main info tree
+    let infoHole ← mkFreshMVarId
+    let infoPromise ← IO.Promise.new
+    modifyInfoState fun s => { s with
+      trees := s.trees.push <| .hole infoHole
+      lazyAssignment := s.lazyAssignment.insert infoHole <| infoPromise.resultD default
+    }
+
+    -- now start new thread for body elaboration, then nested thread for kernel checking
+    let cancelTk ← IO.CancelToken.new
+    let act ← wrapAsyncAsSnapshot (desc := s!"elaborating proof of {declId.declName}")
+        (cancelTk? := cancelTk) fun _ => do
+      setEnv async.asyncEnv
+      try
+        finishElab #[header]
+      finally
+        reportDiag
+        -- must introduce node to fill `infoHole` with multiple info trees
+        let info := .ofCustomInfo { stx := header.value, value := .mk (α := AsyncBodyInfo) {} }
+        infoPromise.resolve <| .node info (← getInfoTrees)
+      async.commitConst (← getEnv)
+      let cancelTk ← IO.CancelToken.new
+      let checkAct ← wrapAsyncAsSnapshot (desc := s!"finishing proof of {declId.declName}")
+          (cancelTk? := cancelTk) fun _ => do
+        processDeriving #[header]
+        async.commitCheckEnv (← getEnv)
+      let checkTask ← BaseIO.mapTask (t := (← getEnv).checked) checkAct
+      Core.logSnapshotTask { stx? := none, task := checkTask, cancelTk? := cancelTk }
+    Core.logSnapshotTask { stx? := none, task := (← BaseIO.asTask (act ())), cancelTk? := cancelTk }
+    applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
+    applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
+  finishElab headers := withFunLocalDecls headers fun funFVars => do
+    for view in views, funFVar in funFVars do
+      addLocalVarInfo view.declId funFVar
+    let values ← try
+      let values ← elabFunValues headers vars sc
+      Term.synthesizeSyntheticMVarsNoPostponing
+      values.mapM (instantiateMVarsProfiling ·)
+    catch ex =>
+      logException ex
+      headers.mapM fun header => withRef header.declId <| mkLabeledSorry header.type (synthetic := true) (unique := true)
+    let headers ← headers.mapM instantiateMVarsAtHeader
+    let letRecsToLift ← getLetRecsToLift
+    let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
+    checkLetRecsToLiftTypes funFVars letRecsToLift
+    (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc headers else withUsed vars headers values letRecsToLift) fun vars => do
+      let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+      checkAllDeclNamesDistinct preDefs
+      for preDef in preDefs do
+        trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
+      let allUserLevelNames := getAllUserLevelNames headers
+      let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamTypesPreDecls preDefs
+      let preDefs ← instantiateMVarsAtPreDecls preDefs
+      let preDefs ← shareCommonPreDefs preDefs
+      let scopeLevelNames ← getLevelNames
+      let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
+      for preDef in preDefs do
+        trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
+      addPreDefinitions preDefs
   processDeriving (headers : Array DefViewElabHeader) := do
     for header in headers, view in views do
       if let some classNamesStx := view.deriving? then
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 94c6ee45ce..c245c1740c 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -139,14 +139,25 @@ private def betaReduceLetRecApps (preDefs : Array PreDefinition) : MetaM (Array
     else
       return preDef
 
-private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
+private def addSorried (preDefs : Array PreDefinition) : TermElabM Unit := do
   for preDef in preDefs do
-    let decl := Declaration.axiomDecl {
-      name        := preDef.declName,
-      levelParams := preDef.levelParams,
-      type        := preDef.type,
-      isUnsafe    := preDef.modifiers.isUnsafe
-    }
+    let value ← mkSorry (synthetic := true) preDef.type
+    let decl := if preDef.kind.isTheorem then
+      Declaration.thmDecl {
+        name        := preDef.declName,
+        levelParams := preDef.levelParams,
+        type        := preDef.type,
+        value
+      }
+    else
+      Declaration.defnDecl {
+        name        := preDef.declName,
+        levelParams := preDef.levelParams,
+        type        := preDef.type,
+        hints       := .abbrev
+        safety      := .safe
+        value
+      }
     addDecl decl
     withSaveInfoContext do  -- save new env
       addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
@@ -306,9 +317,9 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
                   catch _ =>
                     -- Compilation failed try again just as axiom
                     s.restore
-                    addAsAxioms preDefs
+                    addSorried preDefs
               else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
-                addAsAxioms preDefs
+                addSorried preDefs
             catch _ => s.restore
 
 builtin_initialize
diff --git a/src/Lean/Elab/Tactic/AsAuxLemma.lean b/src/Lean/Elab/Tactic/AsAuxLemma.lean
index 4c15b42035..3a4370e1b3 100644
--- a/src/Lean/Elab/Tactic/AsAuxLemma.lean
+++ b/src/Lean/Elab/Tactic/AsAuxLemma.lean
@@ -14,15 +14,14 @@ open Lean Meta Elab Tactic Parser.Tactic
 
 @[builtin_tactic as_aux_lemma]
 def elabAsAuxLemma : Lean.Elab.Tactic.Tactic
-| `(tactic| as_aux_lemma => $s) =>
-  liftMetaTactic fun mvarId => do
-    let (mvars, _) ← runTactic mvarId s
-    unless mvars.isEmpty do
-      throwError "Cannot abstract term into auxiliary lemma because there are open goals."
-    let e ← instantiateMVars (mkMVar mvarId)
-    let env ← getEnv
-    -- TODO: this likely should share name creation code with `mkAuxLemma`
-    let e ← mkAuxTheorem (← mkFreshUserName <| env.asyncPrefix?.getD env.mainModule ++ `_auxLemma) (← mvarId.getType) e
-    mvarId.assign e
-    return []
+| `(tactic| as_aux_lemma => $s) => withMainContext do
+  let mvarId ← getMainGoal
+  let mvars ← Tactic.run mvarId (evalTactic s)
+  unless mvars.isEmpty do
+    throwError "Cannot abstract term into auxiliary lemma because there are open goals."
+  let e ← instantiateMVars (mkMVar mvarId)
+  let env ← getEnv
+  -- TODO: this likely should share name creation code with `mkAuxLemma`
+  let e ← mkAuxTheorem (← mkFreshUserName <| env.asyncPrefix?.getD env.mainModule ++ `_auxLemma) (← mvarId.getType) e
+  mvarId.assign e
 | _ => throwError "Invalid as_aux_lemma syntax"
diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean
index cfeebf2feb..4298ad4b6a 100644
--- a/src/Lean/Meta/CongrTheorems.lean
+++ b/src/Lean/Meta/CongrTheorems.lean
@@ -414,7 +414,7 @@ def mkHCongrWithArityForConst? (declName : Name) (levels : List Level) (numArgs
     let suffix := hcongrThmSuffixBasePrefix ++ toString numArgs
     let thmName := Name.str declName suffix
     unless (← getEnv).contains thmName do
-      executeReservedNameAction thmName
+      let _ ← executeReservedNameAction thmName
     let proof := mkConst thmName levels
     let type ← inferType proof
     let some argKinds := congrKindsExt.find? (← getEnv) thmName
@@ -431,7 +431,7 @@ def mkCongrSimpForConst? (declName : Name) (levels : List Level) : MetaM (Option
   try
     let thmName := Name.str declName congrSimpSuffix
     unless (← getEnv).contains thmName do
-      executeReservedNameAction thmName
+      let _ ← executeReservedNameAction thmName
     let proof := mkConst thmName levels
     let type ← inferType proof
     let some argKinds := congrKindsExt.find? (← getEnv) thmName
diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index 3784f0abfa..e7cc5c4b08 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -86,9 +86,7 @@ builtin_initialize registerReservedNamePredicate fun env n =>
   | .str p s =>
     (isEqnReservedNameSuffix s || s == unfoldThmSuffix || s == eqUnfoldThmSuffix)
     && env.isSafeDefinition p
-    -- Remark: `f.match_<idx>.eq_<idx>` are private definitions and are not treated as reserved names
-    -- Reason: `f.match_<idx>.splitter is generated at the same time, and can eliminate into type.
-    -- Thus, it cannot be defined in different modules since it is not a theorem, and is used to generate code.
+    -- Remark: `f.match_<idx>.eq_<idx>` are handled separately in `Lean.Meta.Match.MatchEqs`.
     && !isMatcherCore env p
   | _ => false
 
@@ -289,7 +287,7 @@ def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) :
 builtin_initialize
   registerReservedNameAction fun name => do
     let .str p s := name | return false
-    unless (← getEnv).isSafeDefinition p do return false
+    unless (← getEnv).isSafeDefinition p && !isMatcherCore (← getEnv) p do return false
     if isEqnReservedNameSuffix s then
       return (← MetaM.run' <| getEqnsFor? p).isSome
     if s == unfoldThmSuffix then
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index ffdbfa055b..0aad1a62c6 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -769,4 +769,19 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
 
 builtin_initialize registerTraceClass `Meta.Match.matchEqs
 
+private def isMatchEqName? (env : Environment) (n : Name) : Option Name := do
+  let .str p s := n | failure
+  guard <| isEqnReservedNameSuffix s || s == "splitter"
+  let p ← privateToUserName? p
+  guard <| isMatcherCore env p
+  return p
+
+builtin_initialize registerReservedNamePredicate (isMatchEqName? · · |>.isSome)
+
+builtin_initialize registerReservedNameAction fun name => do
+  let some p := isMatchEqName? (← getEnv) name |
+    return false
+  let _ ← MetaM.run' <| getEquationsFor p
+  return true
+
 end Lean.Meta.Match
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index 1f4072644d..aef9006b6c 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -78,8 +78,8 @@ def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
     | ConstantInfo.recInfo val => k val us
     | _                        => failK ()
 
-def hasConst [Monad m] [MonadEnv m] (constName : Name) : m Bool := do
-  return (← getEnv).contains constName
+def hasConst [Monad m] [MonadEnv m] (constName : Name) (skipRealize := true) : m Bool := do
+  return (← getEnv).contains (skipRealize := skipRealize) constName
 
 private partial def mkAuxNameAux (env : Environment) (base : Name) (i : Nat) : Name :=
   let candidate := base.appendIndexAfter i
diff --git a/src/Lean/ReservedNameAction.lean b/src/Lean/ReservedNameAction.lean
index 030891de04..a11e5afbd6 100644
--- a/src/Lean/ReservedNameAction.lean
+++ b/src/Lean/ReservedNameAction.lean
@@ -31,9 +31,7 @@ Execute a registered reserved action for the given reserved name.
 Note that the handler can throw an exception.
 -/
 def executeReservedNameAction (name : Name) : CoreM Unit := do
-  for act in (← reservedNameActionsRef.get) do
-    if (← act name) then
-      return ()
+  let _ ← (← reservedNameActionsRef.get).anyM (· name)
 
 /--
 Similar to `resolveGlobalName`, but also executes reserved name actions.
@@ -46,7 +44,9 @@ def realizeGlobalName (id : Name) : CoreM (List (Name × List String)) := do
     else
       try
         executeReservedNameAction c
-        return (← getEnv).contains c
+        -- note that even if an action "handled" a name, it may still be undefined, e.g. with an
+        -- out-of-bounds equation index
+        return (← getEnv).containsOnBranch c
       catch ex =>
         -- We record the error produced by the reserved name action generator
         logError m!"Failed to realize constant {id}:{indentD ex.toMessageData}"
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 8486dcbe9d..9992f4b3f2 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -393,7 +393,7 @@ def setupImports (meta : DocumentMeta) (cmdlineOpts : Options) (chanOut : Std.Ch
   let opts := cmdlineOpts.mergeBy (fun _ _ fileOpt => fileOpt) fileSetupResult.fileOptions
 
   -- default to async elaboration; see also `Elab.async` docs
-  let opts := Elab.async.setIfNotSet opts true
+  --let opts := Elab.async.setIfNotSet opts true
 
   return .ok {
     mainModuleName
diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean
index 00fe3b994c..0ab8c071b0 100644
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@@ -343,7 +343,7 @@ We use an environment extension to cache resolution orders.
 These are not expensive to compute, but worth caching, and we save olean storage space.
 -/
 builtin_initialize structureResolutionExt : EnvExtension StructureResolutionState ←
-  registerEnvExtension (pure {})
+  registerEnvExtension (pure {}) (asyncMode := .local)  -- mere cache
 
 /-- Gets the resolution order if it has already been cached. -/
 private def getStructureResolutionOrder? (env : Environment) (structName : Name) : Option (Array Name) :=
diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h
index ee225c1734..923e75e26b 100644
--- a/src/stdlib_flags.h
+++ b/src/stdlib_flags.h
@@ -22,6 +22,9 @@ options get_default_options() {
     opts = opts.update({"quotPrecheck"}, true);
 
     opts = opts.update({"pp", "rawOnError"}, true);
+
+    // temporarily restrict async to language server used in core, i.e. stage 0
+    opts = opts.update({"Elab", "async"}, true);
 #endif
     return opts;
 }
diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean
index 11e7f393ea..9143a721a4 100644
--- a/tests/lean/run/ack.lean
+++ b/tests/lean/run/ack.lean
@@ -5,6 +5,15 @@ def ack : Nat → Nat → Nat
 termination_by a b => (a, b)
 
 /--
+info: [diag] Diagnostics
+  [kernel] unfolded declarations (max: 1193, num: 5):
+    [kernel] Nat.casesOn ↦ 1193
+    [kernel] Nat.rec ↦ 1065
+    [kernel] Eq.ndrec ↦ 973
+    [kernel] Eq.rec ↦ 973
+    [kernel] Acc.rec ↦ 754
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+---
 info: [diag] Diagnostics
   [reduction] unfolded declarations (max: 2567, num: 5):
     [reduction] Nat.rec ↦ 2567
diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean
index 1d60fef423..82f54483d4 100644
--- a/tests/lean/run/allGoals.lean
+++ b/tests/lean/run/allGoals.lean
@@ -301,46 +301,46 @@ theorem idEq (a : α) : id a = a :=
 
 /--
 info: case sunday
-⊢ Weekday.sunday.previous.next = id Weekday.sunday
+⊢ sunday.previous.next = id sunday
 
 case monday
-⊢ Weekday.monday.previous.next = id Weekday.monday
+⊢ monday.previous.next = id monday
 
 case tuesday
-⊢ Weekday.tuesday.previous.next = id Weekday.tuesday
+⊢ tuesday.previous.next = id tuesday
 
 case wednesday
-⊢ Weekday.wednesday.previous.next = id Weekday.wednesday
+⊢ wednesday.previous.next = id wednesday
 
 case thursday
-⊢ Weekday.thursday.previous.next = id Weekday.thursday
+⊢ thursday.previous.next = id thursday
 
 case friday
-⊢ Weekday.friday.previous.next = id Weekday.friday
+⊢ friday.previous.next = id friday
 
 case saturday
-⊢ Weekday.saturday.previous.next = id Weekday.saturday
+⊢ saturday.previous.next = id saturday
 ---
 info: case sunday
-⊢ Weekday.sunday.previous.next = Weekday.sunday
+⊢ sunday.previous.next = sunday
 
 case monday
-⊢ Weekday.monday.previous.next = Weekday.monday
+⊢ monday.previous.next = monday
 
 case tuesday
-⊢ Weekday.tuesday.previous.next = Weekday.tuesday
+⊢ tuesday.previous.next = tuesday
 
 case wednesday
-⊢ Weekday.wednesday.previous.next = Weekday.wednesday
+⊢ wednesday.previous.next = wednesday
 
 case thursday
-⊢ Weekday.thursday.previous.next = Weekday.thursday
+⊢ thursday.previous.next = thursday
 
 case friday
-⊢ Weekday.friday.previous.next = Weekday.friday
+⊢ friday.previous.next = friday
 
 case saturday
-⊢ Weekday.saturday.previous.next = Weekday.saturday
+⊢ saturday.previous.next = saturday
 -/
 #guard_msgs in
 theorem Weekday.test (d : Weekday) : next (previous d) = id d := by
@@ -352,25 +352,25 @@ theorem Weekday.test (d : Weekday) : next (previous d) = id d := by
 
 /--
 info: case sunday
-⊢ Weekday.sunday.previous.next = Weekday.sunday
+⊢ sunday.previous.next = sunday
 
 case monday
-⊢ Weekday.monday.previous.next = Weekday.monday
+⊢ monday.previous.next = monday
 
 case tuesday
-⊢ Weekday.tuesday.previous.next = Weekday.tuesday
+⊢ tuesday.previous.next = tuesday
 
 case wednesday
-⊢ Weekday.wednesday.previous.next = Weekday.wednesday
+⊢ wednesday.previous.next = wednesday
 
 case thursday
-⊢ Weekday.thursday.previous.next = Weekday.thursday
+⊢ thursday.previous.next = thursday
 
 case friday
-⊢ Weekday.friday.previous.next = Weekday.friday
+⊢ friday.previous.next = friday
 
 case saturday
-⊢ Weekday.saturday.previous.next = Weekday.saturday
+⊢ saturday.previous.next = saturday
 -/
 #guard_msgs in
 theorem Weekday.test2 (d : Weekday) : next (previous d) = id d := by
diff --git a/tests/lean/run/decideTacticKernel.lean b/tests/lean/run/decideTacticKernel.lean
index 4daf8df3f1..ad3756ad30 100644
--- a/tests/lean/run/decideTacticKernel.lean
+++ b/tests/lean/run/decideTacticKernel.lean
@@ -58,15 +58,14 @@ theorem thm1 : ∀ x < 100, x * x ≤ 10000 := by decide +kernel
 
 theorem thm1' : ∀ x < 100, x * x ≤ 10000 := by decide +kernel
 
--- (Note: when run within VS Code, these tests fail since the auxLemmas have a `lean.run` prefix.)
 /--
 info: theorem thm1 : ∀ (x : Nat), x < 100 → x * x ≤ 10000 :=
-decideTacticKernel._auxLemma.3
+thm1._auxLemma.1
 -/
 #guard_msgs in #print thm1
 /--
 info: theorem thm1' : ∀ (x : Nat), x < 100 → x * x ≤ 10000 :=
-decideTacticKernel._auxLemma.3
+thm1'._auxLemma.1
 -/
 #guard_msgs in #print thm1'
 
diff --git a/tests/lean/run/eqnsReducible.lean b/tests/lean/run/eqnsReducible.lean
index 802683a893..273ce38013 100644
--- a/tests/lean/run/eqnsReducible.lean
+++ b/tests/lean/run/eqnsReducible.lean
@@ -77,7 +77,7 @@ theorem ex2 : P (semired o) := by simp [semired]; fail
 
 /-- info: true -/
 #guard_msgs in
-run_meta Lean.logInfo m!"{← Lean.hasConst `semired.eq_1}"
+run_meta Lean.logInfo m!"{← Lean.hasConst (skipRealize := false) `semired.eq_1}"
 
 def semired2 : Option α → Bool
   | .some _ => true
diff --git a/tests/lean/run/grind_attrs.lean b/tests/lean/run/grind_attrs.lean
index 67938973f0..5eb965cc8b 100644
--- a/tests/lean/run/grind_attrs.lean
+++ b/tests/lean/run/grind_attrs.lean
@@ -27,25 +27,19 @@ opaque Expr.eval : Expr → State → Nat
 axiom Expr.constProp : Expr → State → Expr
 
 
-/--
-info: [grind.ematch.pattern] Expr.eval_constProp_of_sub: [State.le #3 #2, Expr.constProp #1 #3]
--/
+/-- info: [grind.ematch.pattern] eval_constProp_of_sub: [State.le #3 #2, constProp #1 #3] -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.pattern true in
 @[grind =>] theorem Expr.eval_constProp_of_sub (e : Expr) (h : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ :=
   sorry
 
-/--
-info: [grind.ematch.pattern] Expr.eval_constProp_of_eq_of_sub: [State.le #3 #2, Expr.constProp #1 #3]
--/
+/-- info: [grind.ematch.pattern] eval_constProp_of_eq_of_sub: [State.le #3 #2, constProp #1 #3] -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.pattern true in
 @[grind =>] theorem Expr.eval_constProp_of_eq_of_sub {e : Expr} (h₂ : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ :=
   sorry
 
-/--
-info: [grind.ematch.pattern] State.update_le_update: [State.le #4 #3, State.update #4 #2 #1]
--/
+/-- info: [grind.ematch.pattern] update_le_update: [le #4 #3, update #4 #2 #1] -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.pattern true in
 @[grind =>] theorem State.update_le_update (h : State.le σ' σ) : State.le (σ'.update x v) (σ.update x v) :=
diff --git a/tests/lean/run/info_trees.lean b/tests/lean/run/info_trees.lean
index 2ef75ea014..beee048cf9 100644
--- a/tests/lean/run/info_trees.lean
+++ b/tests/lean/run/info_trees.lean
@@ -3,78 +3,79 @@
 -- it is fine to simply remove the `#guard_msgs` and expected output.
 
 /--
-info: Try this: exact Nat.zero_le n
----
-info: • command @ ⟨81, 0⟩-⟨81, 40⟩ @ Lean.Elab.Command.elabDeclaration
-  • Nat : Type @ ⟨81, 15⟩-⟨81, 18⟩ @ Lean.Elab.Term.elabIdent
-    • [.] Nat : some Sort.{?_uniq.1} @ ⟨81, 15⟩-⟨81, 18⟩
-    • Nat : Type @ ⟨81, 15⟩-⟨81, 18⟩
-  • n (isBinder := true) : Nat @ ⟨81, 11⟩-⟨81, 12⟩
-  • 0 ≤ n : Prop @ ⟨81, 22⟩-⟨81, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
+info: • command @ ⟨82, 0⟩-⟨82, 40⟩ @ Lean.Elab.Command.elabDeclaration
+  • Nat : Type @ ⟨82, 15⟩-⟨82, 18⟩ @ Lean.Elab.Term.elabIdent
+    • [.] Nat : some Sort.{?_uniq.1} @ ⟨82, 15⟩-⟨82, 18⟩
+    • Nat : Type @ ⟨82, 15⟩-⟨82, 18⟩
+  • n (isBinder := true) : Nat @ ⟨82, 11⟩-⟨82, 12⟩
+  • 0 ≤ n : Prop @ ⟨82, 22⟩-⟨82, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
     • Macro expansion
       0 ≤ n
       ===>
       binrel% LE.le✝ 0 n
-      • 0 ≤ n : Prop @ ⟨81, 22⟩†-⟨81, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
-        • 0 ≤ n : Prop @ ⟨81, 22⟩†-⟨81, 27⟩†
-          • [.] LE.le✝ : none @ ⟨81, 22⟩†-⟨81, 27⟩†
-          • 0 : Nat @ ⟨81, 22⟩-⟨81, 23⟩ @ Lean.Elab.Term.elabNumLit
-          • n : Nat @ ⟨81, 26⟩-⟨81, 27⟩ @ Lean.Elab.Term.elabIdent
-            • [.] n : none @ ⟨81, 26⟩-⟨81, 27⟩
-            • n : Nat @ ⟨81, 26⟩-⟨81, 27⟩
-  • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨81, 8⟩-⟨81, 9⟩
-  • n (isBinder := true) : Nat @ ⟨81, 11⟩-⟨81, 12⟩
-  • CustomInfo(Lean.Elab.Term.BodyInfo)
-    • Tactic @ ⟨81, 31⟩-⟨81, 40⟩
-      (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])))
-      before ⏎
-      n : Nat
-      ⊢ 0 ≤ n
-      after no goals
-      • Tactic @ ⟨81, 31⟩-⟨81, 33⟩
-        "by"
+      • 0 ≤ n : Prop @ ⟨82, 22⟩†-⟨82, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
+        • 0 ≤ n : Prop @ ⟨82, 22⟩†-⟨82, 27⟩†
+          • [.] LE.le✝ : none @ ⟨82, 22⟩†-⟨82, 27⟩†
+          • 0 : Nat @ ⟨82, 22⟩-⟨82, 23⟩ @ Lean.Elab.Term.elabNumLit
+          • n : Nat @ ⟨82, 26⟩-⟨82, 27⟩ @ Lean.Elab.Term.elabIdent
+            • [.] n : none @ ⟨82, 26⟩-⟨82, 27⟩
+            • n : Nat @ ⟨82, 26⟩-⟨82, 27⟩
+  • CustomInfo(Lean.Elab.Term.AsyncBodyInfo)
+    • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨82, 8⟩-⟨82, 9⟩
+    • n (isBinder := true) : Nat @ ⟨82, 11⟩-⟨82, 12⟩
+    • CustomInfo(Lean.Elab.Term.BodyInfo)
+      • Tactic @ ⟨82, 31⟩-⟨82, 40⟩
+        (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])))
         before ⏎
         n : Nat
         ⊢ 0 ≤ n
         after no goals
-        • Tactic @ ⟨81, 34⟩-⟨81, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
-          (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]))
+        • Tactic @ ⟨82, 31⟩-⟨82, 33⟩
+          "by"
           before ⏎
           n : Nat
           ⊢ 0 ≤ n
           after no goals
-          • Tactic @ ⟨81, 34⟩-⟨81, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
-            (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])
+          • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
+            (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]))
             before ⏎
             n : Nat
             ⊢ 0 ≤ n
             after no goals
-            • Tactic @ ⟨81, 34⟩-⟨81, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
-              (Tactic.exact? "exact?" [])
+            • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
+              (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])
               before ⏎
               n : Nat
               ⊢ 0 ≤ n
               after no goals
-              • Tactic @ ⟨81, 34⟩†-⟨81, 40⟩† @ Lean.Elab.Tactic.evalExact
-                (Tactic.exact "exact" (Term.app `Nat.zero_le [`n]))
+              • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
+                (Tactic.exact? "exact?" [])
                 before ⏎
                 n : Nat
                 ⊢ 0 ≤ n
                 after no goals
-                • Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp
-                  • [.] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.36 @ ⟨1, 0⟩†-⟨1, 0⟩†
-                  • Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩†
-                  • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent
-                    • [.] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†
-                    • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩†
-              • CustomInfo(Lean.Meta.Tactic.TryThis.TryThisInfo)
-              • UserWidget Lean.Meta.Tactic.TryThis.tryThisWidget
-                {"suggestions": [{"suggestion": "exact Nat.zero_le n"}],
-                 "style": null,
-                 "range":
-                 {"start": {"line": 80, "character": 34}, "end": {"line": 80, "character": 40}},
-                 "isInline": true,
-                 "header": "Try this: "} • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨81, 8⟩-⟨81, 9⟩
+                • Tactic @ ⟨82, 34⟩†-⟨82, 40⟩† @ Lean.Elab.Tactic.evalExact
+                  (Tactic.exact "exact" (Term.app `Nat.zero_le [`n]))
+                  before ⏎
+                  n : Nat
+                  ⊢ 0 ≤ n
+                  after no goals
+                  • Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp
+                    • [.] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.37 @ ⟨1, 0⟩†-⟨1, 0⟩†
+                    • Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩†
+                    • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent
+                      • [.] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†
+                      • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩†
+                • CustomInfo(Lean.Meta.Tactic.TryThis.TryThisInfo)
+                • UserWidget Lean.Meta.Tactic.TryThis.tryThisWidget
+                  {"suggestions": [{"suggestion": "exact Nat.zero_le n"}],
+                   "style": null,
+                   "range":
+                   {"start": {"line": 81, "character": 34}, "end": {"line": 81, "character": 40}},
+                   "isInline": true,
+                   "header": "Try this: "} • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨82, 8⟩-⟨82, 9⟩
+---
+info: Try this: exact Nat.zero_le n
 -/
 #guard_msgs in
 #info_trees in
diff --git a/tests/lean/run/variable.lean b/tests/lean/run/variable.lean
index c5d12180b2..300d8af97e 100644
--- a/tests/lean/run/variable.lean
+++ b/tests/lean/run/variable.lean
@@ -122,21 +122,13 @@ variable (a : α) in
 omit α in
 theorem t11 (a : α) : True := trivial
 
-/--
-error: cannot omit referenced section variable 'α'
----
-error: cannot omit referenced section variable 'α'
--/
+/-- error: cannot omit referenced section variable 'α' -/
 #guard_msgs in
 variable (α : Type) in
 omit α in
 theorem t12 (a : α) : True := trivial
 
-/--
-error: cannot omit referenced section variable 'inst✝'
----
-error: cannot omit referenced section variable 'inst✝'
--/
+/-- error: cannot omit referenced section variable 'inst✝' -/
 #guard_msgs in
 variable [ToString α] in
 omit [ToString α] in
@@ -165,10 +157,10 @@ omit [ToString Nat]
 variable (α : Type) in
 include α in
 omit α in
-theorem t13 : True := trivial
+theorem t14 : True := trivial
 
 /--
-warning: automatically included section variable(s) unused in theorem 't14':
+warning: automatically included section variable(s) unused in theorem 't15':
   α
 consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
   omit α in theorem ...
@@ -179,7 +171,7 @@ variable (α : Type) in
 include α in
 omit α in
 include α in
-theorem t14 : True := trivial
+theorem t15 : True := trivial
 
 /-! But you probably shouldn't use it -/
 
@@ -192,4 +184,4 @@ note: this linter can be disabled with `set_option linter.omit false`
 variable (α : Type) in
 include α in
 omit α in
-theorem t15 : True := trivial
+theorem t16 : True := trivial
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index db3cdf24fc..c5fa1de371 100644
--- a/tests/lean/shadow.lean.expected.out
+++ b/tests/lean/shadow.lean.expected.out
@@ -19,7 +19,7 @@ inst✝ inst : α
 shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
-inst.78 : Inhabited α
+inst.74 : Inhabited α
 inst inst : α
 ⊢ {β δ : Type} → α → β → δ → α × β × δ
 shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder
diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out
index d5bc121d47..98fd14c4eb 100644
--- a/tests/lean/syntaxPrec.lean.expected.out
+++ b/tests/lean/syntaxPrec.lean.expected.out
@@ -1,10 +1,10 @@
 syntaxPrec.lean:1:17-1:21: error: unexpected token '<|>'; expected ':'
+[Elab.command] @[term_parser 1000]
+    def «termFoo*_» : Lean.ParserDescr✝ :=
+      ParserDescr.node✝ `«termFoo*_» 1022
+        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo")
+          (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*"))
+            ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) ","
+              (ParserDescr.symbol✝ ", ") Bool.false✝)))
 [Elab.command] syntax "foo" ("*" <|> term,+) : term
-  [Elab.command] @[term_parser 1000]
-      def «termFoo*_» : Lean.ParserDescr✝ :=
-        ParserDescr.node✝ `«termFoo*_» 1022
-          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo")
-            (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*"))
-              ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) ","
-                (ParserDescr.symbol✝ ", ") Bool.false✝)))
 [Elab.command]