diff --git a/src/Init/Grind/Config.lean b/src/Init/Grind/Config.lean
new file mode 100644
index 0000000000..abaa3bd579
--- /dev/null
+++ b/src/Init/Grind/Config.lean
@@ -0,0 +1,216 @@
+/-
+Copyright (c) 2025 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
+-/
+module
+prelude
+public import Init.Core
+public section
+namespace Lean.Grind
+/--
+The configuration for `grind`.
+Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
+-/
+structure Config where
+  /-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
+  trace : Bool := false
+  /-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
+  or for which no patterns can be generated. -/
+  lax : Bool := false
+  /-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
+  and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
+  premises : Bool := false
+  /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
+  splits : Nat := 9
+  /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
+  ematch : Nat := 5
+  /--
+  Maximum term generation.
+  The input goal terms have generation 0. When we instantiate a theorem using a term from generation `n`,
+  the new terms have generation `n+1`. Thus, this parameter limits the length of an instantiation chain. -/
+  gen : Nat := 8
+  /-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
+  instances : Nat := 1000
+  /-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
+  matchEqs : Bool := true
+  /-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
+  splitMatch : Bool := true
+  /-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
+  splitIte : Bool := true
+  /--
+  If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
+  Otherwise, it performs case-splitting only on types marked with `[grind cases]` attribute. -/
+  splitIndPred : Bool := false
+  /--
+  If `splitImp` is `true`, then given an implication `p → q` or `(h : p) → q h`, `grind` splits on `p`
+  if the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
+  -/
+  splitImp : Bool := false
+  /-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/
+  canonHeartbeats : Nat := 1000
+  /-- If `ext` is `true`, `grind` uses extensionality theorems that have been marked with `[grind ext]`. -/
+  ext : Bool := true
+  /-- If `extAll` is `true`, `grind` uses any extensionality theorems available in the environment. -/
+  extAll : Bool := false
+  /--
+  If `etaStruct` is `true`, then for each term `t : S` such that `S` is a structure,
+  and is tagged with `[grind ext]`, `grind` adds the equation `t = ⟨t.1, ..., t.n⟩`
+  which holds by reflexivity. Moreover, the extensionality theorem for `S` is not used.
+  -/
+  etaStruct : Bool := true
+  /--
+  If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
+  on equalities between lambda expressions.
+  -/
+  funext : Bool := true
+  /-- TODO -/
+  lookahead : 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
+  /--
+  If `qlia` is `true`, `grind` may generate counterexamples for integer constraints
+  using rational numbers, and ignoring divisibility constraints.
+  This approach is cheaper but incomplete. -/
+  qlia : Bool := false
+  /--
+  If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
+  See paper "Model-based Theory Combination" for details.
+  -/
+  mbtc : Bool := true
+  /--
+  When set to `true` (default: `true`), local definitions are unfolded during normalization and internalization.
+  In other words, given a local context with an entry `x : t := e`, the free variable `x` is reduced to `e`.
+  Note that this behavior is also available in `simp`, but there its default is `false` because `simp` is not
+  always used as a terminal tactic, and it important to preserve the abstractions introduced by users.
+  Additionally, in `grind` we observed that `zetaDelta` is particularly important when combined with function induction.
+  In such scenarios, the same let-expressions can be introduced by function induction and also by unfolding the
+  corresponding definition. We want to avoid a situation in which `zetaDelta` is not applied to let-declarations
+  introduced by function induction while `zeta` unfolds the definition, causing a mismatch.
+  Finally, note that congruence closure is less effective on terms containing many binders such as
+  `lambda` and `let` expressions.
+  -/
+  zetaDelta := true
+  /--
+  When `true` (default: `true`), performs zeta reduction of let expressions during normalization.
+  That is, `let x := v; e[x]` reduces to `e[v]`. See also `zetaDelta`.
+  -/
+  zeta := true
+  /--
+  When `true` (default: `true`), uses procedure for handling equalities over commutative rings.
+  This solver also support commutative semirings, fields, and normalizer non-commutative rings and
+  semirings.
+  -/
+  ring := true
+  /--
+  Maximum number of steps performed by the `ring` solver.
+  A step is counted whenever one polynomial is used to simplify another.
+  For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
+  used to simplify the second to `-1 * y^3 + x * y`.
+  -/
+  ringSteps := 10000
+  /--
+  When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
+  `CommRing`.
+  -/
+  linarith := true
+  /--
+  When `true` (default: `true`), uses procedure for handling linear integer arithmetic for `Int` and `Nat`.
+  -/
+  cutsat := true
+  /--
+  When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
+  -/
+  ac := true
+  /--
+  Maximum number of steps performed by the `ac` solver.
+  A step is counted whenever one AC equation is used to simplify another.
+  For example, given `ma x z = w` and `max x (max y z) = x`, the first can be
+  used to simplify the second to `max w y = x`.
+  -/
+  acSteps := 1000
+  /--
+  Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
+  the characteristic of a ring.
+  -/
+  exp : Nat := 2^20
+  /--
+  When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
+  -/
+  abstractProof := true
+  /--
+  When `true` (default: `true`), enables the procedure for handling injective functions.
+  In this mode, `grind` takes into account theorems such as:
+  ```
+  @[grind inj] theorem double_inj : Function.Injective double
+  ```
+  -/
+  inj := true
+  /--
+  When `true` (default: `true`), enables the procedure for handling orders that implement
+  at least `Std.IsPreorder`
+  -/
+  order := true
+  /--
+  When `true` (default: `true`), enables the legacy module `offset`. This module will be deleted in
+  the future.
+  -/
+  offset := true
+  deriving Inhabited, BEq
+
+/--
+Configuration for interactive mode.
+We disable `clean := false`.
+-/
+structure ConfigInteractive extends Config where
+  clean := false
+
+/--
+A minimal configuration, with ematching and splitting disabled, and all solver modules turned off.
+`grind` will not do anything in this configuration,
+which can be used a starting point for minimal configurations.
+-/
+-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
+structure NoopConfig extends Config where
+  -- Disable splitting
+  splits := 0
+  -- We don't override the various `splitMatch` / `splitIte` settings separately.
+
+  -- Disable e-matching
+  ematch := 0
+  -- We don't override `matchEqs` separately.
+
+  -- Disable extensionality
+  ext       := false
+  extAll    := false
+  etaStruct := false
+  funext    := false
+
+  -- Disable all solver modules
+  ring      := false
+  linarith  := false
+  cutsat    := false
+  ac        := false
+
+/--
+A `grind` configuration that only uses `cutsat` and splitting.
+
+Note: `cutsat` benefits from some amount of instantiation, e.g. `Nat.max_def`.
+We don't currently have a mechanism to enable only a small set of lemmas.
+-/
+-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
+structure CutsatConfig extends NoopConfig where
+  cutsat := true
+  -- Allow the default number of splits.
+  splits := ({} : Config).splits
+
+/--
+A `grind` configuration that only uses `ring`.
+-/
+-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
+structure GrobnerConfig extends NoopConfig where
+  ring := true
+
+end Lean.Grind
diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index f6e7ee99a0..ec91d16125 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -16,6 +16,16 @@ when selecting patterns.
 -/
 syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)
 
