chore: fix tests

src/Init/Grind/Tactics.lean

@@ -67,6 +67,8 @@ structure Config where
   ext : Bool := true
   /-- If `verbose` is `false`, additional diagnostics information is not collected. -/
   verbose : Bool := true
+  /-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/
+  clean : Bool := true
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Lean/Meta/Tactic/ExposeNames.lean

@@ -36,7 +36,7 @@ def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.wi
     let mut baseName := localDecl.userName
     if baseName.hasMacroScopes then
       baseName := baseName.eraseMacroScopes
-      if baseName == `x then
+      if baseName == `x || baseName == `a then
         if (← isProp localDecl.type) then
           baseName := `h
     let mut userName := baseName

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

@@ -82,7 +82,7 @@ Updates the modification time to `gmt` for the parents of `root`.
 The modification time is used to decide which terms are considered during e-matching.
 -/
 private partial def updateMT (root : Expr) : GoalM Unit := do
-  let gmt := (← get).gmt
+  let gmt := (← get).ematch.gmt
   for parent in (← getParents root) do
     let node ← getENode parent
     if node.mt < gmt then

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

@@ -58,12 +58,12 @@ structure Context where
   deriving Inhabited
 
 /-- State for the E-matching monad -/
-structure State where
+structure SearchState where
   /-- Choices that still have to be processed. -/
   choiceStack  : List Choice := []
   deriving Inhabited
 
-abbrev M := ReaderT Context $ StateRefT State GoalM
+abbrev M := ReaderT Context $ StateRefT SearchState GoalM
 
 def M.run' (x : M α) : GoalM α :=
   x {} |>.run' {}
@@ -315,7 +315,7 @@ private def processChoices : M Unit := do
   while !(← get).choiceStack.isEmpty do
     checkSystem "ematch"
     if (← checkMaxInstancesExceeded) then return ()
-    let c ← modifyGet fun s : State => (s.choiceStack.head!, { s with choiceStack := s.choiceStack.tail! })
+    let c ← modifyGet fun s : SearchState => (s.choiceStack.head!, { s with choiceStack := s.choiceStack.tail! })
     if c.gen < maxGeneration then
       match c.cnstrs with
       | [] => instantiateTheorem c
@@ -329,7 +329,7 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
   let numParams  := (← read).thm.numParams
   let assignment := mkArray numParams unassigned
   let useMT      := (← read).useMT
-  let gmt        := (← getThe Goal).gmt
+  let gmt        := (← getThe Goal).ematch.gmt
   for app in apps do
     if (← checkMaxInstancesExceeded) then return ()
     let n ← getENode app
@@ -351,7 +351,7 @@ private def matchEqBwdPat (p : Expr) : M Unit := do
   let numParams  := (← read).thm.numParams
   let assignment := mkArray numParams unassigned
   let useMT      := (← read).useMT
-  let gmt        := (← getThe Goal).gmt
+  let gmt        := (← getThe Goal).ematch.gmt
   let false      ← getFalseExpr
   let mut curr   := false
   repeat
@@ -412,19 +412,19 @@ def ematch : GoalM Unit := do
   if (← checkMaxInstancesExceeded <||> checkMaxEmatchExceeded) then
     return ()
   else
-    go (← get).thms (← get).newThms |>.run'
+    go (← get).ematch.thms (← get).ematch.newThms |>.run'
     modify fun s => { s with
-      thms         := s.thms ++ s.newThms
-      newThms      := {}
-      gmt          := s.gmt + 1
-      numEmatch    := s.numEmatch + 1
+      ematch.thms      := s.ematch.thms ++ s.ematch.newThms
+      ematch.newThms   := {}
+      ematch.gmt       := s.ematch.gmt + 1
+      ematch.num       := s.ematch.num + 1
     }
 
 /-- Performs one round of E-matching, and assert new instances. -/
 def ematchAndAssert : GrindTactic := fun goal => do
-  let numInstances := goal.numInstances
+  let numInstances := goal.ematch.numInstances
   let goal ← GoalM.run' goal ematch
-  if goal.numInstances == numInstances then
+  if goal.ematch.numInstances == numInstances then
     return none
   assertAll goal
 

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

@@ -64,20 +64,20 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   let origin ← if let some fvarId := isEqTrueHyp? proof then
     pure <| .fvar fvarId
   else
