diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index 3e41e9e50c16..d1c885129ae7 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -41,7 +41,7 @@ def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
 def mkAttrKindGlobal : Syntax :=
   mkNode ``Lean.Parser.Term.attrKind #[mkNullNode]
 
-def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadInfoTree m] (attrInstance : Syntax) : m Attribute := do
+def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadInfoTree m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
   /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
   let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
   let attr := attrInstance[1]
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 81b367251792..1aeb01385968 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -128,12 +128,19 @@ private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core.
     initHeartbeats := heartbeats
     currMacroScope := ctx.currMacroScope }
 
-private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog :=
-  traceState.traces.foldl (init := log) fun (log : MessageLog) traceElem =>
+private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do
+  if traceState.traces.isEmpty then return log
+  let mut traces : Std.HashMap (String.Pos × String.Pos) (Array MessageData) := ∅
+  for traceElem in traceState.traces do
     let ref := replaceRef traceElem.ref ctx.ref
     let pos := ref.getPos?.getD 0
     let endPos := ref.getTailPos?.getD pos
-    log.add (mkMessageCore ctx.fileName ctx.fileMap traceElem.msg MessageSeverity.information pos endPos)
+    traces := traces.insert (pos, endPos) <| traces.findD (pos, endPos) #[] |>.push traceElem.msg
+  let mut log := log
+  let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
+  for ((pos, endPos), traceMsg) in traces' do
+    log := log.add <| mkMessageCore ctx.fileName ctx.fileMap (.joinSep traceMsg.toList "\n") .information pos endPos
+  return log
 
 private def addTraceAsMessages : CommandElabM Unit := do
   let ctx ← read
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 3e2120893da5..1c2042c9fb81 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1329,11 +1329,10 @@ where
 private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : Bool) (implicitLambda : Bool) : Syntax → TermElabM Expr
   | .missing => mkSyntheticSorryFor expectedType?
   | stx => withFreshMacroScope <| withIncRecDepth do
-    trace[Elab.step] "expected type: {expectedType?}, term\n{stx}"
+    withTraceNode `Elab.step (fun _ => return m!"expected type: {expectedType?}, term\n{stx}") do
     checkMaxHeartbeats "elaborator"
-    withNestedTraces do
     let env ← getEnv
-    match (← liftMacroM (expandMacroImpl? env stx)) with
+    let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (decl, stxNew?) =>
       let stxNew ← liftMacroM <| liftExcept stxNew?
       withInfoContext' stx (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <|
@@ -1345,6 +1344,8 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
       match implicit? with
       | some expectedType => elabImplicitLambda stx catchExPostpone expectedType
       | none              => elabUsingElabFns stx expectedType? catchExPostpone
+    trace[Elab.step.result] result
+    pure result
 
 /-- Store in the `InfoTree` that `e` is a "dot"-completion target. -/
 def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr) (field? : Option Syntax := none) : TermElabM Unit := do
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 20574beda3bd..c78e9d2cc62b 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -158,7 +158,7 @@ instance (m n) [MonadLift m n] [MonadMacroAdapter m] : MonadMacroAdapter n := {
   setNextMacroScope := fun s => liftM (MonadMacroAdapter.setNextMacroScope s : m _)
 }
 
-def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (x : MacroM α) : m α := do
+def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : MacroM α) : m α := do
   let env  ← getEnv
   let currNamespace ← getCurrNamespace
   let openDecls ← getOpenDecls
@@ -192,7 +192,7 @@ def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEn
     s.traceMsgs.reverse.forM fun (clsName, msg) => trace clsName fun _ => msg
     return a
 
-@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m]  [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (x : Macro) (stx : Syntax) : m Syntax :=
+@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m]  [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : Macro) (stx : Syntax) : m Syntax :=
   liftMacroM (x stx)
 
 partial def mkUnusedBaseName (baseName : Name) : MacroM Name := do
@@ -220,13 +220,6 @@ def withLogging [Monad m] [MonadLog m] [MonadExcept Exception m] [AddMessageCont
     (x : m Unit) : m Unit := do
   try x catch ex => logException ex
 
-@[inline] def trace [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (cls : Name) (msg : Unit → MessageData) : m Unit := do
-  if checkTraceOption (← getOptions) cls then
-    logTrace cls (msg ())
-
-def logDbgTrace [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (msg : MessageData) : m Unit := do
-  trace `Elab.debug fun _ => msg
-
 def nestedExceptionToMessageData [Monad m] [MonadLog m] (ex : Exception) : m MessageData := do
   let pos ← getRefPos
   match ex.getRef.getPos? with