+/-!
+`grind` tactic and related tactics.
+-/
+syntax grindErase    := "-" ident
+/--
+The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
+when selecting patterns.
+-/
+syntax grindParam    := grindErase <|> grindLemma <|> grindLemmaMin
+
 namespace Grind
 declare_syntax_cat grind_filter (behavior := both)
 
@@ -152,6 +162,12 @@ inaccessible names to the given names.
 -/
 syntax (name := next) "next " binderIdent* " => " grindSeq : grind
 
+/--
+`· grindSeq` focuses on the main `grind` goal and tries to solve it using the given
+sequence of `grind` tactics.
+-/
+macro dot:patternIgnore("· " <|> ". ") s:grindSeq : grind => `(grind| next%$dot =>%$dot $s:grindSeq )
+
 /--
 `any_goals tac` applies the tactic `tac` to every goal,
 concatenating the resulting goals for successful tactic applications.
diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index 43edd19e22..5f7dddded5 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -7,227 +7,9 @@ module
 prelude
 public import Init.Core
 public import Init.Grind.Interactive
+public import Init.Grind.Config
 public section
-namespace Lean.Grind
-/--
-The configuration for `grind`.
-Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
--/
-structure Config where
-  /-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
-  trace : Bool := false
-  /-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
-  or for which no patterns can be generated. -/
-  lax : Bool := false
-  /-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
-  and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
-  premises : Bool := false
-  /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
-  splits : Nat := 9
-  /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
-  ematch : Nat := 5
-  /--
-  Maximum term generation.
-  The input goal terms have generation 0. When we instantiate a theorem using a term from generation `n`,
-  the new terms have generation `n+1`. Thus, this parameter limits the length of an instantiation chain. -/
-  gen : Nat := 8
-  /-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
-  instances : Nat := 1000
-  /-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
-  matchEqs : Bool := true
-  /-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
-  splitMatch : Bool := true
-  /-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
-  splitIte : Bool := true
-  /--
-  If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
-  Otherwise, it performs case-splitting only on types marked with `[grind cases]` attribute. -/
-  splitIndPred : Bool := false
-  /--
-  If `splitImp` is `true`, then given an implication `p → q` or `(h : p) → q h`, `grind` splits on `p`
-  if the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
-  -/
-  splitImp : Bool := false
-  /-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/
-  canonHeartbeats : Nat := 1000
-  /-- If `ext` is `true`, `grind` uses extensionality theorems that have been marked with `[grind ext]`. -/
-  ext : Bool := true
-  /-- If `extAll` is `true`, `grind` uses any extensionality theorems available in the environment. -/
-  extAll : Bool := false
-  /--
-  If `etaStruct` is `true`, then for each term `t : S` such that `S` is a structure,
-  and is tagged with `[grind ext]`, `grind` adds the equation `t = ⟨t.1, ..., t.n⟩`
-  which holds by reflexivity. Moreover, the extensionality theorem for `S` is not used.
-  -/
-  etaStruct : Bool := true
-  /--
-  If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
-  on equalities between lambda expressions.
-  -/
-  funext : Bool := true
-  /-- TODO -/
-  lookahead : 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
-  /--
-  If `qlia` is `true`, `grind` may generate counterexamples for integer constraints
-  using rational numbers, and ignoring divisibility constraints.
-  This approach is cheaper but incomplete. -/
-  qlia : Bool := false
-  /--
-  If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
-  See paper "Model-based Theory Combination" for details.
-  -/
-  mbtc : Bool := true
-  /--
-  When set to `true` (default: `true`), local definitions are unfolded during normalization and internalization.
-  In other words, given a local context with an entry `x : t := e`, the free variable `x` is reduced to `e`.
-  Note that this behavior is also available in `simp`, but there its default is `false` because `simp` is not
-  always used as a terminal tactic, and it important to preserve the abstractions introduced by users.
-  Additionally, in `grind` we observed that `zetaDelta` is particularly important when combined with function induction.
-  In such scenarios, the same let-expressions can be introduced by function induction and also by unfolding the
-  corresponding definition. We want to avoid a situation in which `zetaDelta` is not applied to let-declarations
-  introduced by function induction while `zeta` unfolds the definition, causing a mismatch.
-  Finally, note that congruence closure is less effective on terms containing many binders such as
-  `lambda` and `let` expressions.
-  -/
-  zetaDelta := true
-  /--
-  When `true` (default: `true`), performs zeta reduction of let expressions during normalization.
-  That is, `let x := v; e[x]` reduces to `e[v]`. See also `zetaDelta`.
-  -/
-  zeta := true
-  /--
-  When `true` (default: `true`), uses procedure for handling equalities over commutative rings.
-  This solver also support commutative semirings, fields, and normalizer non-commutative rings and
-  semirings.
-  -/
-  ring := true
-  /--
-  Maximum number of steps performed by the `ring` solver.
-  A step is counted whenever one polynomial is used to simplify another.
-  For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
-  used to simplify the second to `-1 * y^3 + x * y`.
-  -/
-  ringSteps := 10000
-  /--
-  When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
-  `CommRing`.
-  -/
-  linarith := true
-  /--
-  When `true` (default: `true`), uses procedure for handling linear integer arithmetic for `Int` and `Nat`.
-  -/
-  cutsat := true
-  /--
-  When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
-  -/
-  ac := true
-  /--
-  Maximum number of steps performed by the `ac` solver.
-  A step is counted whenever one AC equation is used to simplify another.
-  For example, given `ma x z = w` and `max x (max y z) = x`, the first can be
-  used to simplify the second to `max w y = x`.
-  -/
-  acSteps := 1000
-  /--
-  Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
-  the characteristic of a ring.
-  -/
-  exp : Nat := 2^20
-  /--
-  When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
-  -/
-  abstractProof := true
-  /--
-  When `true` (default: `true`), enables the procedure for handling injective functions.
-  In this mode, `grind` takes into account theorems such as:
-  ```
-  @[grind inj] theorem double_inj : Function.Injective double
-  ```
-  -/
-  inj := true
-  /--
-  When `true` (default: `true`), enables the procedure for handling orders that implement
-  at least `Std.IsPreorder`
-  -/
-  order := true
-  /--
-  When `true` (default: `true`), enables the legacy module `offset`. This module will be deleted in
-  the future.
-  -/
-  offset := true
-  deriving Inhabited, BEq
-
-/--
-Configuration for interactive mode.
-We disable `clean := false`.
--/
-structure ConfigInteractive extends Config where
-  clean := false
-
-/--
-A minimal configuration, with ematching and splitting disabled, and all solver modules turned off.
-`grind` will not do anything in this configuration,
-which can be used a starting point for minimal configurations.
--/
--- This is a `structure` rather than `def` so we can use `declare_config_elab`.
-structure NoopConfig extends Config where
-  -- Disable splitting
-  splits := 0
-  -- We don't override the various `splitMatch` / `splitIte` settings separately.
-
-  -- Disable e-matching
-  ematch := 0
-  -- We don't override `matchEqs` separately.
-
-  -- Disable extensionality
-  ext       := false
-  extAll    := false
-  etaStruct := false
-  funext    := false
-
-  -- Disable all solver modules
-  ring      := false
-  linarith  := false
-  cutsat    := false
-  ac        := false
-
-/--
-A `grind` configuration that only uses `cutsat` and splitting.
-
-Note: `cutsat` benefits from some amount of instantiation, e.g. `Nat.max_def`.
-We don't currently have a mechanism to enable only a small set of lemmas.
--/
--- This is a `structure` rather than `def` so we can use `declare_config_elab`.
-structure CutsatConfig extends NoopConfig where
-  cutsat := true
-  -- Allow the default number of splits.
-  splits := ({} : Config).splits
-
-/--
-A `grind` configuration that only uses `ring`.
--/
--- This is a `structure` rather than `def` so we can use `declare_config_elab`.
-structure GrobnerConfig extends NoopConfig where
-  ring := true
-
-end Lean.Grind
-
 namespace Lean.Parser.Tactic
-
-/-!
-`grind` tactic and related tactics.
--/
-syntax grindErase    := "-" ident
-/--
-The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
-when selecting patterns.
--/
-syntax grindParam    := grindErase <|> grindLemma <|> grindLemmaMin
-
 open Parser.Tactic.Grind
 
 /--
diff --git a/src/Lean/Meta/Tactic/Grind/Action.lean b/src/Lean/Meta/Tactic/Grind/Action.lean
index f84ec616f1..d4279e0999 100644
--- a/src/Lean/Meta/Tactic/Grind/Action.lean
+++ b/src/Lean/Meta/Tactic/Grind/Action.lean
@@ -159,17 +159,16 @@ def mkGrindSeq (s : List TGrind) : TSyntax ``Parser.Tactic.Grind.grindSeq :=
 /--
 Given `[t₁, ..., tₙ]`, returns
 ```