-    let idx ← modifyGet fun s => (s.nextThmIdx, { s with nextThmIdx := s.nextThmIdx + 1 })
+    let idx ← modifyGet fun s => (s.ematch.nextThmIdx, { s with ematch.nextThmIdx := s.ematch.nextThmIdx + 1 })
     pure <| .local ((`local).appendIndexAfter idx)
   let proof := mkOfEqTrueCore e proof
-  let size := (← get).newThms.size
+  let size := (← get).ematch.newThms.size
   let gen ← getGeneration e
   -- TODO: we should have a flag for collecting all unary patterns in a local theorem
   if let some thm ← mkEMatchTheoremWithKind'? origin proof .leftRight then
     activateTheorem thm gen
   if let some thm ← mkEMatchTheoremWithKind'? origin proof .rightLeft then
     activateTheorem thm gen
-  if (← get).newThms.size == size then
+  if (← get).ematch.newThms.size == size then
     if let some thm ← mkEMatchTheoremWithKind'? origin proof .default then
       activateTheorem thm gen
-  if (← get).newThms.size == size then
+  if (← get).ematch.newThms.size == size then
     reportIssue! "failed to create E-match local theorem for{indentExpr e}"
 
 def propagateForallPropDown (e : Expr) : GoalM Unit := do

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

@@ -52,7 +52,7 @@ private def updateAppMap (e : Expr) : GoalM Unit := do
 /-- Inserts `e` into the list of case-split candidates. -/
 private def addSplitCandidate (e : Expr) : GoalM Unit := do
   trace_goal[grind.split.candidate] "{e}"
-  modify fun s => { s with splitCandidates := e :: s.splitCandidates }
+  modify fun s => { s with split.candidates := e :: s.split.candidates }
 
 private def forbiddenSplitTypes := [``Eq, ``HEq, ``True, ``False]
 
@@ -85,13 +85,13 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
         return ()
       unless (← isInductivePredicate declName) do
         return ()
-      if (← get).casesTypes.isSplit declName then
+      if (← get).split.casesTypes.isSplit declName then
         addSplitCandidate e
       else if (← getConfig).splitIndPred then
         addSplitCandidate e
   | .fvar .. =>
     let .const declName _ := (← whnfD (← inferType e)).getAppFn | return ()
-    if (← get).casesTypes.isSplit declName then
+    if (← get).split.casesTypes.isSplit declName then
       addSplitCandidate e
   | _ => pure ()
 
@@ -142,7 +142,7 @@ def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
   let proof ← shareCommon thm.proof
   let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation)) }
   trace_goal[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}"
-  modify fun s => { s with newThms := s.newThms.push thm }
+  modify fun s => { s with ematch.newThms := s.ematch.newThms.push thm }
 
 /--
 If `Config.matchEqs` is set to `true`, and `f` is `match`-auxiliary function,
@@ -152,25 +152,25 @@ private def addMatchEqns (f : Expr) (generation : Nat) : GoalM Unit := do
   if !(← getConfig).matchEqs then return ()
   let .const declName _ := f | return ()
   if !(← isMatcher declName) then return ()
-  if (← get).matchEqNames.contains declName then return ()
-  modify fun s => { s with matchEqNames := s.matchEqNames.insert declName }
+  if (← get).ematch.matchEqNames.contains declName then return ()
+  modify fun s => { s with ematch.matchEqNames := s.ematch.matchEqNames.insert declName }
   for eqn in (← Match.getEquationsFor declName).eqnNames do
     -- We disable pattern normalization to prevent the `match`-expression to be reduced.
     activateTheorem (← mkEMatchEqTheorem eqn (normalizePattern := false)) generation
 
 private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
-  if let some (thms, thmMap) := (← get).thmMap.retrieve? fName then
-    modify fun s => { s with thmMap }
+  if let some (thms, thmMap) := (← get).ematch.thmMap.retrieve? fName then
+    modify fun s => { s with ematch.thmMap := thmMap }
     let appMap := (← get).appMap
     for thm in thms do
-      unless (← get).thmMap.isErased thm.origin do
+      unless (← get).ematch.thmMap.isErased thm.origin do
         let symbols := thm.symbols.filter fun sym => !appMap.contains sym
         let thm := { thm with symbols }
         match symbols with
         | [] => activateTheorem thm generation
         | _ =>
           trace_goal[grind.ematch] "reinsert `{thm.origin.key}`"
-          modify fun s => { s with thmMap := s.thmMap.insert thm }
+          modify fun s => { s with ematch.thmMap := s.ematch.thmMap.insert thm }
 
 /--
 If type of `a` is an inductive datatype with one constructor `ctor` without fields,

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

@@ -35,21 +35,74 @@ private def preprocessHypothesis (e : Expr) : GoalM Simp.Result := do
   else
     preprocess e
 
+/--
+Helper function for `mkCleanName`.
+Creates a base name for creating a clean name for `name`.
+It ensures base name is a simple `Name` and does not have a `_<idx>` suffix
+-/
+private def mkBaseName (name : Name) (type : Expr) : MetaM Name := do
+  if let .str _ s := name then
+    let pos := s.find (· == '_')
+    unless pos < s.endPos do
+      return Name.mkSimple s
+    let suffix := s.extract (pos+'_') s.endPos
+    unless suffix.isNat do
+      return Name.mkSimple s
+    let s := s.extract ⟨0⟩ pos
+    unless s == "" do
+      return Name.mkSimple s
+  if (← isProp type) then return `h else return `x
+
+private def mkCleanName (name : Name) (type : Expr) : GoalM Name := do
+  unless (← getConfig).clean do
+    return name
+  let mut name := name
+  if name.hasMacroScopes then
+    name := name.eraseMacroScopes
+    if name == `x || name == `a then
+      if (← isProp type) then
+        name := `h
+  if (← get).clean.used.contains name then
+    let base ← mkBaseName name type
+    let mut i := if let some i := (← get).clean.next.find? base then i else 1
+    repeat
+      name := base.appendIndexAfter i
+      i := i + 1
+      unless (← get).clean.used.contains name do
+        break
+    modify fun s => { s with clean.next := s.clean.next.insert base i }
+  modify fun s => { s with clean.used := s.clean.used.insert name }
+  return name
+
+private def intro1 : GoalM FVarId := do
+  let target ← (← get).mvarId.getType
+  let (name, type) ← match target with
+    | .forallE n d .. => pure (n, d)
+    | .letE n d .. => pure (n, d)
+    | _ =>
+      let some (n, d, _) := target.letFun? |
+        throwError "`grind` internal error, binder expected"
+      pure (n, d)
+  let name ← mkCleanName name type
+  let (fvarId, mvarId) ← (← get).mvarId.intro name
+  modify fun s => { s with mvarId }
+  return fvarId
+
 private def introNext (goal : Goal) (generation : Nat) : GrindM IntroResult := do
-  let target ← goal.mvarId.getType
-  if target.isArrow then
-    let (r, _) ← GoalM.run goal do
-      let mvarId := (← get).mvarId
+  Prod.fst <$> GoalM.run goal do
+    let target ← (← get).mvarId.getType
+    if target.isArrow then
       let p := target.bindingDomain!
       if !(← isProp p) then
-        let (fvarId, mvarId) ← mvarId.intro1P
-        return .newLocal fvarId { (← get) with mvarId }
+        let fvarId ← intro1
+        return .newLocal fvarId (← get)
       else
-        let tag ← mvarId.getTag
+        let tag ← (← get).mvarId.getTag
         let q := target.bindingBody!
         let r ← preprocessHypothesis p
         let fvarId ← mkFreshFVarId
-        let lctx := (← getLCtx).mkLocalDecl fvarId target.bindingName! r.expr target.bindingInfo!
+        let lctx := (← getLCtx).mkLocalDecl fvarId (← mkCleanName target.bindingName! r.expr) r.expr target.bindingInfo!
+        let mvarId := (← get).mvarId
         let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) q .syntheticOpaque tag
         let mvarIdNew := mvarNew.mvarId!
         mvarIdNew.withContext do
@@ -63,32 +116,29 @@ private def introNext (goal : Goal) (generation : Nat) : GrindM IntroResult := d
             -- `p` and `p'` are definitionally equal
             mvarId.assign h
             return .newHyp fvarId { (← get) with mvarId := mvarIdNew }
-    return r
-  else if target.isLet || target.isForall || target.isLetFun then
-    let (fvarId, mvarId) ← goal.mvarId.intro1P
-    mvarId.withContext do
-      let localDecl ← fvarId.getDecl
-      if (← isProp localDecl.type) then
-        -- Add a non-dependent copy
-        let mvarId ← mvarId.assert (← mkFreshUserName localDecl.userName) localDecl.type (mkFVar fvarId)
-        return .newDepHyp { goal with mvarId }
-      else
-        let goal := { goal with mvarId }
-        if target.isLet || target.isLetFun then
-          let goal ← GoalM.run' goal do
+    else if target.isLet || target.isForall || target.isLetFun then
+      let fvarId ← intro1
+      (← get).mvarId.withContext do
+        let localDecl ← fvarId.getDecl
+        if (← isProp localDecl.type) then
+          -- Add a non-dependent copy
+          let mvarId ← (← get).mvarId.assert (← mkCleanName `h localDecl.type) localDecl.type (mkFVar fvarId)
+          return .newDepHyp { (← get) with mvarId }
+        else
+          if target.isLet || target.isLetFun then
             let v := (← fvarId.getDecl).value
             let r ← preprocessHypothesis v
             let x ← shareCommon (mkFVar fvarId)
             addNewEq x r.expr (← r.getProof) generation
-          return .newLocal fvarId goal
-        else
-          return .newLocal fvarId goal
-  else
-    return .done
+            return .newLocal fvarId (← get)
+          else
+            return .newLocal fvarId (← get)
+    else
+      return .done
 
 private def isEagerCasesCandidate (goal : Goal) (type : Expr) : Bool := Id.run do
   let .const declName _ := type.getAppFn | return false
-  return goal.casesTypes.isEagerSplit declName
+  return goal.split.casesTypes.isEagerSplit declName
 
 private def applyCases? (goal : Goal) (fvarId : FVarId) : GrindM (Option (List Goal)) := goal.mvarId.withContext do
   let type ← whnfD (← fvarId.getType)

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind.Lemmas
 import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.ExposeNames
 import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Proj
@@ -65,7 +66,15 @@ def GrindM.run (x : GrindM α) (mainDeclName : Name) (params : Params) (fallback
   x (← mkMethods fallback).toMethodsRef { mainDeclName, config, simprocs, simp }
     |>.run' { scState, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr }
 
+private def mkCleanState (mvarId : MVarId) (params : Params) : MetaM Clean.State := mvarId.withContext do
+  unless params.config.clean do return {}
+  let mut used : PHashSet Name := {}
+  for localDecl in (← getLCtx) do
+    used := used.insert localDecl.userName
+  return { used }
+
 private def mkGoal (mvarId : MVarId) (params : Params) : GrindM Goal := do
+  let mvarId ← if params.config.clean then mvarId.exposeNames else pure mvarId
   let trueExpr ← getTrueExpr
   let falseExpr ← getFalseExpr
   let btrueExpr ← getBoolTrueExpr
@@ -73,7 +82,8 @@ private def mkGoal (mvarId : MVarId) (params : Params) : GrindM Goal := do
   let natZeroExpr ← getNatZeroExpr
   let thmMap := params.ematch
   let casesTypes := params.casesTypes
-  GoalM.run' { mvarId, thmMap, casesTypes } do
+  let clean ← mkCleanState mvarId params
+  GoalM.run' { mvarId, ematch.thmMap := thmMap, split.casesTypes := casesTypes, clean } do
     mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0)
     mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0)
     mkENodeCore btrueExpr (interpreted := false) (ctor := true) (generation := 0)

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

@@ -110,8 +110,8 @@ private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
 
 private def ppActiveTheoremPatterns : 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)
+  let m ← goal.ematch.thms.toArray.mapM fun thm => ppEMatchTheorem thm
+  let m := m ++ (← goal.ematch.newThms.toArray.mapM fun thm => ppEMatchTheorem thm)
   unless m.isEmpty do
     pushMsg <| .trace { cls := `ematch } "E-matching patterns" m
 
@@ -131,11 +131,11 @@ 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
+  if goal.ematch.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
+  if goal.ematch.num ≥ 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
+  if goal.split.num ≥ 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})`" #[]
@@ -144,9 +144,9 @@ private def ppThresholds (c : Grind.Config) : M Unit := do
 
 private def ppCasesTrace : M Unit := do
   let goal ← read
-  unless goal.casesTrace.isEmpty do
+  unless goal.split.trace.isEmpty do
     let mut msgs := #[]
-    for { expr, i , num } in goal.casesTrace.reverse do
+    for { expr, i , num } in goal.split.trace.reverse do
       msgs := msgs.push <| .trace { cls := `cases } m!"[{i+1}/{num}]: {expr}" #[]
     pushMsg <| .trace { cls := `cases } "Case analyses" msgs
 

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

@@ -76,7 +76,7 @@ private def checkIffStatus (e a b : Expr) : GoalM CaseSplitStatus := do
 
 /-- Returns `true` is `c` is congruent to a case-split that was already performed. -/
 private def isCongrToPrevSplit (c : Expr) : GoalM Bool := do
-  (← get).resolvedSplits.foldM (init := false) fun flag { expr := c' } => do
+  (← get).split.resolved.foldM (init := false) fun flag { expr := c' } => do
     if flag then
       return true
     else
@@ -118,19 +118,19 @@ private inductive SplitCandidate where
 private def selectNextSplit? : GoalM SplitCandidate := do
   if (← isInconsistent) then return .none
   if (← checkMaxCaseSplit) then return .none
-  go (← get).splitCandidates .none []
+  go (← get).split.candidates .none []
 where
   go (cs : List Expr) (c? : SplitCandidate) (cs' : List Expr) : GoalM SplitCandidate := do
     match cs with
     | [] =>
-      modify fun s => { s with splitCandidates := cs'.reverse }
+      modify fun s => { s with split.candidates := cs'.reverse }
       if let .some _ numCases isRec := c? then
-        let numSplits := (← get).numSplits
+        let numSplits := (← get).split.num
         -- We only increase the number of splits if there is more than one case or it is recursive.
         let numSplits := if numCases > 1 || isRec then numSplits + 1 else numSplits
         -- Remark: we reset `numEmatch` after each case split.
         -- We should consider other strategies in the future.
-        modify fun s => { s with numSplits, numEmatch := 0 }
+        modify fun s => { s with split.num := numSplits, ematch.num := 0 }
       return c?
     | c::cs =>
     match (← checkCaseSplitStatus c) with
@@ -196,7 +196,7 @@ def splitNext : GrindTactic := fun goal => do
       cases (← get).mvarId major
     let goal ← get
     let numSubgoals := mvarIds.length
-    let goals := mvarIds.mapIdx fun i mvarId => { goal with mvarId, casesTrace := { expr := c, i, num := numSubgoals } :: goal.casesTrace }
+    let goals := mvarIds.mapIdx fun i mvarId => { goal with mvarId, split.trace := { expr := c, i, num := numSubgoals } :: goal.split.trace }
     let goals ← introNewHyp goals [] genNew
     return some goals
   return goals?

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

@@ -441,6 +441,56 @@ structure CaseTrace where
   num  : Nat
   deriving Inhabited
 
+/-- E-matching related fields for the `grind` goal. -/
+structure EMatch.State where
+  /--
+  Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols.
+  Local theorem provided by users are added directly into `newThms`.
+  -/
+  thmMap       : EMatchTheorems
+  /-- Goal modification time. -/
+  gmt          : Nat := 0
+  /-- Active theorems that we have performed ematching at least once. -/
+  thms         : PArray EMatchTheorem := {}
+  /-- Active theorems that we have not performed any round of ematching yet. -/
+  newThms      : PArray EMatchTheorem := {}
+  /-- Number of theorem instances generated so far -/
+  numInstances : Nat := 0
+  /-- Number of E-matching rounds performed in this goal since the last case-split. -/
+  num          : Nat := 0
+  /-- (pre-)instances found so far. It includes instances that failed to be instantiated. -/
+  preInstances : PreInstanceSet := {}
+  /-- Next local E-match theorem idx. -/
+  nextThmIdx   : Nat := 0
+  /-- `match` auxiliary functions whose equations have already been created and activated. -/
+  matchEqNames : PHashSet Name := {}
+  deriving Inhabited
+
+/-- Case splitting related fields for the `grind` goal. -/
+structure Split.State where
+  /-- Inductive datatypes marked for case-splitting -/
+  casesTypes : CasesTypes := {}
+  /-- Case-split candidates. -/
+  candidates : List Expr := []
+  /-- Number of splits performed to get to this goal. -/
+  num        : Nat := 0
+  /-- Case-splits that have already been performed, or that do not have to be performed anymore. -/
+  resolved   : PHashSet ENodeKey := {}
+  /--
+  Sequence of cases steps that generated this goal. We only use this information for diagnostics.
+  Remark: `casesTrace.length ≥ numSplits` because we don't increase the counter for `cases`
+  applications that generated only 1 subgoal.
+  -/
+  trace      : List CaseTrace := []
+  deriving Inhabited
+
+/-- Clean name generator. -/
+structure Clean.State where
+  used : PHashSet Name := {}
+  next : PHashMap Name Nat := {}
+  deriving Inhabited
+
+/-- The `grind` goal. -/
 structure Goal where
   mvarId       : MVarId
   canon        : Canon.State := {}
@@ -457,51 +507,22 @@ structure Goal where
   newEqs       : Array NewEq := #[]
   /-- `inconsistent := true` if `ENode`s for `True` and `False` are in the same equivalence class. -/
   inconsistent : Bool := false
-  /-- Goal modification time. -/
-  gmt          : Nat := 0
   /-- Next unique index for creating ENodes -/
   nextIdx      : Nat := 0
-  /-- State of arithmetic procedures -/
-  arith        : Arith.State := {}
-  /-- Inductive datatypes marked for case-splitting -/
-  casesTypes : CasesTypes := {}
-  /-- Active theorems that we have performed ematching at least once. -/
-  thms         : PArray EMatchTheorem := {}
-  /-- Active theorems that we have not performed any round of ematching yet. -/
-  newThms      : PArray EMatchTheorem := {}
-  /--
-  Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols.
-  Local theorem provided by users are added directly into `newThms`.
-  -/
-  thmMap       : EMatchTheorems
-  /-- Number of theorem instances generated so far -/
-  numInstances : Nat := 0
-  /-- Number of E-matching rounds performed in this goal since the last case-split. -/
-  numEmatch    : Nat := 0
-  /-- (pre-)instances found so far. It includes instances that failed to be instantiated. -/
-  preInstances : PreInstanceSet := {}
   /-- new facts to be processed. -/
   newFacts     : Std.Queue NewFact := ∅
-  /-- `match` auxiliary functions whose equations have already been created and activated. -/
-  matchEqNames : PHashSet Name := {}
-  /-- Case-split candidates. -/
-  splitCandidates : List Expr := []
-  /-- Number of splits performed to get to this goal. -/
-  numSplits : Nat := 0
-  /-- Case-splits that have already been performed, or that do not have to be performed anymore. -/
-  resolvedSplits : PHashSet ENodeKey := {}
-  /-- Next local E-match theorem idx. -/
-  nextThmIdx : Nat := 0
   /-- Asserted facts -/
   facts      : PArray Expr := {}
   /-- Cached extensionality theorems for types. -/
   extThms    : PHashMap ENodeKey (Array Ext.ExtTheorem) := {}
-  /--
-  Sequence of cases steps that generated this goal. We only use this information for diagnostics.
-  Remark: `casesTrace.length ≥ numSplits` because we don't increase the counter for `cases`
-  applications that generated only 1 subgoal.
-  -/
-  casesTrace : List CaseTrace := []
+  /-- State of the E-matching module. -/
+  ematch     : EMatch.State
+  /-- State of the case-splitting module. -/
+  split      : Split.State := {}
+  /-- State of arithmetic procedures. -/
+  arith      : Arith.State := {}
+  /-- State of the clean name generator. -/
+  clean      : Clean.State := {}
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -540,9 +561,9 @@ It returns `true` if it is a new instance and `false` otherwise.
 -/
 def markTheoremInstance (proof : Expr) (assignment : Array Expr) : GoalM Bool := do
   let k := { proof, assignment }
-  if (← get).preInstances.contains k then
+  if (← get).ematch.preInstances.contains k then
     return false
-  modify fun s => { s with preInstances := s.preInstances.insert k }
+  modify fun s => { s with ematch.preInstances := s.ematch.preInstances.insert k }
   return true
 
 /-- Adds a new fact `prop` with proof `proof` to the queue for processing. -/
@@ -553,19 +574,19 @@ def addNewFact (proof : Expr) (prop : Expr) (generation : Nat) : GoalM Unit := d
 def addTheoremInstance (thm : EMatchTheorem) (proof : Expr) (prop : Expr) (generation : Nat) : GoalM Unit := do
   saveEMatchTheorem thm
   addNewFact proof prop generation
-  modify fun s => { s with numInstances := s.numInstances + 1 }
+  modify fun s => { s with ematch.numInstances := s.ematch.numInstances + 1 }
 
 /-- Returns `true` if the maximum number of instances has been reached. -/
 def checkMaxInstancesExceeded : GoalM Bool := do
-  return (← get).numInstances >= (← getConfig).instances
+  return (← get).ematch.numInstances >= (← getConfig).instances
 
 /-- Returns `true` if the maximum number of case-splits has been reached. -/
 def checkMaxCaseSplit : GoalM Bool := do
-  return (← get).numSplits >= (← getConfig).splits
+  return (← get).split.num >= (← getConfig).splits
 
 /-- Returns `true` if the maximum number of E-matching rounds has been reached. -/
 def checkMaxEmatchExceeded : GoalM Bool := do
-  return (← get).numEmatch >= (← getConfig).ematch
+  return (← get).ematch.num >= (← getConfig).ematch
 
 /--
 Returns `some n` if `e` has already been "internalized" into the
@@ -766,7 +787,7 @@ def mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) : GoalM
     flipped := false
     heqProofs := false
     hasLambdas := e.isLambda
-    mt := (← get).gmt
+    mt := (← get).ematch.gmt
     idx := (← get).nextIdx
     interpreted, ctor, generation
   }
@@ -1020,7 +1041,7 @@ def getEqcs : GoalM (List (List Expr)) :=
 
 /-- 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 }
+  return (← get).split.resolved.contains { expr := e }
 
 /--
 Mark `e` as a case-split that does not need to be performed anymore.
@@ -1030,7 +1051,7 @@ Remark: we also use this feature to record the case-splits that have already bee
 def markCaseSplitAsResolved (e : Expr) : GoalM Unit := do
   unless (← isResolvedCaseSplit e) do
     trace_goal[grind.split.resolved] "{e}"
-    modify fun s => { s with resolvedSplits := s.resolvedSplits.insert { expr := e } }
+    modify fun s => { s with split.resolved := s.split.resolved.insert { expr := e } }
 
 /--
 Returns extensionality theorems for the given type if available.

tests/lean/grind_guide.lean.expected.out

@@ -1,239 +0,0 @@
-[grind.assert] a = 3
-[grind.assert] b = 3
-[grind.assert] ¬a = b
-[grind.eqc] f a = [1, 2]
-[grind.eqc] f b = []
-[grind.eqc] a = b
-[grind.eqc] f a = f b
-[grind.split] match x with
-    | 0 => 1
-    | n.succ => 2, generation: 0
-grind_guide.lean:60:2-60:21: error: `grind` failed
-case grind
-x : Nat
-x✝ :
-  (match x with
-    | 0 => 1
-    | n.succ => 2) =
-    0
-⊢ False
-[grind] Diagnostics
-  [facts] Asserted facts
-    [prop] (match x with
-          | 0 => 1
-          | n.succ => 2) =
-          0
-  [eqc] Equivalence classes
-    [eqc] {match x with
-        | 0 => 1
-        | n.succ => 2,
-        0}
-  [ematch] E-matching patterns
-    [thm] _example.match_1.eq_1: [_example.match_1 #2 `[0] #1 #0]
-    [thm] _example.match_1.eq_2: [_example.match_1 #3 (#2 + 1) #1 #0]
-  [limits] Thresholds reached
-    [limit] maximum number of case-splits has been reached, threshold: `(splits := 0)`
-grind_guide.lean:68:2-68:7: error: `grind` failed
-case grind.1
-x : Nat
-x✝ :
-  (match x with
-    | 0 => 1
-    | n.succ => 2) ≤
-    1
-h : x = 0
-⊢ False
-[grind] Diagnostics
-  [facts] Asserted facts
-    [prop] (match x with
-          | 0 => 1
-          | n.succ => 2) ≤
-          1
-    [prop] x = 0
-    [prop] (match 0 with
-          | 0 => 1
-          | n.succ => 2) =
-          1
-  [eqc] True propositions
-    [prop] (match x with
-          | 0 => 1
-          | n.succ => 2) ≤
-          1
-    [prop] (match 0 with
-          | 0 => 1
-          | n.succ => 2) =
-          1
-  [eqc] Equivalence classes
-    [eqc] {match 0 with
-        | 0 => 1
-        | n.succ => 2,
-        match x with
-        | 0 => 1
-        | n.succ => 2,
-        1}
-    [eqc] {x, 0}
-  [cases] Case analyses
-    [cases] [1/2]: match x with
-        | 0 => 1
-        | n.succ => 2
-  [ematch] E-matching patterns
-    [thm] _example.match_1.eq_1: [_example.match_1 #2 `[0] #1 #0]
-    [thm] _example.match_1.eq_2: [_example.match_1 #3 (#2 + 1) #1 #0]
-  [offset] Assignment satisfying offset contraints
-    [assign] match x with
-        | 0 => 1
-        | n.succ => 2 := 1
-[grind] Issues
-  [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
-[grind] Counters
-  [thm] E-Matching instances
-    [thm] _example.match_1.eq_1 ↦ 1
-grind_guide.lean:82:19-82:21: warning: declaration uses 'sorry'
-[grind.assert] f a = b
-[grind.assert] a = g c
-[grind.assert] ¬b = c
-[grind.ematch.instance] fg: f (g c) = c
-[grind.assert] f (g c) = c
-grind_guide.lean:100:19-100:25: warning: declaration uses 'sorry'
-grind_guide.lean:101:19-101:24: warning: declaration uses 'sorry'
-[grind.assert] R a b
-[grind.assert] R c b
-[grind.assert] R d c
-[grind.assert] ¬R a d
-[grind.assert] R a d → R d a
-[grind.assert] R d c → R c d
-[grind.assert] R c b → R b c
-[grind.assert] R a b → R b a
-[grind.assert] R a d → R d c → R a c
-[grind.assert] R d c → R c b → R d b
-[grind.assert] R d b → R b d
-[grind.assert] R a c → R c a
-[grind.assert] R b a → R a b
-[grind.assert] R b c → R c b
-[grind.assert] R c d → R d c
-[grind.assert] R d a → R a d
-[grind.assert] R d b → R b c → R d c
-[grind.assert] R d b → R b a → R d a
-grind_guide.lean:114:8-114:14: warning: declaration uses 'sorry'
-[grind.assert] bla a = b
-[grind.assert] ¬bla b = b
-[grind.assert] bla (bla a) = bla a
-grind_guide.lean:137:20-137:30: warning: declaration uses 'sorry'
-grind_guide.lean:144:2-144:12: error: `grind` failed
-case grind
-a b c d : Nat
-a✝² : R a b
-a✝¹ : R c b
-a✝ : R d c
-x✝ : ¬R a d
-⊢ False
-[grind] Diagnostics
-  [facts] Asserted facts
-    [prop] R a b
-    [prop] R c b
-    [prop] R d c
-    [prop] ¬R a d
-  [eqc] True propositions
-    [prop] R a b
-    [prop] R c b
-    [prop] R d c
-  [eqc] False propositions
-    [prop] R a d
-Try this: grind only [→ Rtrans, → Rsymm]
-[grind] Counters
-  [thm] E-Matching instances
-    [thm] Array.get_set_ne ↦ 3
-    [thm] Array.size_set ↦ 3
-[diag] Diagnostics
-  [reduction] unfolded declarations (max: 76, num: 3):
-    [reduction] getElem ↦ 76
-    [reduction] LT.lt ↦ 47
-    [reduction] Nat.lt ↦ 35
-  [reduction] unfolded instances (max: 38, num: 1):
-    [reduction] Array.instGetElemNatLtSize ↦ 38
-  [reduction] unfolded reducible declarations (max: 351, num: 7):
-    [reduction] Array.size ↦ 351
-    [reduction] Array.toList ↦ 212
-    [reduction] outParam ↦ 172
-    [reduction] Ne ↦ 60
-    [reduction] GT.gt ↦ 46
-    [reduction] autoParam ↦ 39
-    [reduction] List.casesOn ↦ 24
-  [kernel] unfolded declarations (max: 106, num: 5):
-    [kernel] LT.lt ↦ 106
-    [kernel] outParam ↦ 46
-    [kernel] Array.size ↦ 36
-    [kernel] Array.toList ↦ 31
-    [kernel] autoParam ↦ 26
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
-grind_guide.lean:266:43-268:7: error: unsolved goals
-case h_1
-b a : Vec Nat (0 + 1)
-n✝¹ : Nat
-v✝ w✝ : Vec Nat n✝¹
-n✝ : Nat
-x✝ : Vec Nat (n✝ + 1 + 1)
-a✝² a✝¹ : Nat
-a✝ : Vec Nat n✝
-heq✝² : 0 + 1 = n✝ + 1 + 1
-heq✝¹ : HEq a x✝
-heq✝ : HEq b (Vec.cons a✝² (Vec.cons a✝¹ a✝))
-⊢ b = Vec.cons 1 Vec.nil → 20 = 40
-
-case h_2
-b a : Vec Nat (0 + 1)
-n✝ : Nat
-v✝ w✝ : Vec Nat n✝
-x✝ : Vec Nat 0
-heq✝² : 0 + 1 = 0
-heq✝¹ : HEq a Vec.nil
-heq✝ : HEq b x✝
-⊢ b = Vec.cons 1 Vec.nil → 30 = 40
-
-case h_3
-n✝ : Nat
-v✝¹ w✝¹ : Vec Nat n✝
-v✝ w✝ : Vec Nat (0 + 1)
-x✝¹ :
-  ∀ (n : Nat) (x : Vec Nat (n + 1 + 1)) (a a_1 : Nat) (a_2 : Vec Nat n),
-    0 + 1 = n + 1 + 1 → HEq v✝ x → HEq w✝ (Vec.cons a (Vec.cons a_1 a_2)) → False
-x✝ : ∀ (x : Vec Nat 0), 0 + 1 = 0 → HEq v✝ Vec.nil → HEq w✝ x → False
-⊢ w✝ = Vec.cons 1 Vec.nil → 40 = 40
-Try this: (induction as, bs using app.induct) <;> grind? [= app]
-grind_guide.lean:287:19-287:25: warning: declaration uses 'sorry'
-grind_guide.lean:290:2-290:7: error: `grind` failed
-case grind
-x : Nat
-x✝ : bomb x ≤ 10
-⊢ False
-[grind] Diagnostics
-  [facts] Asserted facts
-    [prop] bomb x ≤ 10
-    [prop] bomb x = bomb (bomb x) + 1
-    [prop] bomb (bomb x) = bomb (bomb (bomb x)) + 1
-    [prop] bomb (bomb (bomb x)) = bomb (bomb (bomb (bomb x))) + 1
-    [prop] bomb (bomb (bomb (bomb x))) = bomb (bomb (bomb (bomb (bomb x)))) + 1
-    [prop] bomb (bomb (bomb (bomb (bomb x)))) = bomb (bomb (bomb (bomb (bomb (bomb x))))) + 1
-  [eqc] True propositions
-    [prop] bomb x ≤ 10
-  [eqc] Equivalence classes
-    [eqc] {bomb (bomb (bomb (bomb (bomb x)))), bomb (bomb (bomb (bomb (bomb (bomb x))))) + 1}
-    [eqc] {bomb (bomb (bomb (bomb x))), bomb (bomb (bomb (bomb (bomb x)))) + 1}
-    [eqc] {bomb (bomb (bomb x)), bomb (bomb (bomb (bomb x))) + 1}
-    [eqc] {bomb (bomb x), bomb (bomb (bomb x)) + 1}
-    [eqc] {bomb x, bomb (bomb x) + 1}
-  [ematch] E-matching patterns
-    [thm] bombEx: [bomb #0]
-  [offset] Assignment satisfying offset contraints
-    [assign] bomb x := 5
-    [assign] bomb (bomb x) := 4
-    [assign] bomb (bomb (bomb x)) := 3
-    [assign] bomb (bomb (bomb (bomb x))) := 2
-    [assign] bomb (bomb (bomb (bomb (bomb x)))) := 1
-    [assign] bomb (bomb (bomb (bomb (bomb (bomb x))))) := 0
-  [limits] Thresholds reached
-    [limit] maximum number of E-matching rounds has been reached, threshold: `(ematch := 5)`
-    [limit] maximum term generation has been reached, threshold: `(gen := 5)`
-[grind] Counters
-  [thm] E-Matching instances
-    [thm] bombEx ↦ 5

tests/lean/run/grind_ctor_ematch.lean

@@ -17,7 +17,7 @@ example : Even 4 := by
 /--
 error: `grind` failed
 case grind
-x✝ : ¬Even 16
+h : ¬Even 16
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts

tests/lean/run/grind_eq.lean

@@ -65,13 +65,13 @@ theorem appV_assoc (a : Vector α n) (b : Vector α m) (c : Vector α n') :
         HEq (appV a (appV b c)) (appV (appV a b) c) := sorry
 
 /--
-info: [grind.assert] x1 = appV a b
+info: [grind.assert] x1 = appV a_2 b
 [grind.assert] x2 = appV x1 c
 [grind.assert] x3 = appV b c
-[grind.assert] x4 = appV a x3
+[grind.assert] x4 = appV a_2 x3
 [grind.assert] ¬HEq x2 x4
-[grind.ematch.instance] appV_assoc: HEq (appV a (appV b c)) (appV (appV a b) c)
-[grind.assert] HEq (appV a (appV b c)) (appV (appV a b) c)
+[grind.ematch.instance] appV_assoc: HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
+[grind.assert] HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
 -/
 #guard_msgs (info) in
 example : x1 = appV a b → x2 = appV x1 c → x3 = appV b c → x4 = appV a x3 → HEq x2 x4 := by

tests/lean/run/grind_guide.lean

@@ -57,7 +57,8 @@ example : (match x with
 example : (match x with
            | 0 => 1
            | _ + 1 => 2) > 0 := by
-  grind (splits := 0) -- `grind` fails if we don't allow it case-split.
+  fail_if_success grind (splits := 0) -- `grind` fails if we don't allow it case-split.
+  sorry
 
 /-
 `grind` shows you the case-splits performed when it fails.
@@ -65,7 +66,8 @@ example : (match x with
 example : (match x with
            | 0 => 1
            | _ + 1 => 2) > 1 := by
-  grind
+  fail_if_success grind
+  sorry
 
 /-
 `simp` uses theorems as rewriting rules.
@@ -141,7 +143,8 @@ whenever it learns a disequality `t = s` where `t` or `s` E-matches `inv a`
 Like `simp`, we also have `grind only`
 -/
 example : R a b → R c b → R d c → R a d := by
-  grind only -- `Rtrans` and `Rsymm` were not applied
+  fail_if_success grind only -- `Rtrans` and `Rsymm` were not applied
+  sorry
 
 example : R a b → R c b → R d c → R a d := by
   grind only [→ Rtrans, → Rsymm]
@@ -263,11 +266,6 @@ def h (v w : Vec α n) : Nat :=
 example : b = .cons 1 .nil → h a b = 40 := by
   grind [h.eq_def]
 
-example : b = .cons 1 .nil → h a b = 40 := by
-  unfold h
-  split
-
-
 /-
 `try?` tactic is a driver around `grind` (and other tactics).
 It tries many different things (e.g., applies function induction principle for you)
@@ -287,7 +285,8 @@ opaque bomb : Nat → Nat
 @[grind =] theorem bombEx : bomb x = bomb (bomb x) + 1 := sorry
 
 example : bomb x > 10 := by
-  grind
+  fail_if_success grind
+  sorry
 
 /-
 Roadmap:

tests/lean/run/grind_offset_cnstr.lean

@@ -264,15 +264,15 @@ info: theorem ex1 : ∀ {a4 : Nat} (p : Prop) (a1 a2 a3 : Nat),
   (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4 :=
 fun {a4} p a1 a2 a3 =>
   intro_with_eq (p ↔ a2 ≤ a1) (p = (a2 ≤ a1)) (¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4) (iff_eq p (a2 ≤ a1))
-    fun a a_1 a_2 =>
-    intro_with_eq (p ↔ a4 ≤ a3 + 2) (p = (a4 ≤ a3 + 2)) (a1 ≤ a4) (iff_eq p (a4 ≤ a3 + 2)) fun a_3 =>
+    fun h h_1 h_2 =>
+    intro_with_eq (p ↔ a4 ≤ a3 + 2) (p = (a4 ≤ a3 + 2)) (a1 ≤ a4) (iff_eq p (a4 ≤ a3 + 2)) fun h_3 =>
       Classical.byContradiction
-        (intro_with_eq (¬a1 ≤ a4) (a4 + 1 ≤ a1) False (Nat.not_le_eq a1 a4) fun x =>
+        (intro_with_eq (¬a1 ≤ a4) (a4 + 1 ≤ a1) False (Nat.not_le_eq a1 a4) fun h_4 =>
           Eq.mp
-            (Eq.trans (Eq.symm (eq_true x))
+            (Eq.trans (Eq.symm (eq_true h_4))
               (Nat.lo_eq_false_of_lo a1 a4 7 1 rfl_true
-                (Nat.lo_lo a1 a2 a4 1 6 (Nat.of_le_eq_false a2 a1 (Eq.trans (Eq.symm a) (eq_false a_1)))
-                  (Nat.lo_lo a2 a3 a4 3 3 a_2 (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm a_3) (eq_false a_1)))))))
+                (Nat.lo_lo a1 a2 a4 1 6 (Nat.of_le_eq_false a2 a1 (Eq.trans (Eq.symm h) (eq_false h_1)))
+                  (Nat.lo_lo a2 a3 a4 3 3 h_2 (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm h_3) (eq_false h_1)))))))
             True.intro)
 -/
 #guard_msgs (info) in

tests/lean/run/grind_offset_model.lean

@@ -8,7 +8,7 @@ error: `grind` failed
 case grind
 i j : Nat
 h : j + 1 ≤ i
-x✝ : ¬g (i + 1) j = i + 1
+h_1 : ¬g (i + 1) j = i + 1
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
@@ -32,7 +32,7 @@ example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = i + 1 := by
 error: `grind` failed
 case grind
 i : Nat
-x✝ : 101 ≤ i
+h : 101 ≤ i
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
@@ -51,7 +51,7 @@ example (i : Nat) : i ≤ 100 := by
 error: `grind` failed
 case grind
 i : Nat
-x✝ : i ≤ 99
+h : i ≤ 99
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
@@ -70,8 +70,8 @@ example (i : Nat) : 100 ≤ i := by
 error: `grind` failed
 case grind
 n m a j i : Nat
-a✝ : g (n + 1) m = a
-x✝ : i ≤ j + 99
+h : g (n + 1) m = a
+h_1 : i ≤ j + 99
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
@@ -96,8 +96,8 @@ example (i : Nat) : g (n + 1) m = a → 100 + j ≤ i := by
 error: `grind` failed
 case grind
 n m a j i : Nat
-a✝ : g (n + 1) m = a
-x✝ : i + 101 ≤ j
+h : g (n + 1) m = a
+h_1 : i + 101 ≤ j
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts

tests/lean/run/grind_params.lean

@@ -33,8 +33,8 @@ example : P x → R x := by
 error: `grind` failed
 case grind
 x : Nat
-a✝ : P x
-x✝ : ¬R x
+h : P x
+h_1 : ¬R x
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts

tests/lean/run/grind_pre.lean

@@ -8,11 +8,11 @@ error: `grind` failed
 case grind
 a b c : Bool
 p q : Prop
-left✝ : a = true
-right✝ : b = true ∨ c = true
-left : p
-right : q
-x✝ : b = false ∨ a = false
+left : a = true
+right : b = true ∨ c = true
+left_1 : p
+right_1 : q
+h_1 : b = false ∨ a = false
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
@@ -47,11 +47,11 @@ error: `grind` failed
 case grind.2.1
 a b c : Bool
 p q : Prop
-left✝ : a = true
-h✝ : c = true
-left : p
-right : q
-h : b = false
+left : a = true
+h_1 : c = true
+left_1 : p
+right_1 : q
+h_3 : b = false
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
@@ -83,8 +83,8 @@ error: `grind` failed
 case grind
 i j : Nat
 h : j + 1 < i + 1
-h✝ : j + 1 ≤ i
-x✝ : ¬g (i + 1) j ⋯ = i + j + 1
+h_2 : j + 1 ≤ i
+h_3 : ¬g (i + 1) j ⋯ = i + j + 1
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
@@ -124,7 +124,7 @@ b₃ : Int
 head_eq : a₁ = b₁
 x_eq : a₂ = b₂
 y_eq : a₃ = b₃
-tail_eq : as = bs
+tail_eq_1 : as = bs
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
@@ -216,9 +216,9 @@ f : Nat → Bool
 g : Int → Bool
 a : Nat
 b : Int
-a✝¹ : HEq f g
-a✝ : HEq a b
-x✝ : ¬f a = g b
+h : HEq f g
+h_1 : HEq a b
+h_2 : ¬f a = g b
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts

tests/lean/run/grind_split_issue.lean

@@ -9,8 +9,8 @@ case grind.1
 c : Nat
 q : X c 0
 s : Nat
-h✝ : 0 = s
-h : HEq ⋯ ⋯
+h : 0 = s
+h_1 : HEq ⋯ ⋯
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts

tests/lean/run/grind_t1.lean

@@ -242,8 +242,8 @@ example (x y : Bool) : ¬(x = true ↔ y = true) ↔ (¬(x = true) ↔ y = true)
 error: `grind` failed
 case grind
 p q : Prop
-a✝¹ : p = q
-a✝ : p
+h : p = q
+h_1 : p
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
@@ -263,8 +263,8 @@ example (p q : Prop) : (p ↔ q) → p → False := by
 error: `grind` failed
 case grind
 p q : Prop
-a✝¹ : p = q
-a✝ : p
+h : p = q
+h_1 : p
 ⊢ False
 -/
 #guard_msgs (error) in
@@ -276,8 +276,8 @@ example (p q : Prop) : (p ↔ q) → p → False := by
 error: `grind` failed
 case grind
 p q : Prop
-a✝¹ : p = ¬q
-a✝ : p
+h : p = ¬q
+h_1 : p
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
@@ -347,8 +347,8 @@ error: `grind` failed
 case grind
 a : Nat
 b : Bool
-a✝¹ : (if b = true then 10 else 20) = a
-a✝ : b = true
+h : (if b = true then 10 else 20) = a
+h_1 : b = true
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts