chore: fix message

src/Init/Grind.lean

@@ -11,3 +11,4 @@ import Init.Grind.Cases
 import Init.Grind.Propagator
 import Init.Grind.Util
 import Init.Grind.Offset
+import Init.Grind.PP

src/Init/Grind/PP.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.NotationExtra
+
+namespace Lean.Grind
+/-!
+This is a hackish module for hovering node information in the `grind` tactic state.
+-/
+
+inductive NodeDef where
+  | unit
+
+set_option linter.unusedVariables false in
+def node_def (_ : Nat) {α : Sort u} {a : α} : NodeDef := .unit
+
+@[app_unexpander node_def]
+def nodeDefUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $id:num) => return mkIdent <| Name.mkSimple $ "#" ++ toString id.getNat
+  | _ => throw ()
+
+@[app_unexpander NodeDef]
+def NodeDefUnexpander : PrettyPrinter.Unexpander := fun _ => do
+  return mkIdent <| Name.mkSimple "NodeDef"
+
+end Lean.Grind

src/Init/Grind/Util.lean

@@ -9,7 +9,7 @@ import Init.Core
 namespace Lean.Grind
 
 /-- A helper gadget for annotating nested proofs in goals. -/
-def nestedProof (p : Prop) (h : p) : p := h
+def nestedProof (p : Prop) {h : p} : p := h
 
 /--
 Gadget for marking terms that should not be normalized by `grind`s simplifier.
@@ -28,7 +28,7 @@ When `EqMatch a b origin` is `True`, we mark `origin` as a resolved case-split.
 -/
 def EqMatch (a b : α) {_origin : α} : Prop := a = b
 
-theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (nestedProof p hp) (nestedProof q hq) := by
+theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (@nestedProof p hp) (@nestedProof q hq) := by
   subst h; apply HEq.refl
 
 end Lean.Grind

src/Lean/Elab/Tactic/Grind.lean

@@ -35,9 +35,9 @@ def elabGrindPattern : CommandElab := fun stx => do
   | _ => throwUnsupportedSyntax
 
 def grind (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
-  let mvarIds ← Grind.main mvarId config mainDeclName fallback
-  unless mvarIds.isEmpty do
-    throwError "`grind` failed\n{goalsToMessageData mvarIds}"
+  let goals ← Grind.main mvarId config mainDeclName fallback
+  unless goals.isEmpty do
+    throwError "`grind` failed\n{← Grind.goalsToMessageData goals}"
 
 private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit) := do
   let some fallback := fallback? | return (pure ())

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -118,7 +118,7 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
   unless (← isInconsistent) do
     if valueInconsistency then
       closeGoalWithValuesEq lhsRoot.self rhsRoot.self
-  trace_goal[grind.debug] "after addEqStep, {← ppState}"
+  trace_goal[grind.debug] "after addEqStep, {← (← get).ppState}"
   checkInvariants
 where
   go (lhs rhs : Expr) (lhsNode rhsNode lhsRoot rhsRoot : ENode) (flipped : Bool) : GoalM Unit := do
@@ -192,22 +192,27 @@ where
     processTodo
 
 /-- Adds a new equality `lhs = rhs`. It assumes `lhs` and `rhs` have already been internalized. -/
-def addEq (lhs rhs proof : Expr) : GoalM Unit := do
+private def addEq (lhs rhs proof : Expr) : GoalM Unit := do
   addEqCore lhs rhs proof false
 
-
 /-- Adds a new heterogeneous equality `HEq lhs rhs`. It assumes `lhs` and `rhs` have already been internalized. -/
-def addHEq (lhs rhs proof : Expr) : GoalM Unit := do
+private def addHEq (lhs rhs proof : Expr) : GoalM Unit := do
   addEqCore lhs rhs proof true
 
+/-- Save asserted facts for pretty printing goal. -/
+private def storeFact (fact : Expr) : GoalM Unit := do
+  modify fun s => { s with facts := s.facts.push fact }
+
 /-- Internalizes `lhs` and `rhs`, and then adds equality `lhs = rhs`. -/
 def addNewEq (lhs rhs proof : Expr) (generation : Nat) : GoalM Unit := do
+  storeFact (← mkEq lhs rhs)
   internalize lhs generation
   internalize rhs generation
   addEq lhs rhs proof
 
 /-- Adds a new `fact` justified by the given proof and using the given generation. -/
 def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
+  storeFact fact
   trace_goal[grind.assert] "{fact}"
   if (← isInconsistent) then return ()
   resetNewEqs

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -72,8 +72,8 @@ def all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List Goa
 private def simple (goals : List Goal) : GrindM (List Goal) := do
   applyToAll (assertAll >> ematchStar >> (splitNext >> assertAll >> ematchStar).iterate) goals
 