-next =>
-  t₁
+· t₁
   ...
   tₙ
 ```
-If the list is empty, it returns `next => done`.
+If the list is empty, it returns `· done`.
 -/
 def mkGrindNext (s : List TGrind) : CoreM TGrind := do
   let s ← if s == [] then pure [← `(grind| done)] else pure s
   let s := mkGrindSeq s
-  `(grind| next => $s:grindSeq)
+  `(grind| · $s:grindSeq)
 
 /--
 Given `[t₁, ..., tₙ]`, returns
@@ -189,8 +188,7 @@ private def mkGrindParen (s : List TGrind) : CoreM TGrind := do
 If tracing is enabled and continuation produced `.closed [t₁, ..., tₙ]`,
 returns the singleton sequence `[t]` where `t` is
 ```
-next =>
-  t₁
+· t₁
   ...
   tₙ
 ```
@@ -205,7 +203,7 @@ def group : Action := fun goal _ kp => do
     return r
 
 /--
-If tracing is enabled and continuation produced `.closed [(next => t₁; ...; tₙ)]`,
+If tracing is enabled and continuation produced `.closed [(next => t₁; ...; tₙ)]` or its variant using `·`
 returns `.close [t₁, ... tₙ]`
 -/
 def ungroup : Action := fun goal _ kp => do
