diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean
index 962c27e078cf..39db7e40fe3c 100644
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@@ -37,7 +37,7 @@ def elabGrindPattern : CommandElab := fun stx => do
 def grind (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
   let goals ← Grind.main mvarId config mainDeclName fallback
   unless goals.isEmpty do
-    throwError "`grind` failed\n{← Grind.goalsToMessageData goals}"
+    throwError "`grind` failed\n{← Grind.goalsToMessageData goals config}"
 
 private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit) := do
   let some fallback := fallback? | return (pure ())
diff --git a/src/Lean/Meta/Tactic/Grind/Ctor.lean b/src/Lean/Meta/Tactic/Grind/Ctor.lean
index 754fe27ad996..53c6922de653 100644
--- a/src/Lean/Meta/Tactic/Grind/Ctor.lean
+++ b/src/Lean/Meta/Tactic/Grind/Ctor.lean
@@ -20,7 +20,7 @@ private partial def propagateInjEqs (eqs : Expr) (proof : Expr) : GoalM Unit :=
   | HEq _ lhs _ rhs =>
     pushHEq (← shareCommon lhs) (← shareCommon rhs) proof
   | _ =>
-   trace_goal[grind.issues] "unexpected injectivity theorem result type{indentExpr eqs}"
+   reportIssue m!"unexpected injectivity theorem result type{indentExpr eqs}"
    return ()
 
 /--
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index b432cf074c0e..007ed1ac7d7f 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -250,7 +250,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   assert! c.assignment.size == numParams
   let (mvars, bis, _) ← forallMetaBoundedTelescope (← inferType proof) numParams
   if mvars.size != thm.numParams then
-    trace_goal[grind.issues] "unexpected number of parameters at {← thm.origin.pp}"
+    reportIssue m!"unexpected number of parameters at {← thm.origin.pp}"
     return ()
   -- Apply assignment
   for h : i in [:mvars.size] do
@@ -260,14 +260,14 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
       let mvarIdType ← mvarId.getType
       let vType ← inferType v
       unless (← isDefEq mvarIdType vType <&&> mvarId.checkedAssign v) do
-        trace_goal[grind.issues] "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
+        reportIssue m!"type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
         return ()
   -- Synthesize instances
   for mvar in mvars, bi in bis do
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
       unless (← synthesizeInstance mvar type) do
-        trace_goal[grind.issues] "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
+        reportIssue m!"failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
         return ()
   let proof := mkAppN proof mvars
   if (← mvars.allM (·.mvarId!.isAssigned)) then
@@ -275,7 +275,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   else
     let mvars ← mvars.filterM fun mvar => return !(← mvar.mvarId!.isAssigned)
     if let some mvarBad ← mvars.findM? fun mvar => return !(← isProof mvar) then
-      trace_goal[grind.issues] "failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
+      reportIssue m!"failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
     let proof ← mkLambdaFVars (binderInfoForMVars := .default) mvars (← instantiateMVars proof)
     addNewInstance thm.origin proof c.gen
 where
diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
index dbf0f234cbd7..e1620b5806af 100644
--- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean
+++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
@@ -77,7 +77,7 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
     if let some thm ← mkEMatchTheoremWithKind'? origin proof .default then
       activateTheorem thm gen
   if (← get).newThms.size == size then
-    trace[grind.issues] "failed to create E-match local theorem for{indentExpr e}"
+    reportIssue m!"failed to create E-match local theorem for{indentExpr e}"
 
 def propagateForallPropDown (e : Expr) : GoalM Unit := do
   let .forallE n a b bi := e | return ()
diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index 6f1c0b2530c2..a0d68ab2d440 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -24,7 +24,7 @@ def addCongrTable (e : Expr) : GoalM Unit := do
     let g := e'.getAppFn
     unless isSameExpr f g do
       unless (← hasSameType f g) do
-        trace_goal[grind.issues] "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
+        reportIssue m!"found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
         return ()
     trace_goal[grind.debug.congr] "{e} = {e'}"
     pushEqHEq e e' congrPlaceholderProof