@@ -244,5 +237,6 @@ def throwErrorWithNestedErrors [MonadError m] [Monad m] [MonadLog m] (msg : Mess
 builtin_initialize
   registerTraceClass `Elab
   registerTraceClass `Elab.step
+  registerTraceClass `Elab.step.result (inherited := true)
 
 end Lean.Elab
diff --git a/src/Lean/Log.lean b/src/Lean/Log.lean
index 0c8c3bf1d059..55793e7c535b 100644
--- a/src/Lean/Log.lean
+++ b/src/Lean/Log.lean
@@ -95,10 +95,6 @@ def logWarning [MonadOptions m] (msgData : MessageData) : m Unit := do
 def logInfo (msgData : MessageData) : m Unit :=
   log msgData MessageSeverity.information
 
-/-- Log a trace message into the message log. -/
-def logTrace (cls : Name) (msgData : MessageData) : m Unit := do
-  logInfo (MessageData.tagged cls m!"[{cls}] {msgData}")
-
 /-- Log the error message "unknown declaration" -/
 def logUnknownDecl (declName : Name) : m Unit :=
   logError m!"unknown declaration '{declName}'"
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 4ecba7983741..94e53a4c9ab4 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -54,7 +54,8 @@ inductive MessageData where
   /- Tagged sections. `Name` should be viewed as a "kind", and is used by `MessageData` inspector functions.
      Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
   | tagged            : Name → MessageData → MessageData
-  | node              : Array MessageData → MessageData
+  | trace (cls : Name) (msg : MessageData) (children : Array MessageData)
+    (collapsed : Bool := false)
   deriving Inhabited
 
 namespace MessageData
@@ -67,7 +68,6 @@ partial def isEmpty : MessageData → Bool
   | group m => m.isEmpty
   | compose m₁ m₂ => m₁.isEmpty && m₂.isEmpty
   | tagged _ m => m.isEmpty
-  | node ms => ms.all (·.isEmpty)
   | _ => false
 
 /- Instantiate metavariables occurring in nexted `ofExpr` constructors.
@@ -85,7 +85,7 @@ where
     | group msg                 => group <| visit msg mctx
     | compose msg₁ msg₂         => compose (visit msg₁ mctx) <| visit msg₂ mctx
     | tagged n msg              => tagged n <| visit msg mctx
-    | node msgs                 => node <| msgs.map (visit · mctx)
+    | trace cls msg msgs c      => trace cls (visit msg mctx) (msgs.map (visit · mctx)) c
     | _                         => msg
 
 variable (p : Name → Bool) in
@@ -96,7 +96,7 @@ partial def hasTag : MessageData → Bool
   | group msg               => hasTag msg
   | compose msg₁ msg₂       => hasTag msg₁ || hasTag msg₂
   | tagged n msg            => p n || hasTag msg
-  | node msgs               => msgs.any hasTag
+  | trace cls msg msgs _    => p cls || hasTag msg || msgs.any hasTag
   | _                       => false
 
 def nil : MessageData :=
@@ -127,18 +127,14 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
   | nCtx, some ctx,  ofGoal mvarId            => ppGoal (mkPPContext nCtx ctx) mvarId
   | nCtx, _,         withContext ctx d        => formatAux nCtx ctx d
   | _,    ctx,       withNamingContext nCtx d => formatAux nCtx ctx d
-  | nCtx, ctx,       tagged t d               =>
-    /- Messages starting a trace context have their tags postfixed with `_traceCtx` so that
-    we can detect them later. Here, we do so in order to print the trace context class. -/
-    if let .str cls "_traceCtx" := t then do
-      let d₁ ← formatAux nCtx ctx d
-      return f!"[{cls}] {d₁}"
-    else
-      formatAux nCtx ctx d
+  | nCtx, ctx,       tagged _ d               => formatAux nCtx ctx d
   | nCtx, ctx,       nest n d                 => Format.nest n <$> formatAux nCtx ctx d
   | nCtx, ctx,       compose d₁ d₂            => return (← formatAux nCtx ctx d₁) ++ (← formatAux nCtx ctx d₂)
   | nCtx, ctx,       group d                  => Format.group <$> formatAux nCtx ctx d
-  | nCtx, ctx,       node ds                  => Format.nest 2 <$> ds.foldlM (fun r d => return r ++ Format.line ++ (← formatAux nCtx ctx d)) Format.nil
+  | nCtx, ctx,       trace cls header children _ => do
+    let msg := f!"[{cls}] {(← formatAux nCtx ctx header).nest 2}"
+    let children ← children.mapM (formatAux nCtx ctx)
+    return .nest 2 (.joinSep (msg::children.toList) "\n")
 
 protected def format (msgData : MessageData) : IO Format :=
   formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index fee4999d5925..d8e5c84e8dd2 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -254,6 +254,18 @@ private def mkFun (constName : Name) : MetaM (Expr × Expr) := do
   let fType ← instantiateTypeLevelParams cinfo us
   return (f, fType)
 
+private def withAppBuilderTrace [ToMessageData α] [ToMessageData β]
+    (f : α) (xs : β) (k : MetaM Expr) : MetaM Expr :=
+  let emoji | .ok .. => checkEmoji | .error .. => crossEmoji
+  withTraceNode `Meta.appBuilder (return m!"{emoji ·} f: {f}, xs: {xs}") do
+    try
+      let res ← k
+      trace[Meta.appBuilder.result] res
+      pure res
+    catch ex =>
+      trace[Meta.appBuilder.error] ex.toMessageData
+      throw ex
+
 /--
   Return the application `constName xs`.
   It tries to fill the implicit arguments before the last element in `xs`.
@@ -264,19 +276,15 @@ private def mkFun (constName : Name) : MetaM (Expr × Expr) := do
   Given a `x : (([Decidable p] → Bool) × Nat`, ``mkAppM `Prod.fst #[x]`` returns `@Prod.fst ([Decidable p] → Bool) Nat x`
 -/
 def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := do
-  traceCtx `Meta.appBuilder <| withNewMCtxDepth do
+  withAppBuilderTrace constName xs do withNewMCtxDepth do
     let (f, fType) ← mkFun constName
-    let r ← mkAppMArgs f fType xs
-    trace[Meta.appBuilder] "constName: {constName}, xs: {xs}, result: {r}"
-    return r
+    mkAppMArgs f fType xs
 
 /-- Similar to `mkAppM`, but takes an `Expr` instead of a constant name. -/
 def mkAppM' (f : Expr) (xs : Array Expr) : MetaM Expr := do
   let fType ← inferType f
-  traceCtx `Meta.appBuilder <| withNewMCtxDepth do
-    let r ← mkAppMArgs f fType xs
-    trace[Meta.appBuilder] "f: {f}, xs: {xs}, result: {r}"
-    return r
+  withAppBuilderTrace f xs do withNewMCtxDepth do
+    mkAppMArgs f fType xs
 
 private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat → Array Expr → Nat → Array MVarId → Expr → MetaM Expr
   | i, args, j, instMVars, Expr.forallE n d b bi => do
@@ -325,14 +333,14 @@ private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat →
   fails because the only explicit argument `(a : α)` is not sufficient for inferring the remaining arguments,
   we would need the expected type. -/
 def mkAppOptM (constName : Name) (xs : Array (Option Expr)) : MetaM Expr := do
-  traceCtx `Meta.appBuilder <| withNewMCtxDepth do
+  withAppBuilderTrace constName xs do withNewMCtxDepth do
     let (f, fType) ← mkFun constName
     mkAppOptMAux f xs 0 #[] 0 #[] fType
 
 /-- Similar to `mkAppOptM`, but takes an `Expr` instead of a constant name -/
 def mkAppOptM' (f : Expr) (xs : Array (Option Expr)) : MetaM Expr := do
   let fType ← inferType f
-  traceCtx `Meta.appBuilder <| withNewMCtxDepth do
+  withAppBuilderTrace f xs do withNewMCtxDepth do
     mkAppOptMAux f xs 0 #[] 0 #[] fType
 
 def mkEqNDRec (motive h1 h2 : Expr) : MetaM Expr := do
@@ -581,6 +589,9 @@ def mkLE (a b : Expr) : MetaM Expr := mkBinaryRel ``LE ``LE.le a b
 /-- Return `a < b`. This method assumes `a` and `b` have the same type. -/
 def mkLT (a b : Expr) : MetaM Expr := mkBinaryRel ``LT ``LT.lt a b
 
-builtin_initialize registerTraceClass `Meta.appBuilder
+builtin_initialize do
+  registerTraceClass `Meta.appBuilder
+  registerTraceClass `Meta.appBuilder.result (inherited := true)
+  registerTraceClass `Meta.appBuilder.error (inherited := true)
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 16e3f020ed91..c08f136ca8fe 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -1577,29 +1577,29 @@ def mkLevelStuckErrorMessage (entry : PostponedEntry) : MetaM MessageData := do
 def mkLevelErrorMessage (entry : PostponedEntry) : MetaM MessageData := do
   mkLeveErrorMessageCore "failed to solve universe constraint" entry
 
-private def processPostponedStep (exceptionOnFailure : Bool) : MetaM Bool :=
-  traceCtx `Meta.isLevelDefEq.postponed.step do
-    let ps ← getResetPostponed
-    for p in ps do
-      unless (← withReader (fun ctx => { ctx with defEqCtx? := p.ctx? }) <| isLevelDefEqAux p.lhs p.rhs) do
-        if exceptionOnFailure then
-          withRef p.ref do
-            throwError (← mkLevelErrorMessage p)
-        else
-          return false
-    return true
+private def processPostponedStep (exceptionOnFailure : Bool) : MetaM Bool := do
+  let ps ← getResetPostponed
+  for p in ps do
+    unless (← withReader (fun ctx => { ctx with defEqCtx? := p.ctx? }) <| isLevelDefEqAux p.lhs p.rhs) do
+      if exceptionOnFailure then
+        withRef p.ref do
+          throwError (← mkLevelErrorMessage p)
+      else
+        return false
+  return true
 
 partial def processPostponed (mayPostpone : Bool := true) (exceptionOnFailure := false) : MetaM Bool := do
   if (← getNumPostponed) == 0 then
     return true
   else
-    traceCtx `Meta.isLevelDefEq.postponed do
+    let numPostponedBegin ← getNumPostponed
+    withTraceNode `Meta.isLevelDefEq.postponed
+        (fun _ => return m!"processing #{numPostponedBegin} postponed is-def-eq level constraints") do
       let rec loop : MetaM Bool := do
         let numPostponed ← getNumPostponed
         if numPostponed == 0 then
           return true
         else
-          trace[Meta.isLevelDefEq.postponed] "processing #{numPostponed} postponed is-def-eq level constraints"
           if !(← processPostponedStep exceptionOnFailure) then
             return false
           else
@@ -1654,17 +1654,12 @@ partial def processPostponed (mayPostpone : Bool := true) (exceptionOnFailure :=
   Determines whether two universe level expressions are definitionally equal to each other.
 -/
 def isLevelDefEq (u v : Level) : MetaM Bool :=
-  traceCtx `Meta.isLevelDefEq do
-    let b ← checkpointDefEq (mayPostpone := true) <| Meta.isLevelDefEqAux u v
-    trace[Meta.isLevelDefEq] "{u} =?= {v} ... {if b then "success" else "failure"}"
-    return b
+  checkpointDefEq (mayPostpone := true) <| Meta.isLevelDefEqAux u v
 
 /-- See `isDefEq`. -/
 def isExprDefEq (t s : Expr) : MetaM Bool :=
-  traceCtx `Meta.isDefEq <| withReader (fun ctx => { ctx with defEqCtx? := some { lhs := t, rhs := s, lctx := ctx.lctx, localInstances := ctx.localInstances } }) do
-    let b ← checkpointDefEq (mayPostpone := true) <| Meta.isExprDefEqAux t s
-    trace[Meta.isDefEq] "{t} =?= {s} ... {if b then "success" else "failure"}"
-    return b
+  withReader (fun ctx => { ctx with defEqCtx? := some { lhs := t, rhs := s, lctx := ctx.lctx, localInstances := ctx.localInstances } }) do
+    checkpointDefEq (mayPostpone := true) <| Meta.isExprDefEqAux t s
 
 /--
   Determines whether two expressions are definitionally equal to each other.
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 47582e08502a..ea05f613ae95 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -187,8 +187,13 @@ where
 Throw an exception if `e` is not type correct.
 -/
 def check (e : Expr) : MetaM Unit :=
-  traceCtx `Meta.check do
-    withTransparency TransparencyMode.all $ checkAux e
+  withTraceNode `Meta.check (fun res =>
+      return m!"{if res.isOk then checkEmoji else crossEmoji} {e}") do
+    try
+      withTransparency TransparencyMode.all $ checkAux e
+    catch ex =>
+      trace[Meta.check] ex.toMessageData
+      throw ex
 
 /--
 Return true if `e` is type correct.
@@ -197,12 +202,10 @@ def isTypeCorrect (e : Expr) : MetaM Bool := do
   try
     check e
     pure true
-  catch ex =>
-    trace[Meta.typeError] ex.toMessageData
+  catch _ =>
     pure false
 
 builtin_initialize
   registerTraceClass `Meta.check
-  registerTraceClass `Meta.typeError
 
 end Lean.Meta
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index bf52ed170a16..e4107ba760cf 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -314,20 +314,18 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
   isDefEqBindingAux lctx #[] a b #[]
 
 private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
-  traceCtx `Meta.isDefEq.assign.checkTypes do
+  withTraceNode `Meta.isDefEq.assign.checkTypes (return m!"{exceptBoolEmoji ·} ({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do
     if !mvar.isMVar then
-      trace[Meta.isDefEq.assign.final] "metavariable expected at {mvar} := {v}"
+      trace[Meta.isDefEq.assign.checkTypes] "metavariable expected"
       return false
     else
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
       let vType ← inferType v
       if (← withTransparency TransparencyMode.default <| Meta.isExprDefEqAux mvarType vType) then
-        trace[Meta.isDefEq.assign.final] "{mvar} := {v}"
         mvar.mvarId!.assign v
         pure true
       else
-        trace[Meta.isDefEq.assign.typeMismatch] "{mvar} : {mvarType} := {v} : {vType}"
         pure false
 
 /--
@@ -1018,8 +1016,7 @@ private partial def processConstApprox (mvar : Expr) (args : Array Expr) (patter
 /-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`.
     It assumes `?m` is unassigned. -/
 private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :=
-  traceCtx `Meta.isDefEq.assign do
-    trace[Meta.isDefEq.assign] "{mvarApp} := {v}"
+  withTraceNode `Meta.isDefEq.assign (return m!"{exceptBoolEmoji ·} {mvarApp} := {v}") do
     let mvar := mvarApp.getAppFn
     let mvarDecl ← mvar.mvarId!.getDecl
     let rec process (i : Nat) (args : Array Expr) (v : Expr) := do
@@ -1135,7 +1132,7 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do
   unless info.hints.isRegular || isMatcherCore (← getEnv) tFn.constName! do
     unless t.hasExprMVar || s.hasExprMVar do
       return false
-  traceCtx `Meta.isDefEq.delta do
+  withTraceNode `Meta.isDefEq.delta (return m!"{exceptBoolEmoji ·} {t} =?= {s}") do
     /-
       We process arguments before universe levels to reduce a source of brittleness in the TC procedure.
 
@@ -1156,12 +1153,8 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do
       Then the entry-point for `isDefEq` checks the flag before returning `true`.
     -/
     checkpointDefEq do
-      let b ← isDefEqArgs tFn t.getAppArgs s.getAppArgs
-              <&&>
-              isListLevelDefEqAux tFn.constLevels! sFn.constLevels!
-      unless b do
-        trace[Meta.isDefEq.delta] "heuristic failed {t} =?= {s}"
-      pure b
+      isDefEqArgs tFn t.getAppArgs s.getAppArgs <&&>
+        isListLevelDefEqAux tFn.constLevels! sFn.constLevels!
 
 /-- Auxiliary method for isDefEqDelta -/
 private abbrev unfold (e : Expr) (failK : MetaM α) (successK : Expr → MetaM α) : MetaM α := do
@@ -1731,9 +1724,8 @@ private def cacheResult (key : Expr × Expr) (result : Bool) : MetaM Unit := do
 
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
-  trace[Meta.isDefEq.step] "{t} =?= {s}"
+  withTraceNode `Meta.isDefEq (return m!"{exceptBoolEmoji ·} {t} =?= {s}") do
   checkMaxHeartbeats "isDefEq"
-  withNestedTraces do
   whenUndefDo (isDefEqQuick t s) do
   whenUndefDo (isDefEqProofIrrel t s) do
   -- We perform `whnfCore` again with `deltaAtProj := true` at `isExprDefEqExpensive` after `isDefEqProj`
@@ -1772,9 +1764,9 @@ builtin_initialize
   registerTraceClass `Meta.isDefEq
   registerTraceClass `Meta.isDefEq.foApprox
   registerTraceClass `Meta.isDefEq.constApprox
-  registerTraceClass `Meta.isDefEq.delta
-  registerTraceClass `Meta.isDefEq.step
+  registerTraceClass `Meta.isDefEq.delta (inherited := true)
   registerTraceClass `Meta.isDefEq.assign
+  registerTraceClass `Meta.isDefEq.assign.checkTypes (inherited := true)
   registerTraceClass `Meta.isDefEq.eta.struct
 
 end Lean.Meta
diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index dee6aedca4e9..a7ed14ac204a 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -86,11 +86,11 @@ mutual
   @[export lean_is_level_def_eq]
   partial def isLevelDefEqAuxImpl : Level → Level → MetaM Bool
     | Level.succ lhs, Level.succ rhs => isLevelDefEqAux lhs rhs
-    | lhs, rhs => do
+    | lhs, rhs =>
+      withTraceNode `Meta.isLevelDefEq (return m!"{exceptBoolEmoji ·} {lhs} =?= {rhs}") do
       if lhs.getLevelOffset == rhs.getLevelOffset then
         return lhs.getOffset == rhs.getOffset
       else
-        trace[Meta.isLevelDefEq.step] "{lhs} =?= {rhs}"
         let lhs' ← instantiateLevelMVars lhs
         let lhs' := lhs'.normalize
         let rhs' ← instantiateLevelMVars rhs
@@ -119,6 +119,6 @@ end
 
 builtin_initialize
   registerTraceClass `Meta.isLevelDefEq
-  registerTraceClass `Meta.isLevelDefEq.step
+  registerTraceClass `Meta.isLevelDefEq.stuck (inherited := true)
 
 end Lean.Meta
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index cac95fde4517..bf5a85087352 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -23,6 +23,7 @@ register_builtin_option synthInstance.maxSize : Nat := {
   defValue := 128
   descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure"
 }
+
 namespace SynthInstance
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -207,9 +208,9 @@ def getInstances (type : Expr) : MetaM (Array Expr) := do
           else
             return some <| e.val.updateConst! (← us.mapM (fun _ => mkFreshLevelMVar))
         | _ => panic! "global instance is not a constant"
-      trace[Meta.synthInstance.globalInstances] "{type}, {result}"
       let result := localInstances.foldl (init := result) fun (result : Array Expr) linst =>
         if linst.className == className then result.push linst.fvar else result
+      trace[Meta.synthInstance.instances] result
       return result
 
 def mkGeneratorNode? (key mvar : Expr) : MetaM (Option GeneratorNode) := do
@@ -229,16 +230,16 @@ def mkGeneratorNode? (key mvar : Expr) : MetaM (Option GeneratorNode) := do
   Create a new generator node for `mvar` and add `waiter` as its waiter.
   `key` must be `mkTableKey mctx mvarType`. -/
 def newSubgoal (mctx : MetavarContext) (key : Expr) (mvar : Expr) (waiter : Waiter) : SynthM Unit :=
-  withMCtx mctx do
-    trace[Meta.synthInstance.newSubgoal] key
+  withMCtx mctx do withTraceNode' `Meta.synthInstance do
     match (← mkGeneratorNode? key mvar) with
-    | none      => pure ()
+    | none      => pure ((), m!"no instances for {key}")
     | some node =>
       let entry : TableEntry := { waiters := #[waiter] }
       modify fun s =>
        { s with
          generatorStack := s.generatorStack.push node
          tableEntries   := s.tableEntries.insert key entry }
+      pure ((), m!"new goal {key}")
 
 def findEntry? (key : Expr) : SynthM (Option TableEntry) := do
   return (← get).tableEntries.find? key
@@ -316,7 +317,12 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array
       return { result with subgoals := result.subgoals.reverse }
   | _ => return result
 
-def tryResolveCore (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) := do
+/--
+  Try to synthesize metavariable `mvar` using the instance `inst`.
+  Remark: `mctx` is set using `withMCtx`.
+  If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
+  A subgoal is created for each instance implicit parameter of `inst`. -/
+def tryResolve (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) := do
   let mvar ← instantiateMVars mvar
   if !(← hasAssignableMVar mvar) then
     /- The metavariable `mvar` may have been assinged when solving typing constraints.
@@ -343,26 +349,13 @@ def tryResolveCore (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext 
   let localInsts ← getLocalInstances
   forallTelescopeReducing mvarType fun xs mvarTypeBody => do
     let ⟨subgoals, instVal, instTypeBody⟩ ← getSubgoals lctx localInsts xs inst
-    trace[Meta.synthInstance.tryResolve] "{mvarTypeBody} =?= {instTypeBody}"
+    withTraceNode `Meta.synthInstance.tryResolve (withMCtx (← getMCtx) do
+        return m!"{exceptOptionEmoji ·} {← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
     if (← isDefEq mvarTypeBody instTypeBody) then
       let instVal ← mkLambdaFVars xs instVal
       if (← isDefEq mvar instVal) then
-        trace[Meta.synthInstance.tryResolve] "success"
         return some ((← getMCtx), subgoals)
-      else
-        trace[Meta.synthInstance.tryResolve] "failure assigning"
-        return none
-    else
-      trace[Meta.synthInstance.tryResolve] "failure"
-      return none
-
-/--
-  Try to synthesize metavariable `mvar` using the instance `inst`.
-  Remark: `mctx` contains `mvar`.
-  If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
-  A subgoal is created for each instance implicit parameter of `inst`. -/
-def tryResolve (mctx : MetavarContext) (mvar : Expr) (inst : Expr) : SynthM (Option (MetavarContext × List Expr)) :=
-  traceCtx `Meta.synthInstance.tryResolve <| withMCtx mctx <| tryResolveCore mvar inst
+    return none
 
 /--
   Assign a precomputed answer to `mvar`.
@@ -398,9 +391,8 @@ def isNewAnswer (oldAnswers : Array Answer) (answer : Answer) : Bool :=
 
 private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
   withMCtx cNode.mctx do
-    traceM `Meta.synthInstance.newAnswer do pure m!"size: {cNode.size}, {← inferType cNode.mvar}"
     let val ← instantiateMVars cNode.mvar
-    trace[Meta.synthInstance.newAnswer] "val: {val}"
+    trace[Meta.synthInstance.newAnswer] "size: {cNode.size}, val: {val}"
     let result ← abstractMVars val -- assignable metavariables become parameters
     let resultType ← inferType result.expr
     return { result, resultType, size := cNode.size + 1 }
@@ -410,10 +402,12 @@ private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
   That is, `cNode.subgoals == []`.
   And then, store it in the tabled entries map, and wakeup waiters. -/
 def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
+  withMCtx cNode.mctx do
   if cNode.size ≥ (← read).maxResultSize then
-    traceM `Meta.synthInstance.discarded do withMCtx cNode.mctx do pure m!"size: {cNode.size} ≥ {(← read).maxResultSize}, {← inferType cNode.mvar}"
-    return ()
+      trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
   else
+    withTraceNode `Meta.synthInstance.answer
+      (fun _ => return m!"{checkEmoji} {← instantiateMVars (← inferType cNode.mvar)}") do
     let answer ← mkAnswer cNode
     -- Remark: `answer` does not contain assignable or assigned metavariables.
     let key := cNode.key
@@ -527,11 +521,14 @@ def generate : SynthM Unit := do
     let inst := gNode.instances.get! idx
     let mctx := gNode.mctx
     let mvar := gNode.mvar
-    trace[Meta.synthInstance.generate] "instance {inst}"
-    modifyTop fun gNode => { gNode with currInstanceIdx := idx }
-    match (← tryResolve mctx mvar inst) with
-    | none                  => return ()
-    | some (mctx, subgoals) => consume { key, mvar, subgoals, mctx, size := 0 }
+    discard do withMCtx mctx do
+      withTraceNode `Meta.synthInstance
+        (return m!"{exceptOptionEmoji ·} apply {inst} to {← instantiateMVars (← inferType mvar)}") do
+      modifyTop fun gNode => { gNode with currInstanceIdx := idx }
+      if let some (mctx, subgoals) ← tryResolve mvar inst then
+        consume { key, mvar, subgoals, mctx, size := 0 }
+        return some ()
+      return none
 
 def getNextToResume : SynthM (ConsumerNode × Answer) := do
   let r := (← get).resumeStack.back
@@ -549,10 +546,13 @@ def resume : SynthM Unit := do
     match (← tryAnswer cNode.mctx mvar answer) with
     | none      => return ()
     | some mctx =>
-      withMCtx mctx <| traceM `Meta.synthInstance.resume do
-        let goal    ← inferType cNode.mvar
-        let subgoal ← inferType mvar
-        return m!"size: {cNode.size + answer.size}, {goal} <== {subgoal}"
+      withMCtx mctx do
+      let goal    ← inferType cNode.mvar
+      let subgoal ← inferType mvar
+      withTraceNode `Meta.synthInstance.resume
+        (fun _ => withMCtx cNode.mctx do
+          return m!"propagating {← instantiateMVars answer.resultType} to subgoal {← instantiateMVars subgoal} of {← instantiateMVars goal}") do
+      trace[Meta.synthInstance.resume] "size: {cNode.size + answer.size}"
       consume { key := cNode.key, mvar := cNode.mvar, subgoals := rest, mctx, size := cNode.size + answer.size }
 
 def step : SynthM Bool := do
@@ -576,12 +576,10 @@ partial def synth : SynthM (Option AbstractMVarsResult) := do
     | none        => synth
     | some result => return result
   else
-    trace[Meta.synthInstance] "failed"
     return none
 
 def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult) :=
-  withCurrHeartbeats <| traceCtx `Meta.synthInstance do
-     trace[Meta.synthInstance] "main goal {type}"
+  withCurrHeartbeats do
      let mvar ← mkFreshExprMVar type
      let key  ← mkTableKey type
      let action : SynthM (Option AbstractMVarsResult) := do
@@ -679,9 +677,10 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     match s.cache.synthInstance.find? type with
     | some result => pure result
     | none        =>
+      withTraceNode `Meta.synthInstance
+        (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
       let result? ← withNewMCtxDepth do
         let normType ← preprocessOutParam type
-        trace[Meta.synthInstance] "preprocess: {type} ==> {normType}"
         SynthInstance.main normType maxResultSize
       let resultHasUnivMVars := if let some result := result? then !result.paramNames.isEmpty else false
       let result? ← match result? with
@@ -782,11 +781,9 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <|
 builtin_initialize
   registerTraceClass `Meta.synthPending
   registerTraceClass `Meta.synthInstance
-  registerTraceClass `Meta.synthInstance.globalInstances
-  registerTraceClass `Meta.synthInstance.newSubgoal
-  registerTraceClass `Meta.synthInstance.tryResolve
-  registerTraceClass `Meta.synthInstance.resume
-  registerTraceClass `Meta.synthInstance.generate
+  registerTraceClass `Meta.synthInstance.instances (inherited := true)
+  registerTraceClass `Meta.synthInstance.tryResolve (inherited := true)
+  registerTraceClass `Meta.synthInstance.resume (inherited := true)
   registerTraceClass `Meta.synthInstance.unusedArgs
   registerTraceClass `Meta.synthInstance.newAnswer
 
diff --git a/src/Lean/Meta/Tactic/Simp.lean b/src/Lean/Meta/Tactic/Simp.lean
index 7f8fda529891..aaadb53a4105 100644
--- a/src/Lean/Meta/Tactic/Simp.lean
+++ b/src/Lean/Meta/Tactic/Simp.lean
@@ -13,10 +13,10 @@ import Lean.Meta.Tactic.Simp.SimpAll
 namespace Lean
 
 builtin_initialize registerTraceClass `Meta.Tactic.simp
-builtin_initialize registerTraceClass `Meta.Tactic.simp.congr
-builtin_initialize registerTraceClass `Meta.Tactic.simp.discharge
-builtin_initialize registerTraceClass `Meta.Tactic.simp.rewrite
-builtin_initialize registerTraceClass `Meta.Tactic.simp.unify
+builtin_initialize registerTraceClass `Meta.Tactic.simp.congr (inherited := true)
+builtin_initialize registerTraceClass `Meta.Tactic.simp.discharge (inherited := true)
+builtin_initialize registerTraceClass `Meta.Tactic.simp.rewrite (inherited := true)
+builtin_initialize registerTraceClass `Meta.Tactic.simp.unify (inherited := true)
 builtin_initialize registerTraceClass `Debug.Meta.Tactic.simp
 
 end Lean
diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean
index 098a977a0d08..9c3957537f71 100644
--- a/src/Lean/Meta/UnificationHint.lean
+++ b/src/Lean/Meta/UnificationHint.lean
@@ -105,8 +105,9 @@ where
     withReducible <| Meta.isExprDefEqAux p e
 
   tryCandidate candidate : MetaM Bool :=
-    traceCtx `Meta.isDefEq.hint <| checkpointDefEq do
-      trace[Meta.isDefEq.hint] "trying hint {candidate} at {t} =?= {s}"
+    withTraceNode `Meta.isDefEq.hint
+      (return m!"{exceptBoolEmoji ·} hint {candidate} at {t} =?= {s}") do
+    checkpointDefEq do
       let cinfo ← getConstInfo candidate
       let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar
       let val ← instantiateValueLevelParams cinfo us
diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index 808532b07a92..531c6f0f1dda 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -66,7 +66,8 @@ private partial def noContext : MessageData → MessageData
   | MessageData.group msg  => MessageData.group (noContext msg)
   | MessageData.compose msg₁ msg₂ => MessageData.compose (noContext msg₁) (noContext msg₂)
   | MessageData.tagged tag msg => MessageData.tagged tag (noContext msg)
-  | MessageData.node msgs => MessageData.node (msgs.map noContext)
+  | MessageData.trace cls header children collapsed =>
+    MessageData.trace cls (noContext header) (children.map noContext) collapsed
   | msg => msg
 
 -- strip context (including environments with registered pretty printers) to prevent infinite recursion when pretty printing pretty printer error
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 8f1b41081a18..7ac184f81ec5 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -627,22 +627,22 @@ open TopDownAnalyze SubExpr
 
 def topDownAnalyze (e : Expr) : MetaM OptionsPerPos := do
   let s₀ ← get
-  traceCtx `pp.analyze do
+  withTraceNode `pp.analyze (fun _ => return e) do
     withReader (fun ctx => { ctx with config := Elab.Term.setElabConfig ctx.config }) do
       let ϕ : AnalyzeM OptionsPerPos := do withNewMCtxDepth analyze; pure (← get).annotations
       try
         let knowsType := getPPAnalyzeKnowsType (← getOptions)
         ϕ { knowsType := knowsType, knowsLevel := knowsType, subExpr := mkRoot e }
           |>.run' { : TopDownAnalyze.State }
-      catch _ =>
-        trace[pp.analyze.error] "failed"
+      catch e =>
+        trace[pp.analyze.error] "failed {e.toMessageData}"
         pure {}
       finally set s₀
 
 builtin_initialize
   registerTraceClass `pp.analyze
-  registerTraceClass `pp.analyze.annotate
-  registerTraceClass `pp.analyze.tryUnify
-  registerTraceClass `pp.analyze.error
+  registerTraceClass `pp.analyze.annotate (inherited := true)
+  registerTraceClass `pp.analyze.tryUnify (inherited := true)
+  registerTraceClass `pp.analyze.error (inherited := true)
 
 end Lean.PrettyPrinter.Delaborator
diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index df9de092dcba..067ea372e109 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -136,4 +136,13 @@ builtin_initialize
       i.ctx.runMetaM ti.lctx <|
         locationLinksFromDecl rc.srcSearchPath rc.doc.meta.uri nm none
 
+def lazyTraceChildrenToInteractive (children : WithRpcRef LazyTraceChildren) :
+    RequestM (RequestTask (Array (TaggedText MsgEmbed))) :=
+  RequestM.asTask do
+    let ⟨indent, children⟩ := children
+    children.mapM fun ⟨child⟩ =>
+      msgToInteractive child (hasWidgets := true) (indent := indent)
+
+builtin_initialize registerBuiltinRpcProcedure ``lazyTraceChildrenToInteractive _ _ lazyTraceChildrenToInteractive
+
 end Lean.Widget
diff --git a/src/Lean/Util/Sorry.lean b/src/Lean/Util/Sorry.lean
index cb57adfed787..34012824ccac 100644
--- a/src/Lean/Util/Sorry.lean
+++ b/src/Lean/Util/Sorry.lean
@@ -37,7 +37,7 @@ partial def MessageData.hasSorry : MessageData → Bool
   | group msg         => msg.hasSorry
   | compose msg₁ msg₂ => msg₁.hasSorry || msg₂.hasSorry
   | tagged _ msg      => msg.hasSorry
-  | node msgs         => msgs.any hasSorry
+  | trace _ msg msgs _ => msg.hasSorry || msgs.any hasSorry
   | _                 => false
 
 partial def MessageData.hasSyntheticSorry (msg : MessageData) : Bool :=
@@ -51,7 +51,7 @@ where
   | group msg               => visit msg
   | compose msg₁ msg₂       => visit msg₁ || visit msg₂
   | tagged _ msg            => visit msg
-  | node msgs               => msgs.any hasSyntheticSorry
+  | trace _ msg msgs _      => msg.hasSyntheticSorry || msgs.any hasSyntheticSorry
   | _                       => false
 
 def Exception.hasSyntheticSorry : Exception → Bool
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 7d0af333024a..0830bdf510c6 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -5,7 +5,56 @@ Authors: Sebastian Ullrich, Leonardo de Moura
 -/
 import Lean.Message
 import Lean.MonadEnv
-universe u
+
+/-!
+# Trace messages
+
+Trace messages explain to the user what problem Lean solved and what steps it took.
+Think of trace messages like a figure in a paper.
+
+They are shown in the editor as a collapsible tree,
+usually as `[class.name] message ▸`.
+Every trace node has a class name, a message, and an array of children.
+This module provides the API to produce trace messages,
+the key entry points are:
+- ``registerTraceMessage `class.name`` registers a trace class
+- ``withTraceNode `class.name (fun result => return msg) do body`
+  produces a trace message containing the trace messages in `body` as children
+- `trace[class.name] msg` produces a trace message without children
+
+Users can enable trace options for a class using
+`set_option trace.class.name true`.
+This only enables trace messages for the `class.name` trace class
+as well as child classes that are explicitly marked as inherited
+(see `registerTraceClass`).
+
+Internally, trace messages are stored as `MessageData`:
+`.trace cls msg #[.trace .., .trace ..]`
+
+When writing trace messages,
+try to follow these guidelines:
+1. **Expansion progressively increases detail.**
+  Each level of expansion (of the trace node in the editor) should reveal more details.
+  For example, the unexpanded node should show the top-level goal.
+  Expanding it should show a list of steps.
+  Expanding one of the steps then shows what happens during that step.
+2. **One trace message per step.**
+  The `[trace.class]` marker functions as a visual bullet point,
+  making it easy to identify the different steps at a glance.
+3. **Outcome first.**
+  The top-level trace message should already show whether the action failed or succeeded,
+  as opposed to a "success" trace message that comes pages later.
+4. **Be concise.**
+  Keep messages short.
+  Avoid repetitive text.
+  (This is also why the editor plugins abbreviate the common prefixes.)
+5. **Emoji are concisest.**
+  Several helper functions in this module help with a consistent emoji language.
+6. **Good defaults.**
+  Setting `set_option trace.Meta.synthInstance true` (etc.)
+  should produce great trace messages out-of-the-box,
+  without needing extra options to tweak it.
+-/
 
 namespace Lean
 
@@ -17,20 +66,10 @@ structure TraceElem where
   deriving Inhabited
 
 structure TraceState where
-  enabled : Bool := true
   traces  : PersistentArray TraceElem := {}
   deriving Inhabited
 
-namespace TraceState
-
-private def toFormat (traces : PersistentArray TraceElem) (sep : Format) : IO Format :=
-  traces.size.foldM
-    (fun i r => do
-      let curr ← (traces.get! i).msg.format
-      return if i > 0 then r ++ sep ++ curr else r ++ curr)
-    Format.nil
-
-end TraceState
+builtin_initialize inheritedTraceOptions : IO.Ref (Std.HashSet Name) ← IO.mkRef ∅
 
 class MonadTrace (m : Type → Type) where
   modifyTraceState : (TraceState → TraceState) → m Unit
@@ -42,38 +81,29 @@ instance (m n) [MonadLift m n] [MonadTrace m] : MonadTrace n where
   modifyTraceState := fun f => liftM (modifyTraceState f : m _)
   getTraceState    := liftM (getTraceState : m _)
 
-variable {α : Type} {m : Type → Type} [Monad m] [MonadTrace m]
+variable {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadOptions m] [MonadLiftT IO m]
 
-def printTraces {m} [Monad m] [MonadTrace m] [MonadLiftT IO m] : m Unit := do
-  let traceState ← getTraceState
-  traceState.traces.forM fun m => do
-    let d ← m.msg.format
-    IO.println d
+def printTraces : m Unit := do
+  for {msg, ..} in (← getTraceState).traces do
+    IO.println (← msg.format)
 
-def resetTraceState {m} [MonadTrace m] : m Unit :=
+def resetTraceState : m Unit :=
   modifyTraceState (fun _ => {})
 
-private def checkTraceOptionAux (opts : Options) : Name → Bool
-  | n@(.str p _) => opts.getBool n || (!opts.contains n && checkTraceOptionAux opts p)
-  | _            => false
-
-def checkTraceOption (opts : Options) (cls : Name) : Bool :=
-  if opts.isEmpty then false
-  else checkTraceOptionAux opts (`trace ++ cls)
-
-private def checkTraceOptionM [MonadOptions m] (cls : Name) : m Bool :=
-  return checkTraceOption (← getOptions) cls
+private def checkTraceOption (inherited : Std.HashSet Name) (opts : Options) (cls : Name) : Bool :=
+  !opts.isEmpty && go (`trace ++ cls)
+where
+  go (opt : Name) : Bool :=
+    if let some enabled := opts.get? opt then
+      enabled
+    else if let .str parent _ := opt then
+      inherited.contains opt && go parent
+    else
+      false
 
-@[inline] def isTracingEnabledFor [MonadOptions m] (cls : Name) : m Bool := do
-  let s ← getTraceState
-  if !s.enabled then pure false
-  else checkTraceOptionM cls
-
-@[inline] def enableTracing (b : Bool) : m Bool := do
-  let s ← getTraceState
-  let oldEnabled := s.enabled
-  modifyTraceState fun s => { s with enabled := b }
-  pure oldEnabled
+def isTracingEnabledFor (cls : Name) : m Bool := do
+  let inherited ← (inheritedTraceOptions.get : IO _)
+  pure (checkTraceOption inherited (← getOptions) cls)
 
 @[inline] def getTraces : m (PersistentArray TraceElem) := do
   let s ← getTraceState
@@ -85,14 +115,6 @@ private def checkTraceOptionM [MonadOptions m] (cls : Name) : m Bool :=
 @[inline] def setTraceState (s : TraceState) : m Unit :=
   modifyTraceState fun _ => s
 
-private def addNode (oldTraces : PersistentArray TraceElem) (cls : Name) (ref : Syntax) : m Unit :=
-  modifyTraces fun traces =>
-    if traces.isEmpty then
-      oldTraces
-    else
-      let d := MessageData.tagged (cls ++ `_traceCtx) (MessageData.node (traces.toArray.map fun elem => elem.msg))
-      oldTraces.push { ref := ref, msg := d }
-
 private def getResetTraces : m (PersistentArray TraceElem) := do
   let oldTraces ← getTraces
   modifyTraces fun _ => {}
@@ -101,22 +123,15 @@ private def getResetTraces : m (PersistentArray TraceElem) := do
 section
 variable [MonadRef m] [AddMessageContext m] [MonadOptions m]
 
-private def addTraceOptions (msg : MessageData) : MessageData :=
-  match msg with
-  | MessageData.withContext ctx msg => MessageData.withContext { ctx with opts := ctx.opts.setBool `pp.analyze false } msg
-  | msg => msg
-
 def addRawTrace (msg : MessageData) : m Unit := do
   let ref ← getRef
   let msg ← addMessageContext msg
-  let msg := addTraceOptions msg
-  modifyTraces fun traces => traces.push { ref, msg }
+  modifyTraces (·.push { ref, msg })
 
 def addTrace (cls : Name) (msg : MessageData) : m Unit := do
   let ref ← getRef
   let msg ← addMessageContext msg
-  let msg := addTraceOptions msg
-  modifyTraces fun traces => traces.push { ref := ref, msg := MessageData.tagged (cls ++ `_traceMsg) m!"[{cls}] {msg}" }
+  modifyTraces (·.push { ref, msg := .trace cls msg #[] })
 
 @[inline] def trace (cls : Name) (msg : Unit → MessageData) : m Unit := do
   if (← isTracingEnabledFor cls) then
@@ -127,24 +142,49 @@ def addTrace (cls : Name) (msg : MessageData) : m Unit := do
     let msg ← mkMsg
     addTrace cls msg
 
-@[inline] def traceCtx [MonadFinally m] (cls : Name) (ctx : m α) : m α := do
-  let b ← isTracingEnabledFor cls
-  if !b then
-    let old ← enableTracing false
-    try ctx finally enableTracing old
+private def addTraceNode (oldTraces : PersistentArray TraceElem)
+    (cls : Name) (ref : Syntax) (msg : MessageData) (collapsed : Bool) : m Unit :=
+  withRef ref do
+  let msg ← addMessageContext msg
+  modifyTraces fun newTraces =>
+    oldTraces.push { ref, msg := .trace cls msg (newTraces.toArray.map (·.msg)) collapsed }
+
+def withTraceNode [MonadExcept ε m] (cls : Name) (msg : Except ε α → m MessageData) (k : m α)
+    (collapsed := true) : m α := do
+  if !(← isTracingEnabledFor cls) then
+    k
   else
     let ref ← getRef
-    let oldCurrTraces ← getResetTraces
-    try ctx finally addNode oldCurrTraces cls ref
+    let oldTraces ← getResetTraces
+    let res ← observing k
+    addTraceNode oldTraces cls ref (← msg res) collapsed
+    MonadExcept.ofExcept res
 
--- TODO: delete after fix old frontend
-def MonadTracer.trace (cls : Name) (msg : Unit → MessageData) : m Unit :=
-  Lean.trace cls msg
+def withTraceNode' [MonadExcept Exception m] (cls : Name) (k : m (α × MessageData)) (collapsed := true) : m α :=
+  let msg := fun
+    | .ok (_, msg) => return msg
+    | .error err => return err.toMessageData
+  Prod.fst <$> withTraceNode cls msg k collapsed
 
 end
 
-def registerTraceClass (traceClassName : Name) : IO Unit :=
-  registerOption (`trace ++ traceClassName) { group := "trace", defValue := false, descr := "enable/disable tracing for the given module and submodules" }
+/--
+Registers a trace class.
+
+By default, trace classes are not inherited;
+that is, `set_option trace.foo true` does not imply `set_option trace.foo.bar true`.
+Calling ``registerTraceClass `foo.bar (inherited := true)`` enables this inheritance
+on an opt-in basis.
+-/
+def registerTraceClass (traceClassName : Name) (inherited := false) : IO Unit := do
+  let optionName := `trace ++ traceClassName
+  registerOption optionName {
+    group := "trace"
+    defValue := false
+    descr := "enable/disable tracing for the given module and submodules"
+  }
+  if inherited then
+    inheritedTraceOptions.modify (·.insert optionName)
 
 macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
   let msg ← if s.raw.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
@@ -153,21 +193,18 @@ macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
     if (← Lean.isTracingEnabledFor cls) then
       Lean.addTrace cls $msg)
 
-private def withNestedTracesFinalizer [Monad m] [MonadTrace m] (ref : Syntax) (currTraces : PersistentArray TraceElem) : m Unit := do
-  modifyTraces fun traces =>
-    if traces.size == 0 then
-      currTraces
-    else if traces.size == 1 && traces[0]!.msg.isNest then
-      currTraces ++ traces -- No nest of nest
-    else
-      let d := traces.foldl (init := MessageData.nil) fun d elem =>
-        if d.isNil then elem.msg else m!"{d}\n{elem.msg}"
-      currTraces.push { ref := ref, msg := MessageData.nestD d }
+def bombEmoji := "💥"
+def checkEmoji := "✅"
+def crossEmoji := "❌"
 
-@[inline] def withNestedTraces [Monad m] [MonadFinally m] [MonadTrace m] [MonadRef m] (x : m α) : m α := do
-  let currTraces ← getTraces
-  modifyTraces fun _ => {}
-  let ref ← getRef
-  try x finally withNestedTracesFinalizer ref currTraces
+def exceptBoolEmoji : Except ε Bool → String
+  | .error _ => bombEmoji
+  | .ok true => checkEmoji
+  | .ok false => crossEmoji
+
+def exceptOptionEmoji : Except ε (Option α) → String
+  | .error _ => bombEmoji
+  | .ok (some _) => checkEmoji
+  | .ok none => crossEmoji
 
 end Lean
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 59727ebf29e6..cf8f2cb68248 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -11,10 +11,21 @@ import Lean.Widget.InteractiveGoal
 namespace Lean.Widget
 open Lsp Server
 
+inductive StrictOrLazy (α β : Type) : Type
+  | strict : α → StrictOrLazy α β
+  | lazy : β → StrictOrLazy α β
+  deriving Inhabited, RpcEncodable
+
+structure LazyTraceChildren where
+  indent : Nat
+  children : Array (WithRpcRef MessageData)
+  deriving Std.TypeName
+
 inductive MsgEmbed where
   | expr : CodeWithInfos → MsgEmbed
   | goal : InteractiveGoal → MsgEmbed
-  | lazyTrace : Nat → Name → WithRpcRef MessageData → MsgEmbed
+  | trace (indent : Nat) (cls : Name) (msg : TaggedText MsgEmbed) (collapsed : Bool)
+      (children : StrictOrLazy (Array (TaggedText MsgEmbed)) (WithRpcRef LazyTraceChildren))
   deriving Inhabited, RpcEncodable
 
 /-- We embed objects in LSP diagnostics by storing them in the tag of an empty subtree (`text ""`).
@@ -32,9 +43,9 @@ def toDiagnostic (diag : InteractiveDiagnostic) : Lsp.Diagnostic :=
 where
   prettyTt (tt : TaggedText MsgEmbed) : String :=
     let tt : TaggedText MsgEmbed := tt.rewrite fun
-      | expr tt,         _     => TaggedText.text tt.stripTags
-      | goal g,          _     => TaggedText.text (toString g.pretty)
-      | lazyTrace _ _ _, subTt => subTt
+      | .expr tt,           _ => .text tt.stripTags
+      | .goal g,            _ => .text (toString g.pretty)
+      | .trace ..,          _ => .text "(trace)"
     tt.stripTags
 
 end InteractiveDiagnostic
@@ -50,9 +61,9 @@ private inductive EmbedFmt
   | goal (ctx : Elab.ContextInfo) (lctx : LocalContext) (g : MVarId)
   | /-- Some messages (in particular, traces) are too costly to print eagerly. Instead, we allow
     the user to expand sub-traces interactively. -/
-    lazyTrace (nCtx : NamingContext) (ctx? : Option MessageDataContext) (cls : Name) (m : MessageData)
-  | /-- Ignore any tags in this subtree. -/
-    ignoreTags
+    trace (cls : Name) (msg : Format) (collapsed : Bool)
+      (children : StrictOrLazy (Array Format) (Array MessageData))
+  | /-- Ignore any tags in this subtree. -/ ignoreTags
   deriving Inhabited
 
 private abbrev MsgFmtM := StateT (Array EmbedFmt) IO
@@ -60,7 +71,7 @@ private abbrev MsgFmtM := StateT (Array EmbedFmt) IO
 open MessageData in
 /-- We first build a `Nat`-tagged `Format` with the most shallow tag, if any,
 in every branch indexing into the array of embedded objects. -/
-private partial def msgToInteractiveAux (msgData : MessageData) (hasWidgets : Bool) : IO (Format × Array EmbedFmt) :=
+private partial def msgToInteractiveAux (msgData : MessageData) : IO (Format × Array EmbedFmt) :=
   go { currNamespace := Name.anonymous, openDecls := [] } none msgData #[]
 where
   pushEmbed (e : EmbedFmt) : MsgFmtM Nat :=
@@ -71,6 +82,17 @@ where
     let t ← pushEmbed EmbedFmt.ignoreTags
     return Format.tag t fmt
 
+  mkContextInfo (nCtx : NamingContext) (ctx : MessageDataContext) : Elab.ContextInfo := {
+    env           := ctx.env
+    mctx          := ctx.mctx
+    fileMap       := default
+    options       := ctx.opts
+    currNamespace := nCtx.currNamespace
+    openDecls     := nCtx.openDecls
+    -- Hack: to make sure unique ids created at `ppExprWithInfos` do not collide with ones in `ctx.mctx`
+    ngen          := { namePrefix := `_diag }
+  }
+
   go : NamingContext → Option MessageDataContext → MessageData → MsgFmtM Format
   | _,    _,         ofFormat fmt             => withIgnoreTags (pure fmt)
   | _,    _,         ofLevel u                => return format u
@@ -79,62 +101,59 @@ where
   | _,    none,      ofSyntax s               => withIgnoreTags (pure s.formatStx)
   | _,    none,      ofExpr e                 => return format (toString e)
   | nCtx, some ctx,  ofExpr e                 => do
-    let ci : Elab.ContextInfo := {
-      env           := ctx.env
-      mctx          := ctx.mctx
-      fileMap       := default
-      options       := ctx.opts
-      currNamespace := nCtx.currNamespace
-      openDecls     := nCtx.openDecls
-      -- Hack: to make sure unique ids created at `ppExprWithInfos` do not collide with ones in `ctx.mctx`
-      ngen          := { namePrefix := `_diag }
-    }
+    let ci := mkContextInfo nCtx ctx
     let (fmt, infos) ← ci.runMetaM ctx.lctx <| PrettyPrinter.ppExprWithInfos e
     let t ← pushEmbed <| EmbedFmt.expr ci infos
     return Format.tag t fmt
   | _,    none,      ofGoal mvarId            => pure $ "goal " ++ format (mkMVar mvarId)
-  | nCtx, some ctx,  ofGoal mvarId            => withIgnoreTags <| ppGoal (mkPPContext nCtx ctx) mvarId
+  | nCtx, some ctx,  ofGoal mvarId            =>
+    return .tag (← pushEmbed (.goal (mkContextInfo nCtx ctx) ctx.lctx mvarId)) "\n"
   | nCtx, _,         withContext ctx d        => go nCtx ctx d
   | _,    ctx,       withNamingContext nCtx d => go nCtx ctx d
-  | nCtx, ctx,       tagged t d               => do
-    -- We postfix trace contexts with `_traceCtx` in order to detect them in messages.
-    if let .str cls "_traceCtx" := t then
-      -- When interactive trace exploration is possible, we hide traces which can otherwise
-      -- take significant resources to pretty-print.
-      if hasWidgets then
-        let f ← pushEmbed <| EmbedFmt.lazyTrace nCtx ctx cls d
-        return Format.tag f s!"[{cls}] (trace hidden)"
-      else
-        go nCtx ctx d
-    else
-      go nCtx ctx d
+  | nCtx, ctx,       tagged _ d               => go nCtx ctx d
   | nCtx, ctx,       nest n d                 => Format.nest n <$> go nCtx ctx d
   | nCtx, ctx,       compose d₁ d₂            => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
   | nCtx, ctx,       group d                  => Format.group <$> go nCtx ctx d
-  | nCtx, ctx,       node ds                  => Format.nest 2 <$> ds.foldlM (fun r d => do let d ← go nCtx ctx d; pure $ r ++ Format.line ++ d) Format.nil
+  | nCtx, ctx,       .trace cls header children collapsed => do
+    let header := (← go nCtx ctx header).nest 4
+    let nodes ←
+      if collapsed && !children.isEmpty then
+        let children := children.map fun child =>
+          MessageData.withNamingContext nCtx <|
+            match ctx with
+            | some ctx => MessageData.withContext ctx child
+            | none     => child
+        pure (.lazy children)
+      else
+        pure (.strict (← children.mapM (go nCtx ctx)))
+    let e := .trace cls header collapsed nodes
+    pure (.tag (← pushEmbed e) ".\n")
 
 partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent : Nat := 0) : IO (TaggedText MsgEmbed) := do
-  let (fmt, embeds) ← msgToInteractiveAux msgData hasWidgets
-  let tt := TaggedText.prettyTagged fmt indent
+  if !hasWidgets then
+    return (TaggedText.prettyTagged (← msgData.format)).rewrite fun _ tt => .text tt.stripTags
+  let (fmt, embeds) ← msgToInteractiveAux msgData
   /- Here we rewrite a `TaggedText Nat` corresponding to a whole `MessageData` into one where
   the tags are `TaggedText MsgEmbed`s corresponding to embedded objects with their subtree
   empty (`text ""`). In other words, we terminate the `MsgEmbed`-tagged -tree at embedded objects
   and store the pretty-printed embed (which can itself be a `TaggedText`) in the tag. -/
-  tt.rewriteM fun (n, col) subTt =>
-    match embeds.get! n with
-    | EmbedFmt.expr ctx infos =>
-      let subTt' := tagExprInfos ctx infos subTt
-      return TaggedText.tag (MsgEmbed.expr subTt') (TaggedText.text subTt.stripTags)
-    | EmbedFmt.goal _   _    _ =>
-      -- TODO(WN): use InteractiveGoal types here
-      unreachable!
-    | EmbedFmt.lazyTrace nCtx ctx? cls m =>
-      let msg :=
-        match ctx? with
-        | some ctx => MessageData.withNamingContext nCtx <| MessageData.withContext ctx m
-        | none     => MessageData.withNamingContext nCtx m
-      return TaggedText.tag (MsgEmbed.lazyTrace col cls ⟨msg⟩) (TaggedText.text subTt.stripTags)
-    | EmbedFmt.ignoreTags => return TaggedText.text subTt.stripTags
+  let rec fmtToTT (fmt : Format) (indent : Nat) : IO (TaggedText MsgEmbed) :=
+    (TaggedText.prettyTagged fmt indent).rewriteM fun (n, col) tt =>
+      match embeds[n]! with
+        | .expr ctx infos =>
+          return .tag (.expr (tagExprInfos ctx infos tt)) default
+        | .goal ctx lctx g =>
+          ctx.runMetaM lctx do
+            return .tag (.goal (← goalToInteractive g)) default
+        | .trace cls msg collapsed children => do
+          let col := col + tt.stripTags.length - 2
+          let children ←
+            match children with
+              | .lazy children => pure <| .lazy ⟨{indent := col+2, children := children.map .mk}⟩
+              | .strict children => pure <| .strict (← children.mapM (fmtToTT · (col+2)))
+          return .tag (.trace indent cls (← fmtToTT msg col) collapsed children) default
+        | .ignoreTags => return .text tt.stripTags
+  fmtToTT fmt indent
 
 /-- Transform a Lean Message concerning the given text into an LSP Diagnostic. -/
 def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool) : IO InteractiveDiagnostic := do
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index 1237c65eb986..a5346e035215 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -1,5 +1,5 @@
 [Elab.info] command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption
-  [.] (Command.set_option "set_option" `trace.Elab.info) @ ⟨6, 0⟩-⟨6, 26⟩
+      [.] (Command.set_option "set_option" `trace.Elab.info) @ ⟨6, 0⟩-⟨6, 26⟩
 1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
 context:
 α✝ β : Type
@@ -8,68 +8,68 @@ x : Fam2 α✝ β
 a : α
 ⊢ α
 [Elab.info] command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
-  α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
-    [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
-    α : Type @ ⟨7, 13⟩-⟨7, 14⟩
-  a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
-  α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
-    [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
-    α : Type @ ⟨7, 13⟩-⟨7, 14⟩
-  a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
-  Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
-    [.] `Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
-    Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
-    α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
-      [.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
-      α : Type @ ⟨7, 26⟩-⟨7, 27⟩
-    β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
-      [.] `β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
-      β : Type @ ⟨7, 28⟩-⟨7, 29⟩
-  x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-  β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
-    [.] `β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
-    β : Type @ ⟨7, 33⟩-⟨7, 34⟩
-  _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
-  a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
-  x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-  _example.match_1 (fun α β x a => β) α β x a (fun α_1 a => ?m x α_1 a) fun n a =>
-    n : <failed-to-infer-type> @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
-    x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
-    [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-    @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-    Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-    [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
-    [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-    @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-    [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-    α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-    α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-    Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
-      α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
-    a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-    FVarAlias _uniq.669 -> _uniq.327
-    FVarAlias _uniq.668 -> _uniq.325
-    ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
-    [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-    Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-    [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
-    [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-    [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
-    [.] `n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
-    [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-    Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-    Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-    Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
-      n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
-    a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-    FVarAlias _uniq.700 -> _uniq.327
-    FVarAlias _uniq.699 -> _uniq.325
-    n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
-      [.] `n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
-      n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
-  @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
+      α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
+        [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
+        α : Type @ ⟨7, 13⟩-⟨7, 14⟩
+      a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
+      α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
+        [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
+        α : Type @ ⟨7, 13⟩-⟨7, 14⟩
+      a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
+      Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
+        [.] `Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
+        Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
+        α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
+          [.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
+          α : Type @ ⟨7, 26⟩-⟨7, 27⟩
+        β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
+          [.] `β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
+          β : Type @ ⟨7, 28⟩-⟨7, 29⟩
+      x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
+      β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
+        [.] `β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
+        β : Type @ ⟨7, 33⟩-⟨7, 34⟩
+      _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
+      a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
+      x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
+      _example.match_1 (fun α β x a => β) α β x a (fun α_1 a => ?m x α_1 a) fun n a =>
+        n : <failed-to-infer-type> @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
+        x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
+        [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
+        [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
+        Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
+        [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
+        [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
+        [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
+        [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
+        [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+        α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
+          α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
+        a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
+        FVarAlias _uniq.669 -> _uniq.327
+        FVarAlias _uniq.668 -> _uniq.325
+        ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
+        [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
+        Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
+        [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
+        [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
+        [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
+        [.] `n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
+        [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+        Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
+          n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
+        a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
+        FVarAlias _uniq.700 -> _uniq.327
+        FVarAlias _uniq.699 -> _uniq.325
+        n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
+          [.] `n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
+          n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
+      @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
diff --git a/tests/lean/1079.lean b/tests/lean/1079.lean
index 9d294800620a..d1a60108347c 100644
--- a/tests/lean/1079.lean
+++ b/tests/lean/1079.lean
@@ -2,7 +2,7 @@ theorem bad : ∀ (m n : Nat), (if m = n then Ordering.eq else Ordering.gt) = Or
   intros m n
   cases (Nat.decEq m n) with -- an error as expected: "alternative `isFalse` has not bee provided"
   | isTrue h =>
-    set_option trace.Meta.Tactic true in
+    set_option trace.Meta.Tactic.simp true in
     simp [h]
 
 theorem bad' : ∀ (m n : Nat), (if m = n then Ordering.eq else Ordering.gt) = Ordering.lt → False := by
diff --git a/tests/lean/1079.lean.expected.out b/tests/lean/1079.lean.expected.out
index e192d6538e87..36423069dabe 100644
--- a/tests/lean/1079.lean.expected.out
+++ b/tests/lean/1079.lean.expected.out
@@ -2,12 +2,12 @@
 [Meta.Tactic.simp.rewrite] h:1000, m ==> n
 [Meta.Tactic.simp.rewrite] eq_self:1000, n = n ==> True
 [Meta.Tactic.simp.unify] ite_self:1000, failed to unify
-  if ?c then ?a else ?a
-with
-  if True then Ordering.eq else Ordering.gt
+      if ?c then ?a else ?a
+    with
+      if True then Ordering.eq else Ordering.gt
 [Meta.Tactic.simp.rewrite] ite_true:1000, if True then Ordering.eq else Ordering.gt ==> Ordering.eq
 [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
-  ?a = ?a
-with
-  Ordering.eq = Ordering.lt
+      ?a = ?a
+    with
+      Ordering.eq = Ordering.lt
 [Meta.Tactic.simp.rewrite] false_implies:1000, False → False ==> True
diff --git a/tests/lean/366.lean.expected.out b/tests/lean/366.lean.expected.out
index ccac7ce637e4..f32fe47022ab 100644
--- a/tests/lean/366.lean.expected.out
+++ b/tests/lean/366.lean.expected.out
@@ -1,12 +1,6 @@
-[Meta.synthInstance] preprocess: Inhabited Nat ==> Inhabited Nat
-  [Meta.synthInstance] 
-    [Meta.synthInstance] main goal Inhabited Nat
-    [Meta.synthInstance.newSubgoal] Inhabited Nat
-    [Meta.synthInstance.globalInstances] Inhabited Nat, [@instInhabited, instInhabitedNat]
-    [Meta.synthInstance.generate] instance instInhabitedNat
-    [Meta.synthInstance.tryResolve] 
-      [Meta.synthInstance.tryResolve] Inhabited Nat =?= Inhabited Nat
-      [Meta.synthInstance.tryResolve] success
-    [Meta.synthInstance.newAnswer] size: 0, Inhabited Nat
-    [Meta.synthInstance.newAnswer] val: instInhabitedNat
+[Meta.synthInstance] ✅ Inhabited Nat
+  [Meta.synthInstance] new goal Inhabited Nat
+    [Meta.synthInstance.instances] #[@instInhabited, instInhabitedNat]
+  [Meta.synthInstance] ✅ apply instInhabitedNat to Inhabited Nat
+    [Meta.synthInstance.tryResolve] ✅ Inhabited Nat ≟ Inhabited Nat
   [Meta.synthInstance] result instInhabitedNat
diff --git a/tests/lean/815b.lean b/tests/lean/815b.lean
index c3dd07a13fad..33a2ea0cfe50 100644
--- a/tests/lean/815b.lean
+++ b/tests/lean/815b.lean
@@ -11,11 +11,5 @@ instance comp (f : β → γ) (g : α → β) [IsSmooth f] [IsSmooth g] : IsSmoo
 instance diag (f : β → δ → γ) (g : α → β) (h : α → δ) [IsSmooth f] [∀ b, IsSmooth (f b)] [IsSmooth g] [IsSmooth h] : IsSmooth (λ a => f (g a) (h a)) := sorry
 
 set_option trace.Meta.synthInstance true
-set_option trace.Meta.synthInstance.globalInstances false
-set_option trace.Meta.synthInstance.newSubgoal false
-set_option trace.Meta.synthInstance.tryResolve false
-set_option trace.Meta.synthInstance.resume false
-set_option trace.Meta.synthInstance.generate false
-set_option trace.Meta.synthInstance.newAnswer false
 set_option trace.Meta.synthInstance.unusedArgs true
 example (f : β → δ → γ) [IsSmooth f] (d : δ) : IsSmooth (λ (g : α → β) a => f (g a) d) := by infer_instance
diff --git a/tests/lean/815b.lean.expected.out b/tests/lean/815b.lean.expected.out
index 5a41b130b9b1..734c3220da77 100644
--- a/tests/lean/815b.lean.expected.out
+++ b/tests/lean/815b.lean.expected.out
@@ -5,57 +5,171 @@
 815b.lean:9:9-9:13: warning: declaration uses 'sorry'
 815b.lean:10:9-10:13: warning: declaration uses 'sorry'
 815b.lean:11:9-11:13: warning: declaration uses 'sorry'
-[Meta.synthInstance] preprocess: IsSmooth fun g a => f (g a) d ==> IsSmooth fun g a => f (g a) d
-  [Meta.synthInstance] 
-    [Meta.synthInstance] main goal IsSmooth fun g a => f (g a) d
+[Meta.synthInstance] ✅ IsSmooth fun g a => f (g a) d
+  [Meta.synthInstance] new goal IsSmooth fun g a => f (g a) d
+    [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
+  [Meta.synthInstance] ❌ apply inst✝ to IsSmooth fun g a => f (g a) d
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g a => f (g a) d ≟ IsSmooth f
+  [Meta.synthInstance] ✅ apply @swap to IsSmooth fun g a => f (g a) d
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g a => f (g a) d ≟ IsSmooth fun b a => f (b a) d
+    [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a) d
+      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
+  [Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) d
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a) d ≟ IsSmooth f
+  [Meta.synthInstance] ✅ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) d
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
     [Meta.synthInstance.unusedArgs] α → IsSmooth f
-    has unused arguments, reduced type
-      IsSmooth f
-    Transformer
-      fun redf a => redf
+        has unused arguments, reduced type
+          IsSmooth f
+        Transformer
+          fun redf a => redf
+    [Meta.synthInstance] new goal IsSmooth f
+      [Meta.synthInstance.instances] #[inst✝]
+  [Meta.synthInstance] ✅ apply inst✝ to IsSmooth f
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth f ≟ IsSmooth f
+  [Meta.synthInstance.resume] propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
+    [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance.unusedArgs] α → IsSmooth f
-    has unused arguments, reduced type
-      IsSmooth f
-    Transformer
-      fun redf a => redf
+        has unused arguments, reduced type
+          IsSmooth f
+        Transformer
+          fun redf a => redf
+  [Meta.synthInstance.resume] propagating α →
+        IsSmooth f to subgoal α → IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
+    [Meta.synthInstance.resume] size: 2
     [Meta.synthInstance.unusedArgs] α → ∀ (b : β), IsSmooth (f b)
-    has unused arguments, reduced type
-      ∀ (b : β), IsSmooth (f b)
-    Transformer
-      fun redf a b => redf b
+        has unused arguments, reduced type
+          ∀ (b : β), IsSmooth (f b)
+        Transformer
+          fun redf a b => redf b
+    [Meta.synthInstance] new goal ∀ (b : β), IsSmooth (f b)
+      [Meta.synthInstance.instances] #[inst✝]
+  [Meta.synthInstance] ❌ apply inst✝ to ∀ (b : β), IsSmooth (f b)
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth (f b) ≟ IsSmooth f
+  [Meta.synthInstance] ❌ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) d
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
+  [Meta.synthInstance] ✅ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
+    [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a)
+      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
+  [Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a)
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a) ≟ IsSmooth f
+  [Meta.synthInstance] ✅ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a)
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) ≟ IsSmooth fun b a_1 => f (b a) a_1
+    [Meta.synthInstance] new goal ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
+  [Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth f
+  [Meta.synthInstance] ✅ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
     [Meta.synthInstance.unusedArgs] α → δ → IsSmooth f
-    has unused arguments, reduced type
-      IsSmooth f
-    Transformer
-      fun redf a a => redf
+        has unused arguments, reduced type
+          IsSmooth f
+        Transformer
+          fun redf a a => redf
+  [Meta.synthInstance.resume] propagating α →
+        δ → IsSmooth f to subgoal α → δ → IsSmooth f of ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance.unusedArgs] α → δ → ∀ (b : β), IsSmooth (f b)
-    has unused arguments, reduced type
-      ∀ (b : β), IsSmooth (f b)
-    Transformer
-      fun redf a a b => redf b
+        has unused arguments, reduced type
+          ∀ (b : β), IsSmooth (f b)
+        Transformer
+          fun redf a a b => redf b
+  [Meta.synthInstance] ❌ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
+  [Meta.synthInstance] ✅ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
     [Meta.synthInstance.unusedArgs] ∀ (a : α), δ → IsSmooth fun g => f (g a)
-    has unused arguments, reduced type
-      ∀ (a : α), IsSmooth fun g => f (g a)
-    Transformer
-      fun redf a a_1 => redf a
+        has unused arguments, reduced type
+          ∀ (a : α), IsSmooth fun g => f (g a)
+        Transformer
+          fun redf a a_1 => redf a
+  [Meta.synthInstance] ❌ apply @const to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a
+  [Meta.synthInstance] ❌ apply @identity to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a => a
+  [Meta.synthInstance] ❌ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a)
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g =>
+          f (g a) ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
+  [Meta.synthInstance] ✅ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a)
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) ≟ IsSmooth fun a_1 => f (a_1 a)
     [Meta.synthInstance.unusedArgs] α → IsSmooth f
-    has unused arguments, reduced type
-      IsSmooth f
-    Transformer
-      fun redf a => redf
+        has unused arguments, reduced type
+          IsSmooth f
+        Transformer
+          fun redf a => redf
+  [Meta.synthInstance.resume] propagating α →
+        IsSmooth f to subgoal α → IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a)
+    [Meta.synthInstance.resume] size: 1
+    [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => g a
+      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
+  [Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g a ≟ IsSmooth f
+  [Meta.synthInstance] ❌ apply @diag to ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g =>
+          g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
+  [Meta.synthInstance] ❌ apply @comp to ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
+  [Meta.synthInstance] ✅ apply @parm to ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => a_1 a
     [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
-    has unused arguments, reduced type
-      IsSmooth fun g => g
-    Transformer
-      fun redf a => redf
+        has unused arguments, reduced type
+          IsSmooth fun g => g
+        Transformer
+          fun redf a => redf
+    [Meta.synthInstance] new goal IsSmooth fun g => g
+      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
+  [Meta.synthInstance] ❌ apply inst✝ to IsSmooth fun g => g
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth f
+  [Meta.synthInstance] ✅ apply @swap to IsSmooth fun g => g
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g ≟ IsSmooth fun b a => b a
+  [Meta.synthInstance] ❌ apply @diag to IsSmooth fun g => g
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a) (?m a)
+  [Meta.synthInstance] ❌ apply @comp to IsSmooth fun g => g
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a)
+  [Meta.synthInstance] ❌ apply @parm to IsSmooth fun g => g
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m a ?m
+  [Meta.synthInstance] ❌ apply @const to IsSmooth fun g => g
+    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m
+  [Meta.synthInstance] ✅ apply @identity to IsSmooth fun g => g
+    [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g ≟ IsSmooth fun a => a
+  [Meta.synthInstance.resume] propagating IsSmooth fun a =>
+        a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
-    has unused arguments, reduced type
-      IsSmooth fun g => g
-    Transformer
-      fun redf a => redf
+        has unused arguments, reduced type
+          IsSmooth fun g => g
+        Transformer
+          fun redf a => redf
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.resume] size: 2
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of IsSmooth fun g => g
+    [Meta.synthInstance.resume] size: 3
+  [Meta.synthInstance.resume] propagating IsSmooth fun b a =>
+        b a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.resume] size: 4
     [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
-    has unused arguments, reduced type
-      IsSmooth fun g => g
-    Transformer
-      fun redf a => redf
+        has unused arguments, reduced type
+          IsSmooth fun g => g
+        Transformer
+          fun redf a => redf
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth fun b a => b a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.resume] size: 8
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.resume] size: 5
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of ∀ (a : α), IsSmooth fun g => f (g a)
+    [Meta.synthInstance.resume] size: 4
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth fun a_1 =>
+          f (a_1 a) to subgoal ∀ (a : α), IsSmooth fun g => f (g a) of ∀ (a : α), IsSmooth fun g => f (g a) d
+    [Meta.synthInstance.resume] size: 5
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth fun a_1 =>
+          f (a_1 a) d to subgoal ∀ (a : α), IsSmooth fun g => f (g a) d of IsSmooth fun g a => f (g a) d
+    [Meta.synthInstance.resume] size: 6
   [Meta.synthInstance] result swap fun a g => f (g a) d
diff --git a/tests/lean/973b.lean.expected.out b/tests/lean/973b.lean.expected.out
index 4b5ec8419f6d..42e17ddbc12a 100644
--- a/tests/lean/973b.lean.expected.out
+++ b/tests/lean/973b.lean.expected.out
@@ -2,13 +2,12 @@
 973b.lean:9:8-9:11: warning: declaration uses 'sorry'
 [Meta.Tactic.simp.discharge] >> discharge?: ?p x
 [Meta.Tactic.simp.discharge] ex, failed to discharge hypotheses
-  ?p x
+      ?p x
 [Meta.Tactic.simp.discharge] >> discharge?: ?p (f x)
 [Meta.Tactic.simp.discharge] >> discharge?: ?p x
 [Meta.Tactic.simp.discharge] ex, failed to discharge hypotheses
-  ?p x
+      ?p x
 [Meta.Tactic.simp.discharge] >> discharge?: ?p x
 [Meta.Tactic.simp.discharge] ex, failed to discharge hypotheses
-  ?p x
-[Meta.Tactic.simp.discharge] ex, failed to discharge hypotheses
-  ?p (f x)
+      ?p x
+[Meta.Tactic.simp.discharge] ex, failed to discharge hypotheses ?p (f x)
diff --git a/tests/lean/byCasesMetaM.lean.expected.out b/tests/lean/byCasesMetaM.lean.expected.out
index d213534f3bc8..c52971f81142 100644
--- a/tests/lean/byCasesMetaM.lean.expected.out
+++ b/tests/lean/byCasesMetaM.lean.expected.out
@@ -1,14 +1,14 @@
 [Meta.debug] p q : Prop
-h : p ∧ q
-⊢ q ∧ q
+    h : p ∧ q
+    ⊢ q ∧ q
 [Meta.debug] case inl
-p q : Prop
-h : p ∧ q
-hAux : p
-⊢ q ∧ q
-------
-case inr
-p q : Prop
-h : p ∧ q
-hAux : ¬p
-⊢ q ∧ q
+    p q : Prop
+    h : p ∧ q
+    hAux : p
+    ⊢ q ∧ q
+    ------
+    case inr
+    p q : Prop
+    h : p ∧ q
+    hAux : ¬p
+    ⊢ q ∧ q
diff --git a/tests/lean/infoFromFailure.lean.expected.out b/tests/lean/infoFromFailure.lean.expected.out
index c523330fa466..04f965edf389 100644
--- a/tests/lean/infoFromFailure.lean.expected.out
+++ b/tests/lean/infoFromFailure.lean.expected.out
@@ -1,13 +1,7 @@
 B.foo "hello" : String × String
-[Meta.synthInstance] preprocess: Add String ==> Add String
-  [Meta.synthInstance] 
-    [Meta.synthInstance] main goal Add String
-    [Meta.synthInstance.newSubgoal] Add String
-    [Meta.synthInstance.globalInstances] Add String, []
-    [Meta.synthInstance] failed
-[Meta.synthInstance] preprocess: Add Bool ==> Add Bool
-  [Meta.synthInstance] 
-    [Meta.synthInstance] main goal Add Bool
-    [Meta.synthInstance.newSubgoal] Add Bool
-    [Meta.synthInstance.globalInstances] Add Bool, []
-    [Meta.synthInstance] failed
+[Meta.synthInstance] ❌ Add String
+  [Meta.synthInstance] no instances for Add String
+    [Meta.synthInstance.instances] #[]
+[Meta.synthInstance] ❌ Add Bool
+  [Meta.synthInstance] no instances for Add Bool
+    [Meta.synthInstance.instances] #[]
diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out
index e71ca5012e91..b8b2e16bbc12 100644
--- a/tests/lean/ppNotationCode.lean.expected.out
+++ b/tests/lean/ppNotationCode.lean.expected.out
@@ -1,85 +1,85 @@
 [Elab.definition.body] «term_+++_» : Lean.TrailingParserDescr :=
-Lean.ParserDescr.trailingNode `«term_+++_» 45 46
-  (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46))
+    Lean.ParserDescr.trailingNode `«term_+++_» 45 46
+      (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46))
 [Elab.definition.body] «_aux_ppNotationCode___macroRules_term_+++__1» : Lean.Macro :=
-fun x =>
-  let discr := x;
-  if Lean.Syntax.isOfKind discr `«term_+++_» = true then
-    let discr_1 := Lean.Syntax.getArg discr 0;
-    let discr_2 := Lean.Syntax.getArg discr 1;
-    let discr := Lean.Syntax.getArg discr 2;
-    let rhs := { raw := discr };
-    let lhs := { raw := discr_1 };
-    do
-    let info ← Lean.MonadRef.mkInfoFromRefPos
-    let scp ← Lean.getCurrMacroScope
-    let mainModule ← Lean.getMainModule
-    pure
-        { raw :=
-              Lean.Syntax.node info `Lean.Parser.Term.app
-                #[Lean.Syntax.ident info (String.toSubstring "Nat.add") (Lean.addMacroScope mainModule `Nat.add scp)
-                    [(`Nat.add, [])],
-                  Lean.Syntax.node info `null #[lhs.raw, rhs.raw]] }.raw
-  else
-    let discr := x;
-    throw Lean.Macro.Exception.unsupportedSyntax
-[Elab.definition.body] _aux_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander :=
-fun x =>
-  let discr := x;
-  if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then
-    let discr_1 := Lean.Syntax.getArg discr 0;
-    bif false || Lean.Syntax.isOfKind discr_1 `ident then
-      let discr_2 := Lean.Syntax.getArg discr 1;
-      if Lean.Syntax.matchesNull discr_2 2 = true then
-        let discr := Lean.Syntax.getArg discr_2 0;
-        let discr_3 := Lean.Syntax.getArg discr_2 1;
-        let rhs := { raw := discr_3 };
-        let lhs := { raw := discr };
-        let f := { raw := discr_1 };
-        Lean.withRef f.raw do
-          let info ← Lean.MonadRef.mkInfoFromRefPos
-          let _ ← Lean.getCurrMacroScope
-          let _ ← Lean.getMainModule
-          pure { raw := Lean.Syntax.node info `«term_+++_» #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw] }.raw
+    fun x =>
+      let discr := x;
+      if Lean.Syntax.isOfKind discr `«term_+++_» = true then
+        let discr_1 := Lean.Syntax.getArg discr 0;
+        let discr_2 := Lean.Syntax.getArg discr 1;
+        let discr := Lean.Syntax.getArg discr 2;
+        let rhs := { raw := discr };
+        let lhs := { raw := discr_1 };
+        do
+        let info ← Lean.MonadRef.mkInfoFromRefPos
+        let scp ← Lean.getCurrMacroScope
+        let mainModule ← Lean.getMainModule
+        pure
+            { raw :=
+                  Lean.Syntax.node info `Lean.Parser.Term.app
+                    #[Lean.Syntax.ident info (String.toSubstring "Nat.add") (Lean.addMacroScope mainModule `Nat.add scp)
+                        [(`Nat.add, [])],
+                      Lean.Syntax.node info `null #[lhs.raw, rhs.raw]] }.raw
       else
-        let discr := Lean.Syntax.getArg discr 1;
-        throw ()
-    else
-      let discr_2 := Lean.Syntax.getArg discr 0;
-      if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.app = true then
-        let discr_3 := Lean.Syntax.getArg discr_2 0;
-        bif false || Lean.Syntax.isOfKind discr_3 `ident then
-          let discr_4 := Lean.Syntax.getArg discr_2 1;
-          if Lean.Syntax.matchesNull discr_4 2 = true then
-            let discr_5 := Lean.Syntax.getArg discr_4 0;
-            let discr_6 := Lean.Syntax.getArg discr_4 1;
-            let discr := Lean.Syntax.getArg discr 1;
-            let moreArgs := Lean.TSyntaxArray.mk (Lean.Syntax.getArgs discr);
-            let rhs := { raw := discr_6 };
-            let lhs := { raw := discr_5 };
-            let f := { raw := discr_3 };
+        let discr := x;
+        throw Lean.Macro.Exception.unsupportedSyntax
+[Elab.definition.body] _aux_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander :=
+    fun x =>
+      let discr := x;
+      if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then
+        let discr_1 := Lean.Syntax.getArg discr 0;
+        bif false || Lean.Syntax.isOfKind discr_1 `ident then
+          let discr_2 := Lean.Syntax.getArg discr 1;
+          if Lean.Syntax.matchesNull discr_2 2 = true then
+            let discr := Lean.Syntax.getArg discr_2 0;
+            let discr_3 := Lean.Syntax.getArg discr_2 1;
+            let rhs := { raw := discr_3 };
+            let lhs := { raw := discr };
+            let f := { raw := discr_1 };
             Lean.withRef f.raw do
               let info ← Lean.MonadRef.mkInfoFromRefPos
               let _ ← Lean.getCurrMacroScope
               let _ ← Lean.getMainModule
-              pure
-                  { raw :=
-                        Lean.Syntax.node info `Lean.Parser.Term.app
-                          #[Lean.Syntax.node info `«term_+++_» #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw],
-                            Lean.Syntax.node info `null (Array.append #[] (Lean.TSyntaxArray.raw moreArgs))] }.raw
+              pure { raw := Lean.Syntax.node info `«term_+++_» #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw] }.raw
           else
-            let discr_5 := Lean.Syntax.getArg discr_2 1;
             let discr := Lean.Syntax.getArg discr 1;
             throw ()
         else
-          let discr_4 := Lean.Syntax.getArg discr_2 0;
-          let discr_5 := Lean.Syntax.getArg discr_2 1;
-          let discr := Lean.Syntax.getArg discr 1;
-          throw ()
+          let discr_2 := Lean.Syntax.getArg discr 0;
+          if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.app = true then
+            let discr_3 := Lean.Syntax.getArg discr_2 0;
+            bif false || Lean.Syntax.isOfKind discr_3 `ident then
+              let discr_4 := Lean.Syntax.getArg discr_2 1;
+              if Lean.Syntax.matchesNull discr_4 2 = true then
+                let discr_5 := Lean.Syntax.getArg discr_4 0;
+                let discr_6 := Lean.Syntax.getArg discr_4 1;
+                let discr := Lean.Syntax.getArg discr 1;
+                let moreArgs := Lean.TSyntaxArray.mk (Lean.Syntax.getArgs discr);
+                let rhs := { raw := discr_6 };
+                let lhs := { raw := discr_5 };
+                let f := { raw := discr_3 };
+                Lean.withRef f.raw do
+                  let info ← Lean.MonadRef.mkInfoFromRefPos
+                  let _ ← Lean.getCurrMacroScope
+                  let _ ← Lean.getMainModule
+                  pure
+                      { raw :=
+                            Lean.Syntax.node info `Lean.Parser.Term.app
+                              #[Lean.Syntax.node info `«term_+++_» #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw],
+                                Lean.Syntax.node info `null (Array.append #[] (Lean.TSyntaxArray.raw moreArgs))] }.raw
+              else
+                let discr_5 := Lean.Syntax.getArg discr_2 1;
+                let discr := Lean.Syntax.getArg discr 1;
+                throw ()
+            else
+              let discr_4 := Lean.Syntax.getArg discr_2 0;
+              let discr_5 := Lean.Syntax.getArg discr_2 1;
+              let discr := Lean.Syntax.getArg discr 1;
+              throw ()
+          else
+            let discr_3 := Lean.Syntax.getArg discr 0;
+            let discr := Lean.Syntax.getArg discr 1;
+            throw ()
       else
-        let discr_3 := Lean.Syntax.getArg discr 0;
-        let discr := Lean.Syntax.getArg discr 1;
+        let discr := x;
         throw ()
-  else
-    let discr := x;
-    throw ()
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 580c151431b3..1aca9eba005a 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -369,7 +369,7 @@ pure ()
 #eval tst26
 
 section
-set_option trace.Meta.isDefEq.step true
+set_option trace.Meta.isDefEq true
 set_option trace.Meta.isDefEq.delta true
 set_option trace.Meta.isDefEq.assign true
 
@@ -572,7 +572,7 @@ checkM $ getAssignment m2 >>= fun v => pure $ v == nat;
 pure ()
 
 set_option pp.all true
-set_option trace.Meta.isDefEq.step true
+set_option trace.Meta.isDefEq true
 set_option trace.Meta.isDefEq.delta true
 set_option trace.Meta.isDefEq.assign true
 
@@ -658,7 +658,7 @@ check w;
 print w;
 pure ()
 
-set_option trace.Meta.isDefEq.step false
+set_option trace.Meta.isDefEq false
 set_option trace.Meta.isDefEq.delta false
 set_option trace.Meta.isDefEq.assign false
 #eval tst41
diff --git a/tests/lean/run/termElab.lean b/tests/lean/run/termElab.lean
index 7ad3f8e72e92..d41055556f2c 100644
--- a/tests/lean/run/termElab.lean
+++ b/tests/lean/run/termElab.lean
@@ -10,7 +10,7 @@ let opt ← getOptions;
 let stx ← `(forall (a b : Nat), Nat);
 IO.println "message 1"; -- This message goes direct to stdio. It will be displayed before trace messages.
 let e ← elabTermAndSynthesize stx none;
-logDbgTrace m!">>> {e}"; -- display message when `trace.Elab.debug` is true
+trace[Elab.debug] m!">>> {e}"; -- display message when `trace.Elab.debug` is true
 IO.println "message 2"
 
 #eval tst1
@@ -21,7 +21,7 @@ let a := mkIdent `a;
 let b := mkIdent `b;
 let stx ← `((fun ($a : Type) (x : $a) => @id $a x) _ 1);
 let e ← elabTermAndSynthesize stx none;
-logDbgTrace m!">>> {e}";
+trace[Elab.debug] m!">>> {e}";
 throwErrorIfErrors
 
 #eval tst2
diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean
index e9fca4687131..16c1701797e6 100644
--- a/tests/lean/run/trace.lean
+++ b/tests/lean/run/trace.lean
@@ -14,7 +14,7 @@ do trace[module] (m!"hello" ++ MessageData.nest 9 (m!"\n" ++ "world"));
    pure ()
 
 def tst2 (b : Bool) : M Unit :=
-traceCtx `module $ do
+withTraceNode `module (fun _ => return "message") do
   tst1;
   trace[bughunt] "at test2";
   if b then throwError "error";
@@ -30,7 +30,7 @@ def slow (b : Bool) : Nat :=
 ack 4 (cond b 0 1)
 
 def tst3 (b : Bool) : M Unit :=
-do traceCtx `module $ do {
+do withTraceNode `module.slow (fun _ => return m!"slow: {slow b}") do {
      tst2 b;
      tst1
    };
@@ -39,7 +39,7 @@ do traceCtx `module $ do {
    -- if `trace.slow is active.
    trace[slow] (m!"slow message: " ++ toString (slow b))
    -- This is true even if it is a monad computation:
-   trace[slow] (m!"slow message: " ++ (toString (slow b)))
+   trace[slow] (m!"slow message: " ++ (← pure (toString (slow b))))
 
 def run (x : M Unit) : M Unit :=
 withReader
diff --git a/tests/lean/sanitizeMacroScopes.lean.expected.out b/tests/lean/sanitizeMacroScopes.lean.expected.out
index 878f678fd20b..fb7ec6f25be8 100644
--- a/tests/lean/sanitizeMacroScopes.lean.expected.out
+++ b/tests/lean/sanitizeMacroScopes.lean.expected.out
@@ -1,13 +1,19 @@
 fun x x_1 => x : (x : ?m) → ?m x → ?m
 [Elab.step] expected type: <not-available>, term
-fun x => m x
-[Elab.step] expected type: Sort ?u, term
-  _
-  [Elab.step] expected type: <not-available>, term
-  m x
-  [Elab.step] expected type: <not-available>, term
-    fun x✝ => x
-    [Elab.step] expected type: Sort ?u, term
+    fun x => m x
+  [Elab.step] expected type: Sort ?u, term
       _
+    [Elab.step.result] ?m
+  [Elab.step] expected type: <not-available>, term
+      m x
+    [Elab.step] expected type: <not-available>, term
+        fun x✝ => x
+      [Elab.step] expected type: Sort ?u, term
+          _
+        [Elab.step.result] ?m
       [Elab.step] expected type: <not-available>, term
-      x
+          x
+        [Elab.step.result] x
+      [Elab.step.result] fun x_1 => x
+    [Elab.step.result] fun x_1 => x
+  [Elab.step.result] fun x x_1 => x
diff --git a/tests/lean/simpDisch.lean.expected.out b/tests/lean/simpDisch.lean.expected.out
index e7b4bfc6e4d0..c6e58fe6a058 100644
--- a/tests/lean/simpDisch.lean.expected.out
+++ b/tests/lean/simpDisch.lean.expected.out
@@ -8,12 +8,7 @@ h1 : x ≠ 0
 h2 : y ≠ 0
 h3 : x = y
 ⊢ x ≠ 0
-case simp.discharger
-x y : Nat
-h1 : x ≠ 0
-h2 : y ≠ 0
-h3 : x = y
-⊢ y ≠ 0
+case simp.discharger x y : Nat h1 : x ≠ 0 h2 : y ≠ 0 h3 : x = y ⊢ y ≠ 0
 x y : Nat
 h1 : x ≠ 0
 h2 : y ≠ 0
diff --git a/tests/lean/smartUnfoldingMatch.lean.expected.out b/tests/lean/smartUnfoldingMatch.lean.expected.out
index 84b4c40133ca..3d995b176e3e 100644
--- a/tests/lean/smartUnfoldingMatch.lean.expected.out
+++ b/tests/lean/smartUnfoldingMatch.lean.expected.out
@@ -1,4 +1,4 @@
 42
 [Meta.debug] r: match x, 0 with
-  | some x, x_1 => x
-  | none, e => e
+    | some x, x_1 => x
+    | none, e => e
diff --git a/tests/lean/syntaxInNamespacesAndPP.lean.expected.out b/tests/lean/syntaxInNamespacesAndPP.lean.expected.out
index a42eda11a450..47aa41c14115 100644
--- a/tests/lean/syntaxInNamespacesAndPP.lean.expected.out
+++ b/tests/lean/syntaxInNamespacesAndPP.lean.expected.out
@@ -1,27 +1,5 @@
-[Elab.command] #check foo true
 true : Bool
-[Elab.step] expected type: <not-available>, term
-foo true
-[Elab.step] expected type: <not-available>, term
-  true
-  [Elab.app.args] explicit: false, ellipsis: false, true : Bool
-    [Elab.app.args] namedArgs: []
-    [Elab.app.args] args: []
-    [Elab.app.finalize] true
-    [Elab.app.finalize] after etaArgs, true : Bool
-[Elab.command] end
-[Elab.command] #check bla true
 true : Bool
-[Elab.step] expected type: <not-available>, term
-bla true
-[Elab.step] expected type: <not-available>, term
-  true
-  [Elab.app.args] explicit: false, ellipsis: false, true : Bool
-    [Elab.app.args] namedArgs: []
-    [Elab.app.args] args: []
-    [Elab.app.finalize] true
-    [Elab.app.finalize] after etaArgs, true : Bool
-[Elab.command] end
 def Bla.bla : Lean.ParserDescr :=
 Lean.ParserDescr.node `Bla.bla 1022
   (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "bla") (Lean.ParserDescr.cat `term 0))
diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out
index 3d1ad2db0e7e..c1626128b656 100644
--- a/tests/lean/syntaxPrec.lean.expected.out
+++ b/tests/lean/syntaxPrec.lean.expected.out
@@ -1,9 +1,9 @@
 syntaxPrec.lean:1:18: error: expected ':'
 [Elab.command] syntax "foo"("*" <|> term,+) : term
 [Elab.command] @[termParser 1000]
-def «termFoo*_» : Lean.ParserDescr✝ :=
-  ParserDescr.node✝ `«termFoo*_» 1022
-    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo")
-      (ParserDescr.binary✝ `orelse (ParserDescr.symbol✝ "*")
-        ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
-          Bool.false✝)))
+    def «termFoo*_» : Lean.ParserDescr✝ :=
+      ParserDescr.node✝ `«termFoo*_» 1022
+        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo")
+          (ParserDescr.binary✝ `orelse (ParserDescr.symbol✝ "*")
+            ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) ","
+              (ParserDescr.symbol✝ ", ") Bool.false✝)))
diff --git a/tests/lean/traceTacticSteps.lean.expected.out b/tests/lean/traceTacticSteps.lean.expected.out
index 0d4e1091e685..3182ab4751d0 100644
--- a/tests/lean/traceTacticSteps.lean.expected.out
+++ b/tests/lean/traceTacticSteps.lean.expected.out
@@ -1,32 +1,34 @@
-[Elab.step] expected type: Sort ?u, term
-True
+[Elab.step] expected type: Prop, term
+    True
+  [Elab.step.result] True
 [Elab.step] expected type: True, term
-by
-  skip
-  trivial
+    by
+      skip
+      trivial
+  [Elab.step.result] ?m
+[Elab.step] skip
 [Elab.step] 
-  skip
-  trivial
+      skip
+      trivial
 [Elab.step] 
-  skip
-  trivial
-[Elab.step] skip
+      skip
+      trivial
 [Elab.step] trivial
 [Elab.step] (apply And.intro✝) <;> trivial
 [Elab.step] focus
-  apply And.intro✝
-  with_annotate_state"<;>" skip
-  all_goals
-    trivial
+      apply And.intro✝
+      with_annotate_state"<;>" skip
+      all_goals
+        trivial
 [Elab.step] 
-  apply And.intro✝
-  with_annotate_state"<;>" skip
-  all_goals
-    trivial
+      apply And.intro✝
+      with_annotate_state"<;>" skip
+      all_goals
+        trivial
 [Elab.step] 
-  apply And.intro✝
-  with_annotate_state"<;>" skip
-  all_goals
-    trivial
+      apply And.intro✝
+      with_annotate_state"<;>" skip
+      all_goals
+        trivial
 [Elab.step] apply And.intro✝
 [Elab.step] apply True.intro✝