@@ -214,7 +212,9 @@ def ungroup : Action := fun goal _ kp => do
     match r with
     | .closed [tac] =>
       match tac with
-      | `(grind| next => $seq;*) => return .closed <| seq.getElems.toList.map TGrindStep.getTactic
+      | `(grind| next => $seq;*)
+      | `(grind| · $seq;*) =>
+        return .closed <| seq.getElems.toList.map TGrindStep.getTactic
       | _ => return r
     | _ => return r
   else
diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean
index 177801c9a9..470353f3cb 100644
--- a/src/Lean/Meta/Tactic/Grind/Split.lean
+++ b/src/Lean/Meta/Tactic/Grind/Split.lean
@@ -322,6 +322,7 @@ where
 private def isCompressibleSeq (seq : List (TSyntax `grind)) : Bool :=
   seq.all fun tac => match tac with
     | `(grind| next $_* => $_:grindSeq) => false
+    | `(grind| · $_:grindSeq) => false
     | _ => true
 
 /--
diff --git a/tests/lean/run/grind_finish_trace.lean b/tests/lean/run/grind_finish_trace.lean
index f0ebcdd30f..9fd9036f89 100644
--- a/tests/lean/run/grind_finish_trace.lean
+++ b/tests/lean/run/grind_finish_trace.lean
@@ -17,8 +17,8 @@ example {α : Type} [CommRing α] (a b c d e : α) :
 info: Try this:
   [apply] ⏎
     cases #b0f4