-def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List MVarId) := do
-  let go : GrindM (List MVarId) := do
+def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List Goal) := do
+  let go : GrindM (List Goal) := do
     let goals ← initCore mvarId
     let goals ← simple goals
     let goals ← goals.filterMapM fun goal => do
@@ -83,7 +83,7 @@ def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallba
       if (← goal.mvarId.isAssigned) then return none
       return some goal
     trace[grind.debug.final] "{← ppGoals goals}"
-    return goals.map (·.mvarId)
+    return goals
   go.run mainDeclName config fallback
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/PP.lean

@@ -5,62 +5,107 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.Util
+import Init.Grind.PP
 import Lean.Meta.Tactic.Grind.Types
 
 namespace Lean.Meta.Grind
 
 /-- Helper function for pretty printing the state for debugging purposes. -/
-def ppENodeRef (e : Expr) : GoalM Format := do
-  let some n ← getENode? e | return "_"
-  return f!"#{n.idx}"
+def Goal.ppENodeRef (goal : Goal) (e : Expr) : MetaM MessageData := do
+  let some n := goal.getENode? e | return "_"
+  let type ← inferType e
+  let u ← getLevel type
+  let d := mkApp3 (mkConst ``Grind.node_def [u]) (toExpr n.idx) type e
+  return m!"{d}"
+
+@[inherit_doc Goal.ppENodeRef]
+def ppENodeRef (e : Expr) : GoalM MessageData := do
+  (← get).ppENodeRef e
 
 /-- Helper function for pretty printing the state for debugging purposes. -/
-def ppENodeDeclValue (e : Expr) : GoalM Format := do
+private def Goal.ppENodeDeclValue (goal : Goal) (e : Expr) : MetaM MessageData := do
   if e.isApp && !(← isLitValue e) then
     e.withApp fun f args => do
       let r ← if f.isConst then
-        ppExpr f
+        pure m!"{f}"
       else
-        ppENodeRef f
+        goal.ppENodeRef f
       let mut r := r
       for arg in args do
-        r := r ++ " " ++ (← ppENodeRef arg)
+        r := r ++ " " ++ (← goal.ppENodeRef arg)
       return r
   else
     ppExpr e
 
 /-- Helper function for pretty printing the state for debugging purposes. -/
-def ppENodeDecl (e : Expr) : GoalM Format := do
-  let mut r := f!"{← ppENodeRef e} := {← ppENodeDeclValue e}"
-  let n ← getENode e
+private def Goal.ppENodeDecl (goal : Goal) (e : Expr) : MetaM MessageData := do
+  let mut r := m!"{← goal.ppENodeRef e} := {← goal.ppENodeDeclValue e}"
+  let n ← goal.getENode e
   unless isSameExpr e n.root do
-    r := r ++ f!" ↦ {← ppENodeRef n.root}"
+    r := r ++ m!" ↦ {← goal.ppENodeRef n.root}"
   if n.interpreted then
     r := r ++ ", [val]"
   if n.ctor then
     r := r ++ ", [ctor]"
   if grind.debug.get (← getOptions) then
-    if let some target ← getTarget? e then
-      r := r ++ f!" ↝ {← ppENodeRef target}"
+    if let some target := goal.getTarget? e then
+      r := r ++ m!" ↝ {← goal.ppENodeRef target}"
   return r
 
 /-- Pretty print goal state for debugging purposes. -/
-def ppState : GoalM Format := do
-  let mut r := f!"Goal:"
-  let nodes ← getENodes
+def Goal.ppState (goal : Goal) : MetaM MessageData := do
+  let mut r := m!"Goal:"
+  let nodes := goal.getENodes
   for node in nodes do
-    r := r ++ "\n" ++ (← ppENodeDecl node.self)
-  let eqcs ← getEqcs
+    r := r ++ "\n" ++ (← goal.ppENodeDecl node.self)
+  let eqcs := goal.getEqcs
   for eqc in eqcs do
     if eqc.length > 1 then
-      r := r ++ "\n" ++ "{" ++ (Format.joinSep (← eqc.mapM ppENodeRef) ", ") ++  "}"
+      r := r ++ "\n" ++ "{" ++ (MessageData.joinSep (← eqc.mapM goal.ppENodeRef) ", ") ++  "}"
   return r
 
-def ppGoals (goals : List Goal) : GrindM Format := do
-  let mut r := f!""
+def ppGoals (goals : List Goal) : MetaM MessageData := do
+  let mut r := m!""
   for goal in goals do