@@ -168,7 +168,7 @@ partial def internalize (e : Expr) (generation : Nat) (parent? : Option Expr :=
   | .mvar ..
   | .mdata ..
   | .proj .. =>
-    trace_goal[grind.issues] "unexpected term during internalization{indentExpr e}"
+    reportIssue m!"unexpected kernel projection term during internalization{indentExpr e}\n`grind` uses a pre-processing step that folds them as projection applications, the pre-processor should have failed to fold this term"
     mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
   | .app .. =>
     if (← isLitValue e) then
diff --git a/src/Lean/Meta/Tactic/Grind/PP.lean b/src/Lean/Meta/Tactic/Grind/PP.lean
index 549cd91342e7..db7766c8468c 100644
--- a/src/Lean/Meta/Tactic/Grind/PP.lean
+++ b/src/Lean/Meta/Tactic/Grind/PP.lean
@@ -76,10 +76,16 @@ private def ppExprArray (cls : Name) (header : String) (es : Array Expr) (clsEle
   let es := es.map fun e => .trace { cls := clsElem} m!"{e}" #[]
   .trace { cls } header es
 
-private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
+private abbrev M := ReaderT Goal (StateT (Array MessageData) MetaM)
+
+private def pushMsg (m : MessageData) : M Unit :=
+  modify fun s => s.push m
+
+private def ppEqcs : M Unit := do
    let mut trueEqc?  : Option MessageData := none
    let mut falseEqc? : Option MessageData := none
    let mut otherEqcs : Array MessageData := #[]
+   let goal ← read
    for eqc in goal.getEqcs do
      if Option.isSome <| eqc.find? (·.isTrue) then
        let eqc := eqc.filter fun e => !e.isTrue
@@ -93,44 +99,68 @@ private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
        -- We may want to add a flag to pretty print equivalence classes of nested proofs
        unless (← isProof e) do
          otherEqcs := otherEqcs.push <| .trace { cls := `eqc } (.group ("{" ++ (MessageData.joinSep (eqc.map toMessageData) ("," ++ Format.line)) ++  "}")) #[]
-   let mut result := #[]
-   if let some trueEqc := trueEqc? then result := result.push trueEqc
-   if let some falseEqc := falseEqc? then result := result.push falseEqc
+   if let some trueEqc := trueEqc? then pushMsg trueEqc
+   if let some falseEqc := falseEqc? then pushMsg falseEqc
    unless otherEqcs.isEmpty do
-     result := result.push <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
-   return result
+     pushMsg <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
 
 private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
   let m := m!"{← thm.origin.pp}:\n{← inferType thm.proof}\npatterns: {thm.patterns.map ppPattern}"
   return .trace { cls := `thm } m #[]
 
-private def ppActiveTheorems (goal : Goal) : MetaM MessageData := do
-  let m ← goal.thms.toArray.mapM ppEMatchTheorem
-  let m := m ++ (← goal.newThms.toArray.mapM ppEMatchTheorem)
-  if m.isEmpty then
-    return ""
-  else
-    return .trace { cls := `ematch } "E-matching" m
+private def ppActiveTheorems : M Unit := do
+  let goal ← read
+  let m ← goal.thms.toArray.mapM fun thm => ppEMatchTheorem thm
+  let m := m ++ (← goal.newThms.toArray.mapM fun thm => ppEMatchTheorem thm)
+  unless m.isEmpty do
+    pushMsg <| .trace { cls := `ematch } "E-matching" m
 
-def ppOffset (goal : Goal) : MetaM MessageData := do
+private def ppOffset : M Unit := do
+  let goal ← read
   let s := goal.arith.offset
   let nodes := s.nodes
-  if nodes.isEmpty then return ""
+  if nodes.isEmpty then return ()
   let model ← Arith.Offset.mkModel goal
   let mut ms := #[]
   for (e, val) in model do
     ms := ms.push <| .trace { cls := `assign } m!"{e} := {val}" #[]
-  return .trace { cls := `offset } "Assignment satisfying offset contraints" ms
-
-def goalToMessageData (goal : Goal) : MetaM MessageData := goal.mvarId.withContext do
-  let mut m : Array MessageData := #[.ofGoal goal.mvarId]
-  m := m.push <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
-  m := m ++ (← ppEqcs goal)
-  m := m.push (← ppActiveTheorems goal)
-  m := m.push (← ppOffset goal)
-  addMessageContextFull <| MessageData.joinSep m.toList ""
-
-def goalsToMessageData (goals : List Goal) : MetaM MessageData :=
-  return MessageData.joinSep (← goals.mapM goalToMessageData) m!"\n"
+  pushMsg <| .trace { cls := `offset } "Assignment satisfying offset contraints" ms
+
+private def ppIssues : M Unit := do
+  let issues := (← read).issues
+  unless issues.isEmpty do
+    pushMsg <| .trace { cls := `issues } "Issues" issues.reverse.toArray
+
+private def ppThresholds (c : Grind.Config) : M Unit := do
+  let goal ← read
+  let maxGen := goal.enodes.foldl (init := 0) fun g _ n => Nat.max g n.generation
+  let mut msgs := #[]
+  if goal.numInstances ≥ c.instances  then
+    msgs := msgs.push <| .trace { cls := `limit } m!"maximum number of instances generated by E-matching has been reached, threshold: `(instances := {c.instances})`" #[]
+  if goal.numEmatch ≥ c.ematch  then
+    msgs := msgs.push <| .trace { cls := `limit } m!"maximum number of E-matching rounds has been reached, threshold: `(ematch := {c.ematch})`" #[]
+  if goal.numSplits ≥ c.splits then
+    msgs := msgs.push <| .trace { cls := `limit } m!"maximum number of case-splits has been reached, threshold: `(splits := {c.splits})`" #[]
+  if maxGen ≥ c.gen then
+    msgs := msgs.push <| .trace { cls := `limit } m!"maximum term generation has been reached, threshold: `(gen := {c.gen})`" #[]
+  unless msgs.isEmpty do
+    pushMsg <| .trace { cls := `limits } "Thresholds reached" msgs
+
+def goalToMessageData (goal : Goal) (config : Grind.Config) : MetaM MessageData := goal.mvarId.withContext do
+  let (_, m) ← go goal |>.run #[]
+  let gm := MessageData.trace { cls := `grind, collapsed := false } "Diagnostics" m
+  let r := m!"{.ofGoal goal.mvarId}\n{gm}"
+  addMessageContextFull r
+where
+  go : M Unit := do
+    pushMsg <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
+    ppEqcs
+    ppActiveTheorems
+    ppOffset
+    ppThresholds config
+    ppIssues
+
+def goalsToMessageData (goals : List Goal) (config : Grind.Config) : MetaM MessageData :=
+  return MessageData.joinSep (← goals.mapM (goalToMessageData · config)) m!"\n"
 
 end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 090e3aad2088..37c739c9e385 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -384,6 +384,11 @@ structure Goal where
   nextThmIdx : Nat := 0
   /-- Asserted facts -/
   facts      : PArray Expr := {}
+  /--
+  Issues found during the proof search in this goal. This issues are reported to
+  users when `grind` fails.
+  -/
+  issues     : List MessageData := []
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -411,6 +416,15 @@ def updateLastTag : GoalM Unit := do
       trace[grind] "working on goal `{currTag}`"
       modifyThe Grind.State fun s => { s with lastTag := currTag }
 
+def reportIssue (msg : MessageData) : GoalM Unit := do
+  let msg ← addMessageContext msg
+  modify fun s => { s with issues := .trace { cls := `issue } msg #[] :: s.issues }
+  /-
+  We also add a trace message because we may want to know when
+  an issue happened relative to other trace messages.
+  -/
+  trace[grind.issues] msg
+
 /--
 Macro similar to `trace[...]`, but it includes the trace message `trace[grind] "working on <current goal>"`
 if the tag has changed since the last trace message.
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index 6c19b483f56e..1d2de01f7ef5 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -13,23 +13,27 @@ left : p
 right : q
 h✝ : b = false
 h : c = true
-⊢ False[facts] Asserted facts
-  [prop] a = true
-  [prop] b = true ∨ c = true
-  [prop] p
-  [prop] q
-  [prop] b = false ∨ a = false
-  [prop] b = false
-  [prop] c = true[eqc] True propositions
-  [prop] b = true ∨ c = true
-  [prop] p
-  [prop] q
-  [prop] b = false ∨ a = false
-  [prop] b = false
-  [prop] c = true[eqc] Equivalence classes
-  [eqc] {b = true, a = false}
-  [eqc] {b, false}
-  [eqc] {a, c, true}
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] a = true
+    [prop] b = true ∨ c = true
+    [prop] p
+    [prop] q
+    [prop] b = false ∨ a = false
+    [prop] b = false
+    [prop] c = true
+  [eqc] True propositions
+    [prop] b = true ∨ c = true
+    [prop] p
+    [prop] q
+    [prop] b = false ∨ a = false
+    [prop] b = false
+    [prop] c = true
+  [eqc] Equivalence classes
+    [eqc] {b = true, a = false}
+    [eqc] {b, false}
+    [eqc] {a, c, true}
 -/
 #guard_msgs (error) in
 theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
@@ -46,16 +50,20 @@ h✝ : c = true
 left : p
 right : q
 h : b = false
-⊢ False[facts] Asserted facts
-  [prop] a = true
-  [prop] c = true
-  [prop] p
-  [prop] q
-  [prop] b = false[eqc] True propositions
-  [prop] p
-  [prop] q[eqc] Equivalence classes
-  [eqc] {b, false}
-  [eqc] {a, c, true}
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] a = true
+    [prop] c = true
+    [prop] p
+    [prop] q
+    [prop] b = false
+  [eqc] True propositions
+    [prop] p
+    [prop] q
+  [eqc] Equivalence classes
+    [eqc] {b, false}
+    [eqc] {a, c, true}
 -/
 #guard_msgs (error) in
 theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
@@ -70,14 +78,19 @@ i j : Nat
 h : j + 1 < i + 1
 h✝ : j + 1 ≤ i
 x✝ : ¬g (i + 1) j ⋯ = i + j + 1
-⊢ False[facts] Asserted facts
-  [prop] j + 1 ≤ i
-  [prop] ¬g (i + 1) j ⋯ = i + j + 1[eqc] True propositions
-  [prop] j + 1 ≤ i[eqc] False propositions
-  [prop] g (i + 1) j ⋯ = i + j + 1[offset] Assignment satisfying offset contraints
-  [assign] j := 0
-  [assign] i := 1
-  [assign] i + j := 1
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] j + 1 ≤ i
+    [prop] ¬g (i + 1) j ⋯ = i + j + 1
+  [eqc] True propositions
+    [prop] j + 1 ≤ i
+  [eqc] False propositions
+    [prop] g (i + 1) j ⋯ = i + j + 1
+  [offset] Assignment satisfying offset contraints
+    [assign] j := 0
+    [assign] i := 1
+    [assign] i + j := 1
 -/
 #guard_msgs (error) in
 example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by
@@ -102,15 +115,18 @@ head_eq : a₁ = b₁
 x_eq : a₂ = b₂
 y_eq : a₃ = b₃
 tail_eq : as = bs
-⊢ False[facts] Asserted facts
-  [prop] a₁ = b₁
-  [prop] a₂ = b₂
-  [prop] a₃ = b₃
-  [prop] as = bs[eqc] Equivalence classes
-  [eqc] {as, bs}
-  [eqc] {a₃, b₃}
-  [eqc] {a₂, b₂}
-  [eqc] {a₁, b₁}
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] a₁ = b₁
+    [prop] a₂ = b₂
+    [prop] a₃ = b₃
+    [prop] as = bs
+  [eqc] Equivalence classes
+    [eqc] {as, bs}
+    [eqc] {a₃, b₃}
+    [eqc] {a₂, b₂}
+    [eqc] {a₁, b₁}
 -/
 #guard_msgs (error) in
 theorem ex3 (h : a₁ :: { x := a₂, y := a₃ : Point } :: as = b₁ :: { x := b₂, y := b₃} :: bs) : False := by
@@ -133,22 +149,26 @@ h₂ : HEq q a
 h₃ : p = r
 left : ¬p ∨ r
 h : ¬r
-⊢ False[facts] Asserted facts
-  [prop] HEq p a
-  [prop] HEq q a
-  [prop] p = r
-  [prop] ¬p ∨ r
-  [prop] ¬r ∨ p
-  [prop] ¬r[eqc] True propositions
-  [prop] p = r
-  [prop] ¬p ∨ r
-  [prop] ¬r ∨ p
-  [prop] ¬p
-  [prop] ¬r[eqc] False propositions
-  [prop] a
-  [prop] p
-  [prop] q
-  [prop] r
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] HEq p a
+    [prop] HEq q a
+    [prop] p = r
+    [prop] ¬p ∨ r
+    [prop] ¬r ∨ p
+    [prop] ¬r
+  [eqc] True propositions
+    [prop] p = r
+    [prop] ¬p ∨ r
+    [prop] ¬r ∨ p
+    [prop] ¬p
+    [prop] ¬r
+  [eqc] False propositions
+    [prop] a
+    [prop] p
+    [prop] q
+    [prop] r
 case grind.2
 α : Type
 a : α
@@ -158,22 +178,26 @@ h₂ : HEq q a
 h₃ : p = r
 left : ¬p ∨ r
 h : p
-⊢ False[facts] Asserted facts
-  [prop] HEq p a
-  [prop] HEq q a
-  [prop] p = r
-  [prop] ¬p ∨ r
-  [prop] ¬r ∨ p
-  [prop] p[eqc] True propositions
-  [prop] p = r
-  [prop] ¬p ∨ r
-  [prop] ¬r ∨ p
-  [prop] a
-  [prop] p
-  [prop] q
-  [prop] r[eqc] False propositions
-  [prop] ¬p
-  [prop] ¬r
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] HEq p a
+    [prop] HEq q a
+    [prop] p = r
+    [prop] ¬p ∨ r
+    [prop] ¬r ∨ p
+    [prop] p
+  [eqc] True propositions
+    [prop] p = r
+    [prop] ¬p ∨ r
+    [prop] ¬r ∨ p
+    [prop] a
+    [prop] p
+    [prop] q
+    [prop] r
+  [eqc] False propositions
+    [prop] ¬p
+    [prop] ¬r
 -/
 #guard_msgs (error) in
 example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by
@@ -200,3 +224,31 @@ set_option trace.grind.debug.proof false in
 example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by
   fail_if_success grind
   sorry
+
+/--
+error: `grind` failed
+case grind
+f : Nat → Bool
+g : Int → Bool
+a : Nat
+b : Int
+a✝¹ : HEq f g
+a✝ : HEq a b
+x✝ : ¬f a = g b
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] HEq f g
+    [prop] HEq a b
+    [prop] ¬f a = g b
+  [eqc] False propositions
+    [prop] f a = g b
+  [eqc] Equivalence classes
+    [eqc] {a, b}
+    [eqc] {f, g}
+  [issues] Issues
+    [issue] found congruence between g b and f a but functions have different types
+-/
+#guard_msgs (error) in
+example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by
+  grind
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index e138b663d328..dd7d5094eea0 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -244,12 +244,15 @@ case grind
 p q : Prop
 a✝¹ : p = q
 a✝ : p
-⊢ False[facts] Asserted facts
-  [prop] p = q
-  [prop] p[eqc] True propositions
-  [prop] p = q
-  [prop] q
-  [prop] p
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] p = q
+    [prop] p
+  [eqc] True propositions
+    [prop] p = q
+    [prop] q
+    [prop] p
 -/
 #guard_msgs (error) in
 set_option trace.grind.split true in
@@ -262,13 +265,17 @@ case grind
 p q : Prop
 a✝¹ : p = ¬q
 a✝ : p
-⊢ False[facts] Asserted facts
-  [prop] p = ¬q
-  [prop] p[eqc] True propositions
-  [prop] p = ¬q
-  [prop] ¬q
-  [prop] p[eqc] False propositions
-  [prop] q
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] p = ¬q
+    [prop] p
+  [eqc] True propositions
+    [prop] p = ¬q
+    [prop] ¬q
+    [prop] p
+  [eqc] False propositions
+    [prop] q
 -/
 #guard_msgs (error) in
 set_option trace.grind.split true in