-    next => cases #50fc
-    next => cases #50fc <;> lia
+    · cases #50fc
+    · cases #50fc <;> lia
 -/
 #guard_msgs in
 example (p : Nat → Prop) (x y z w : Int) :
@@ -65,14 +65,12 @@ set_option warn.sorry false
 info: Try this:
   [apply] ⏎
     cases #c4b6
-    next =>
-      cases #8c9f
-      next => ring
-      next => sorry
-    next =>
-      cases #8c9f
-      next => ring
-      next => sorry
+    · cases #8c9f
+      · ring
+      · sorry
+    · cases #8c9f
+      · ring
+      · sorry
 -/
 #guard_msgs in
 example {α : Type} [CommRing α] (a b c d e : α) :
@@ -86,8 +84,8 @@ info: Try this:
   [apply] ⏎
     instantiate only [= Nat.min_def]
     cases #7640
-    next => sorry
-    next => lia
+    · sorry
+    · lia
 -/
 #guard_msgs in
 example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
diff --git a/tests/lean/run/grind_indexmap_trace.lean b/tests/lean/run/grind_indexmap_trace.lean
index fedade474e..b48a56d369 100644
--- a/tests/lean/run/grind_indexmap_trace.lean
+++ b/tests/lean/run/grind_indexmap_trace.lean
@@ -149,25 +149,18 @@ info: Try this:
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
     cases #4ed2