-    let (f, _) ← GoalM.run goal ppState
-    r := r ++ Format.line ++ f
+    let m ← goal.ppState
+    r := r ++ Format.line ++ m
   return r
 
+private def ppExprArray (cls : Name) (header : String) (es : Array Expr) (clsElem : Name := Name.mkSimple "_") : MessageData :=
+  let es := es.map fun e => .trace { cls := clsElem} m!"{e}" #[]
+  .trace { cls } header es
+
+private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
+   let mut trueEqc?  : Option MessageData := none
+   let mut falseEqc? : Option MessageData := none
+   let mut otherEqcs : Array MessageData := #[]
+   for eqc in goal.getEqcs do
+     if Option.isSome <| eqc.find? (·.isTrue) then
+       let eqc := eqc.filter fun e => !e.isTrue
+       unless eqc.isEmpty do
+         trueEqc? := ppExprArray `eqc "True propositions" eqc.toArray `prop
+     else if Option.isSome <| eqc.find? (·.isFalse) then
+       let eqc := eqc.filter fun e => !e.isFalse
+       unless eqc.isEmpty do
+         falseEqc? := ppExprArray `eqc "False propositions" eqc.toArray `prop
+     else if let e :: _ :: _ := eqc then
+       -- 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
+   unless otherEqcs.isEmpty do
+     result := result.push <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
+   return result
+
+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)
+  addMessageContextFull <| MessageData.joinSep m.toList ""
+
+def goalsToMessageData (goals : List Goal) : MetaM MessageData :=
+  return MessageData.joinSep (← goals.mapM goalToMessageData) m!"\n"
+
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -380,6 +380,8 @@ structure Goal where
   resolvedSplits : PHashSet ENodeKey := {}
   /-- Next local E-match theorem idx. -/
   nextThmIdx : Nat := 0
+  /-- Asserted facts -/
+  facts      : PArray Expr := {}
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -448,15 +450,26 @@ def checkMaxEmatchExceeded : GoalM Bool := do
 Returns `some n` if `e` has already been "internalized" into the
 Otherwise, returns `none`s.
 -/
+def Goal.getENode? (goal : Goal) (e : Expr) : Option ENode :=
+  goal.enodes.find? { expr := e }
+
+@[inline, inherit_doc Goal.getENode?]
 def getENode? (e : Expr) : GoalM (Option ENode) :=
-  return (← get).enodes.find? { expr := e }
+  return (← get).getENode? e
+
+def throwNonInternalizedExpr (e : Expr) : CoreM α :=
+  throwError "internal `grind` error, term has not been internalized{indentExpr e}"
 
 /-- Returns node associated with `e`. It assumes `e` has already been internalized. -/
-def getENode (e : Expr) : GoalM ENode := do
-  let some n := (← get).enodes.find? { expr := e }
-    | throwError "internal `grind` error, term has not been internalized{indentExpr e}"
+def Goal.getENode (goal : Goal) (e : Expr) : CoreM ENode := do
+  let some n := goal.enodes.find? { expr := e }
+    | throwNonInternalizedExpr e
   return n
 
+@[inline, inherit_doc Goal.getENode]
+def getENode (e : Expr) : GoalM ENode := do
+  (← get).getENode e
+
 /-- Returns the generation of the given term. Is assumes it has been internalized -/
 def getGeneration (e : Expr) : GoalM Nat :=
   return (← getENode e).generation
@@ -486,30 +499,53 @@ def isRoot (e : Expr) : GoalM Bool := do
   return isSameExpr n.root e
 
 /-- Returns the root element in the equivalence class of `e` IF `e` has been internalized. -/
-def getRoot? (e : Expr) : GoalM (Option Expr) := do
-  let some n ← getENode? e | return none
+def Goal.getRoot? (goal : Goal) (e : Expr) : Option Expr := Id.run do
+  let some n ← goal.getENode? e | return none
   return some n.root
 
+@[inline, inherit_doc Goal.getRoot?]
+def getRoot? (e : Expr) : GoalM (Option Expr) := do
+  return (← get).getRoot? e
+
 /-- Returns the root element in the equivalence class of `e`. -/
-def getRoot (e : Expr) : GoalM Expr :=
-  return (← getENode e).root
+def Goal.getRoot (goal : Goal) (e : Expr) : CoreM Expr :=
+  return (← goal.getENode e).root
+
+@[inline, inherit_doc Goal.getRoot]
+def getRoot (e : Expr) : GoalM Expr := do
+  (← get).getRoot e
 
 /-- Returns the root enode in the equivalence class of `e`. -/
 def getRootENode (e : Expr) : GoalM ENode := do
   getENode (← getRoot e)
 
+/--
+Returns the next element in the equivalence class of `e`
+if `e` has been internalized in the given goal.
+-/
+def Goal.getNext? (goal : Goal) (e : Expr) : Option Expr := Id.run do
+  let some n ← goal.getENode? e | return none
+  return some n.next
+
 /-- Returns the next element in the equivalence class of `e`. -/
-def getNext (e : Expr) : GoalM Expr :=
-  return (← getENode e).next
+def Goal.getNext (goal : Goal) (e : Expr) : CoreM Expr :=
+  return (← goal.getENode e).next
+
+@[inline, inherit_doc Goal.getRoot]
+def getNext (e : Expr) : GoalM Expr := do
+  (← get).getNext e
 
 /-- Returns `true` if `e` has already been internalized. -/
 def alreadyInternalized (e : Expr) : GoalM Bool :=
   return (← get).enodes.contains { expr := e }
 
-def getTarget? (e : Expr) : GoalM (Option Expr) := do
-  let some n ← getENode? e | return none
+def Goal.getTarget? (goal : Goal) (e : Expr) : Option Expr := Id.run do
+  let some n ← goal.getENode? e | return none
   return n.target?
 
+@[inline] def getTarget? (e : Expr) : GoalM (Option Expr) := do
+  return (← get).getTarget? e
+
 /--
 If `isHEq` is `false`, it pushes `lhs = rhs` with `proof` to `newEqs`.
 Otherwise, it pushes `HEq lhs rhs`.
@@ -681,11 +717,14 @@ def closeGoal (falseProof : Expr) : GoalM Unit := do
     else
       mvarId.assign (← mkFalseElim target falseProof)
 
+def Goal.getENodes (goal : Goal) : Array ENode :=
+  -- We must sort because we are using pointer addresses as keys in `enodes`
+  let nodes := goal.enodes.toArray.map (·.2)
+  nodes.qsort fun a b => a.idx < b.idx
+
 /-- Returns all enodes in the goal -/
 def getENodes : GoalM (Array ENode) := do
-  -- We must sort because we are using pointer addresses as keys in `enodes`
-  let nodes := (← get).enodes.toArray.map (·.2)
-  return nodes.qsort fun a b => a.idx < b.idx
+  return (← get).getENodes
 
 /-- Executes `f` to each term in the equivalence class containing `e` -/
 @[inline] def traverseEqc (e : Expr) (f : ENode → GoalM Unit) : GoalM Unit := do
@@ -743,26 +782,34 @@ def applyFallback : GoalM Unit := do
   fallback
 
 /-- Returns expressions in the given expression equivalence class. -/
-partial def getEqc (e : Expr) : GoalM (List Expr) :=
+partial def Goal.getEqc (goal : Goal) (e : Expr) : List Expr :=
   go e e []
 where
-  go (first : Expr) (e : Expr) (acc : List Expr) : GoalM (List Expr) := do
-    let next ← getNext e
+  go (first : Expr) (e : Expr) (acc : List Expr) : List Expr := Id.run do
+    let some next ← goal.getNext? e | acc
     let acc := e :: acc
     if isSameExpr first next then
       return acc
     else
       go first next acc
 
+@[inline, inherit_doc Goal.getEqc]
+partial def getEqc (e : Expr) : GoalM (List Expr) :=
+  return (← get).getEqc e
+
 /-- Returns all equivalence classes in the current goal. -/
-partial def getEqcs : GoalM (List (List Expr)) := do
-  let mut r := []
-  let nodes ← getENodes
+partial def Goal.getEqcs (goal : Goal) : List (List Expr) := Id.run do
+  let mut r : List (List Expr) := []
+  let nodes ← goal.getENodes
   for node in nodes do
     if isSameExpr node.root node.self then
-      r := (← getEqc node.self) :: r
+      r := goal.getEqc node.self :: r
   return r
 
+@[inline, inherit_doc Goal.getEqcs]
+def getEqcs : GoalM (List (List Expr)) :=
+  return (← get).getEqcs
+
 /-- Returns `true` if `e` is a case-split that does not need to be performed anymore. -/
 def isResolvedCaseSplit (e : Expr) : GoalM Bool :=
   return (← get).resolvedSplits.contains { expr := e }

tests/lean/run/grind_erase_attr.lean

@@ -24,17 +24,15 @@ example : f (f (f a)) = f a := by
 attribute [-grind] fthm
 
 /--
-error: `grind` failed
-case grind
+error: unsolved goals
 a : Nat
-x✝ : ¬f (f (f a)) = f a
-⊢ False
+⊢ f (f (f a)) = f a
 ---
 info: [grind.assert] ¬f (f (f a)) = f a
 -/
 #guard_msgs (info, error) in
 example : f (f (f a)) = f a := by
-  grind
+  fail_if_success grind
 
 /--
 error: `fthm` is not marked with the `[grind]` attribute
@@ -60,13 +58,9 @@ example : g a = b → a = 0 → b = 1 := by
 attribute [-grind] g
 
 /--
-error: `grind` failed
-case grind
+error: unsolved goals
 a b : Nat
-a✝¹ : g a = b
-a✝ : a = 0
-x✝ : ¬b = 1
-⊢ False
+⊢ g a = b → a = 0 → b = 1
 ---
 info: [grind.assert] g a = b
 [grind.assert] a = 0
@@ -74,7 +68,7 @@ info: [grind.assert] g a = b
 -/
 #guard_msgs (info, error) in
 example : g a = b → a = 0 → b = 1 := by
-  grind
+  fail_if_success grind
 
 /--
 error: `g` is not marked with the `[grind]` attribute

tests/lean/run/grind_nested_proofs.lean

@@ -22,9 +22,9 @@ detect equalities between array access terms.
 -/
 
 /--
-info: [Meta.debug] [Lean.Grind.nestedProof (i < a.toList.length) (_example.proof_1 i j a b h1 h2),
-     Lean.Grind.nestedProof (j < a.toList.length) h1,
-     Lean.Grind.nestedProof (j < b.toList.length) h]
+info: [Meta.debug] [Lean.Grind.nestedProof (i < a.toList.length),
+     Lean.Grind.nestedProof (j < a.toList.length),
+     Lean.Grind.nestedProof (j < b.toList.length)]
 [Meta.debug] [a[i], b[j], a[j]]
 -/
 #guard_msgs (info) in
@@ -32,9 +32,9 @@ example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i
   grind on_failure fallback
 
 /--
-info: [Meta.debug] [Lean.Grind.nestedProof (i < a.toList.length) (_example.proof_1 i j a b h1 h2),
-     Lean.Grind.nestedProof (j < a.toList.length) h1,
-     Lean.Grind.nestedProof (j < b.toList.length) h]
+info: [Meta.debug] [Lean.Grind.nestedProof (i < a.toList.length),
+     Lean.Grind.nestedProof (j < a.toList.length),
+     Lean.Grind.nestedProof (j < b.toList.length)]
 [Meta.debug] [a[i], a[j]]
 -/
 #guard_msgs (info) in

tests/lean/run/grind_pre.lean

@@ -13,7 +13,23 @@ left : p
 right : q
 h✝ : b = false
 h : c = true
-⊢ False
+⊢ 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}
 -/
 #guard_msgs (error) in
 theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
@@ -30,7 +46,16 @@ h✝ : c = true
 left : p
 right : q
 h : b = false
-⊢ 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}
 -/
 #guard_msgs (error) in
 theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
@@ -45,7 +70,11 @@ i j : Nat
 h : j + 1 < i + 1
 h✝ : j + 1 ≤ i
 x✝ : ¬g (i + 1) j ⋯ = i + j + 1
-⊢ False
+⊢ 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
 -/
 #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
@@ -70,7 +99,15 @@ head_eq : a₁ = b₁
 x_eq : a₂ = b₂
 y_eq : a₃ = b₃
 tail_eq : as = bs
-⊢ False
+⊢ 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₁}
 -/
 #guard_msgs (error) in
 theorem ex3 (h : a₁ :: { x := a₂, y := a₃ : Point } :: as = b₁ :: { x := b₂, y := b₃} :: bs) : False := by
@@ -93,8 +130,22 @@ h₂ : HEq q a
 h₃ : p = r
 left : ¬p ∨ r
 h : ¬r
-⊢ False
-
+⊢ 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
 case grind.2
 α : Type
 a : α
@@ -104,7 +155,22 @@ h₂ : HEq q a
 h₃ : p = r
 left : ¬p ∨ r
 h : p
-⊢ False
+⊢ 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
 -/
 #guard_msgs (error) in
 example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by

tests/lean/run/grind_t1.lean

@@ -244,7 +244,12 @@ case grind
 p q : Prop
 a✝¹ : p = q
 a✝ : p
-⊢ False
+⊢ False[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
@@ -257,7 +262,13 @@ case grind
 p q : Prop
 a✝¹ : p = ¬q
 a✝ : p
-⊢ False
+⊢ False[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