-    next =>
-      cases #ffdf
-      next => instantiate only
-      next =>
-        instantiate only
+    · cases #ffdf
+      · instantiate only
+      · instantiate only
         instantiate only [= HashMap.contains_insert]
-    next =>
-      cases #95a0
-      next =>
-        cases #2688
-        next => instantiate only
-        next =>
-          instantiate only
+    · cases #95a0
+      · cases #2688
+        · instantiate only
+        · instantiate only
           instantiate only [= HashMap.contains_insert]
-      next =>
-        cases #ffdf
-        next => instantiate only
-        next =>
-          instantiate only
+      · cases #ffdf
+        · instantiate only
+        · instantiate only
           instantiate only [= HashMap.contains_insert]
 -/
 #guard_msgs in
@@ -181,25 +174,18 @@ info: Try this:
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
     cases #4ed2
-    next =>
-      cases #ffdf
-      next => instantiate only
-      next =>
-        instantiate only
+    · cases #ffdf
+      · instantiate only
+      · instantiate only
         instantiate only [= HashMap.contains_insert]
-    next =>
-      cases #95a0
-      next =>
-        cases #2688
-        next => instantiate only
-        next =>
-          instantiate only
+    · cases #95a0
+      · cases #2688
+        · instantiate only
+        · instantiate only
           instantiate only [= HashMap.contains_insert]
-      next =>
-        cases #ffdf
-        next => instantiate only
-        next =>
-          instantiate only
+      · cases #ffdf
+        · instantiate only
+        · instantiate only
           instantiate only [= HashMap.contains_insert]
 -/
 #guard_msgs in
@@ -240,25 +226,19 @@ info: Try this:
     instantiate only [= mem_indices_of_mem, insert, = getElem_def]
     instantiate only [= getElem?_neg, = getElem?_pos]
     cases #f590
-    next =>
-      cases #ffdf
-      next =>
-        instantiate only
+    · cases #ffdf
+      · instantiate only
         instantiate only [= Array.getElem_set]
-      next =>
-        instantiate only
+      · instantiate only
         instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
-    next =>
-      instantiate only [= mem_indices_of_mem, = getElem_def]
+    · instantiate only [= mem_indices_of_mem, = getElem_def]
       instantiate only [usr getElem_indices_lt]
       instantiate only [size]
       cases #ffdf
-      next =>
-        instantiate only [=_ WF]
+      · instantiate only [=_ WF]
         instantiate only [= getElem?_neg, = getElem?_pos, = Array.getElem_set]
         instantiate only [WF']
-      next =>
-        instantiate only
+      · instantiate only
         instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
 -/
 #guard_msgs in
@@ -300,9 +280,8 @@ info: Try this:
     instantiate only [findIdx, insert, = mem_indices_of_mem]
     instantiate only [= getElem?_neg, = getElem?_pos]
     cases #1bba
-    next => instantiate only [findIdx]
-    next =>
-      instantiate only
+    · instantiate only [findIdx]
+    · instantiate only
       instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
 -/
 #guard_msgs in