diff --git a/src/Init/Grind.lean b/src/Init/Grind.lean
index 5d6bc6d744..68d4b6d4b7 100644
--- a/src/Init/Grind.lean
+++ b/src/Init/Grind.lean
@@ -25,3 +25,4 @@ public import Init.Data.Int.OfNat -- This may not have otherwise been imported,
 public import Init.Grind.AC
 public import Init.Grind.Injective
 public import Init.Grind.Order
+public import Init.Grind.Interactive
diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
new file mode 100644
index 0000000000..b20238845b
--- /dev/null
+++ b/src/Init/Grind/Interactive.lean
@@ -0,0 +1,38 @@
+/-
+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.Tactics
+public meta import Init.Meta
+public section
+namespace Lean.Parser.Tactic.Grind
+
+/-- `grind` is the syntax category for a "grind interactive tactic".
+A `grind` tactic is a program which receives a `grind` goal. -/
+declare_syntax_cat grind (behavior := both)
+
+syntax grindSeq1Indented := sepBy1IndentSemicolon(grind)
+syntax grindSeqBracketed := "{" withoutPosition(sepByIndentSemicolon(grind)) "}"
+syntax grindSeq := grindSeqBracketed <|> grindSeq1Indented
+
+/-- `skip` does nothing. -/
+syntax (name := skip) "skip" : grind
+/-- `lia` linear integer arithmetic. -/
+syntax (name := lia) "lia" : grind
+/-- `ring` (commutative) rings and fields. -/
+syntax (name := ring) "ring" : grind
+/-- `finish` tries to close the current goal using `grind`'s default strategy -/
+syntax (name := finish) "finish" : grind
+
+syntax (name := «have») "have" letDecl : grind
+
+/-- Executes the given tactic block to close the current goal. -/
+syntax (name := nestedTacticCore) "tactic" " => " tacticSeq : grind
+
+/-- `grind` interactive mode -/
+syntax (name := grind) "grind" " => " grindSeq : tactic
+
+end Lean.Parser.Tactic.Grind
diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean
index 4af355de16..a1d7b5495e 100644
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@@ -5,376 +5,5 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Tactics
-public import Lean.Meta.Tactic.Grind.Main
-public import Lean.Meta.Tactic.TryThis
-public import Lean.Elab.Command
-public import Lean.Elab.Tactic.Basic
-public import Lean.Elab.Tactic.Config
-import Lean.Meta.Tactic.Grind.SimpUtil
-import Lean.Elab.MutualDef
-meta import Lean.Meta.Tactic.Grind.Parser
-public section
-namespace Lean.Elab.Tactic
-open Meta
-
-declare_config_elab elabGrindConfig Grind.Config
-declare_config_elab elabCutsatConfig Grind.CutsatConfig
-declare_config_elab elabGrobnerConfig Grind.GrobnerConfig
-
-open Command Term in
-@[builtin_command_elab Lean.Parser.Command.grindPattern]
-def elabGrindPattern : CommandElab := fun stx => do
-  match stx with
-  | `(grind_pattern $thmName:ident => $terms,*) => go thmName terms .global
-  | `(scoped grind_pattern $thmName:ident => $terms,*) => go thmName terms .scoped
-  | `(local grind_pattern $thmName:ident => $terms,*) => go thmName terms .local
-  | _ => throwUnsupportedSyntax
-where
-  go (thmName : TSyntax `ident) (terms : Syntax.TSepArray `term ",") (kind : AttributeKind) : CommandElabM Unit := liftTermElabM do
-    let declName ← resolveGlobalConstNoOverload thmName
-    discard <| addTermInfo thmName (← mkConstWithLevelParams declName)
-    let info ← getConstVal declName
-    forallTelescope info.type fun xs _ => do
-      let patterns ← terms.getElems.mapM fun term => do
-        let pattern ← Term.elabTerm term none
-        synthesizeSyntheticMVarsUsingDefault
-        let pattern ← instantiateMVars pattern
-        let pattern ← Grind.preprocessPattern pattern
-        return pattern.abstract xs
-      Grind.addEMatchTheorem declName xs.size patterns.toList .user kind (minIndexable := false)
-
-open Command in
-@[builtin_command_elab Lean.Parser.resetGrindAttrs]
-def elabResetGrindAttrs : CommandElab := fun _ => liftTermElabM do
-  Grind.resetCasesExt
-  Grind.resetEMatchTheoremsExt
-  Grind.resetInjectiveTheoremsExt
-  -- Remark: we do not reset symbol priorities because we would have to then set
-  -- `[grind symbol 0] Eq` after a `reset_grind_attr%` command.
-  -- Grind.resetSymbolPrioExt
-
-open Command Term in
-@[builtin_command_elab Lean.Parser.Command.initGrindNorm]
-def elabInitGrindNorm : CommandElab := fun stx =>
-  withExporting do  -- should generate public aux decls
-  match stx with
-  | `(init_grind_norm $pre:ident* | $post*) =>
-    Command.liftTermElabM do
-      let pre ← pre.mapM fun id => realizeGlobalConstNoOverloadWithInfo id
-      let post ← post.mapM fun id => realizeGlobalConstNoOverloadWithInfo id
-      -- Creates `Lean.Grind._simp_1` etc.. As we do not use this command in independent modules,
-      -- there is no chance of name conflicts.
-      withDeclNameForAuxNaming `Lean.Grind do
-        Grind.registerNormTheorems pre post
-  | _ => throwUnsupportedSyntax
-
-private def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name) : MetaM Unit := do
-  let minIndexable := false -- TODO: infer it
-  let kinds ← match s.getKindsFor (.decl declName) with
-    | [] => return ()
-    | [k] => pure m!"@{k.toAttribute minIndexable}"
-    | [.eqLhs gen, .eqRhs _]
-    | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute minIndexable}"
-    | ks =>
-      let ks := ks.map fun k => m!"@{k.toAttribute minIndexable}"
-      pure m!"{ks}"
-  logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`"
-
-def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool) : MetaM Grind.Params := do
-  let mut params := params
-  for p in ps do
-    match p with
-    | `(Parser.Tactic.grindParam| - $id:ident) =>
-      let declName ← realizeGlobalConstNoOverloadWithInfo id
-      if let some declName ← Grind.isCasesAttrCandidate? declName false then
-        Grind.ensureNotBuiltinCases declName
-        params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) }
-      else if (← Grind.isInjectiveTheorem declName) then
-        params := { params with inj := params.inj.erase (.decl declName) }
-      else
-        params := { params with ematch := (← params.ematch.eraseDecl declName) }
-    | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) =>
-      params ← processParam params p mod? id (minIndexable := false)
-    | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $id:ident) =>
-      params ← processParam params p mod? id (minIndexable := true)
-    | _ => throwError "unexpected `grind` parameter{indentD p}"
-  return params
-where
-  ensureNoMinIndexable (minIndexable : Bool) : MetaM Unit := do
-    if minIndexable then
-      throwError "redundant modifier `!` in `grind` parameter"
-
-  processParam (params : Grind.Params)
-      (p : TSyntax `Lean.Parser.Tactic.grindParam)
-      (mod? : Option (TSyntax `Lean.Parser.Attr.grindMod))
-      (id : TSyntax `ident)
-      (minIndexable : Bool)
-      : MetaM Grind.Params := do
-    let mut params := params
-    let declName ← try
-      realizeGlobalConstNoOverloadWithInfo id
-    catch err =>
-      if (← resolveLocalName id.getId).isSome then
-        throwErrorAt id "redundant parameter `{id}`, `grind` uses local hypotheses automatically"
-      else
-        throw err
-    let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer
-    match kind with
-    | .ematch .user =>
-      unless only do
-        withRef p <| Grind.throwInvalidUsrModifier
-      ensureNoMinIndexable minIndexable
-      let s ← Grind.getEMatchTheorems
-      let thms := s.find (.decl declName)
-      let thms := thms.filter fun thm => thm.kind == .user
-      if thms.isEmpty then
-        throwErrorAt p "invalid use of `usr` modifier, `{.ofConstName declName}` does not have patterns specified with the command `grind_pattern`"
-      for thm in thms do
-        params := { params with extra := params.extra.push thm }
-    | .ematch kind =>
-      params ← withRef p <| addEMatchTheorem params id declName kind minIndexable
-    | .cases eager =>
-      ensureNoMinIndexable minIndexable
-      withRef p <| Grind.validateCasesAttr declName eager
-      params := { params with casesTypes := params.casesTypes.insert declName eager }
-    | .intro =>
-      if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
-        for ctor in info.ctors do
-          params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
-      else
-        throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
-    | .inj =>
-      let thm ← Grind.mkInjectiveTheorem declName
-      params := { params with inj := params.inj.insert thm }
-    | .ext =>
-      throwError "`[grind ext]` cannot be set using parameters"
-    | .infer =>
-      if let some declName ← Grind.isCasesAttrCandidate? declName false then
-        params := { params with casesTypes := params.casesTypes.insert declName false }
-        if let some info ← isInductivePredicate? declName then
-          -- If it is an inductive predicate,
-          -- we also add the constructors (intro rules) as E-matching rules
-          for ctor in info.ctors do
-            params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
-      else
-        params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
-    | .symbol prio =>
-      ensureNoMinIndexable minIndexable
-      params := { params with symPrios := params.symPrios.insert declName prio }
-    return params
-
-  addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name)
-      (kind : Grind.EMatchTheoremKind)
-      (minIndexable : Bool) (suggest : Bool := false) : MetaM Grind.Params := do
-    let info ← getAsyncConstInfo declName
-    match info.kind with
-    | .thm | .axiom | .ctor =>
-      match kind with
-      | .eqBoth gen =>
-        ensureNoMinIndexable minIndexable
-        let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios
-        let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios
-        if params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
-           params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then
-          warnRedundantEMatchArg params.ematch declName
-        return { params with extra := params.extra.push thm₁ |>.push thm₂ }
-      | _ =>
-        if kind matches .eqLhs _ | .eqRhs _ then
-          ensureNoMinIndexable minIndexable
-        let thm ← if suggest && !Grind.backward.grind.inferPattern.get (← getOptions) then
-          Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true)
-        else
-          Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
-        if params.ematch.containsWithSamePatterns thm.origin thm.patterns then
-          warnRedundantEMatchArg params.ematch declName
-        return { params with extra := params.extra.push thm }
-    | .defn =>
-      if (← isReducible declName) then
-        throwError "`{.ofConstName declName}` is a reducible definition, `grind` automatically unfolds them"
-      if !kind.isEqLhs && !kind.isDefault then
-        throwError "invalid `grind` parameter, `{.ofConstName declName}` is a definition, the only acceptable (and redundant) modifier is '='"
-      ensureNoMinIndexable minIndexable
-      let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
-        | throwError "failed to generate equation theorems for `{.ofConstName declName}`"
-      return { params with extra := params.extra ++ thms.toPArray' }
-    | _ =>
-      throwError "invalid `grind` parameter, `{.ofConstName declName}` is not a theorem, definition, or inductive type"
-
-def mkGrindParams (config : Grind.Config) (only : Bool) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
-  let params ← Grind.mkParams config
-  let ematch ← if only then pure default else Grind.getEMatchTheorems
-  let inj ← if only then pure default else Grind.getInjectiveTheorems
-  let casesTypes ← if only then pure default else Grind.getCasesTypes
-  let params := { params with ematch, casesTypes, inj }
-  let params ← elabGrindParams params ps only
-  trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}"
-  return params
-
-def grind
-    (mvarId : MVarId) (config : Grind.Config)
-    (only : Bool)
-    (ps   :  TSyntaxArray ``Parser.Tactic.grindParam)
-    (fallback : Grind.Fallback) : TacticM Grind.Trace := do
-  mvarId.withContext do
-    let params ← mkGrindParams config only ps
-    let type ← mvarId.getType
-    let mvar' ← mkFreshExprSyntheticOpaqueMVar type
-    let result ← Grind.main mvar'.mvarId! params fallback
-    if result.hasFailed then
-      throwError "`grind` failed\n{← result.toMessageData}"
-    trace[grind.debug.proof] "{← instantiateMVars mvar'}"
-    -- `grind` proofs are often big, if `abstractProof` is true, we create an auxiliary theorem.
-    let e ← if !config.abstractProof then
-      instantiateMVarsProfiling mvar'
-    else if (← isProp type) then
-      mkAuxTheorem type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
-    else
-      let auxName ← Term.mkAuxName `grind
-      mkAuxDefinition auxName type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
-    mvarId.assign e
-    return result.trace
-
-private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit) := do
-  let some fallback := fallback? | return (pure ())
-  let type := mkApp (mkConst ``Grind.GoalM) (mkConst ``Unit)
-  let value ← withLCtx {} {} do Term.elabTermAndSynthesize fallback type
-  let auxDeclName ← if let .const declName _ := value then
-    pure declName
-  else
-    let auxDeclName ← Term.mkAuxName `_grind_fallback
-    let decl := Declaration.defnDecl {
-      name := auxDeclName
-      levelParams := []
-      type, value, hints := .opaque, safety := .safe
-    }
-    modifyEnv (addMeta · auxDeclName)
-    addAndCompile decl
-    pure auxDeclName
-  unsafe evalConst (Grind.GoalM Unit) auxDeclName
-
-def evalGrindCore
-    (ref : Syntax)
-    (config : Grind.Config)
-    (only : Option Syntax)
-    (params : Option (Syntax.TSepArray `Lean.Parser.Tactic.grindParam ","))
-    (fallback? : Option Term)
-    : TacticM Grind.Trace := do
-  let fallback ← elabFallback fallback?
-  let only := only.isSome
-  let params := if let some params := params then params.getElems else #[]
-  if Grind.grind.warning.get (← getOptions) then
-    logWarningAt ref "The `grind` tactic is new and its behavior may change in the future. This project has used `set_option grind.warning true` to discourage its use."
-  withMainContext do
-    let result ← grind (← getMainGoal) config only params fallback
-    replaceMainGoal []
-    return result
-
-/-- Position for the `[..]` child syntax in the `grind` tactic. -/
-def grindParamsPos := 3
-
-/-- Position for the `only` child syntax in the `grind` tactic. -/
-def grindOnlyPos := 2
-
-def isGrindOnly (stx : TSyntax `tactic) : Bool :=
-  stx.raw.getKind == ``Parser.Tactic.grind && !stx.raw[grindOnlyPos].isNone
-
-def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `tactic :=
-  if params.isEmpty then
-    ⟨stx.raw.setArg grindParamsPos (mkNullNode)⟩
-  else
-    let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
-    ⟨stx.raw.setArg grindParamsPos (mkNullNode paramsStx)⟩
-
-def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
-  stx.raw[grindParamsPos][1].getSepArgs
-
-def mkGrindOnly
-    (config : TSyntax ``Lean.Parser.Tactic.optConfig)
-    (fallback? : Option Term)
-    (trace : Grind.Trace)
-    : MetaM (TSyntax `tactic) := do
-  let mut params := #[]
-  let mut foundFns : NameSet := {}
-  for { origin, kind, minIndexable } in trace.thms.toList do
-    if let .decl declName := origin then
-      if let some declName ← isEqnThm? declName then
-        unless foundFns.contains declName do
-          foundFns := foundFns.insert declName
-          let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
-          let param ← `(Parser.Tactic.grindParam| $decl:ident)
-          params := params.push param
-      else
-        let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
-        let param ← match kind, minIndexable with
-          | .eqLhs false,   _     => `(Parser.Tactic.grindParam| = $decl:ident)
-          | .eqLhs true,    _     => `(Parser.Tactic.grindParam| = gen $decl:ident)
-          | .eqRhs false,   _     => `(Parser.Tactic.grindParam| =_ $decl:ident)
-          | .eqRhs true,    _     => `(Parser.Tactic.grindParam| =_ gen $decl:ident)
-          | .eqBoth false,  _     => `(Parser.Tactic.grindParam| _=_ $decl:ident)
-          | .eqBoth true,   _     => `(Parser.Tactic.grindParam| _=_ gen $decl:ident)
-          | .eqBwd,         _     => `(Parser.Tactic.grindParam| ←= $decl:ident)
-          | .user,          _     => `(Parser.Tactic.grindParam| usr $decl:ident)
-          | .bwd false,     false => `(Parser.Tactic.grindParam| ← $decl:ident)
-          | .bwd true,      false => `(Parser.Tactic.grindParam| ← gen $decl:ident)
-          | .fwd,           false => `(Parser.Tactic.grindParam| → $decl:ident)
-          | .leftRight,     false => `(Parser.Tactic.grindParam| => $decl:ident)
-          | .rightLeft,     false => `(Parser.Tactic.grindParam| <= $decl:ident)
-          | .default false, false => `(Parser.Tactic.grindParam| $decl:ident)
-          | .default true,  false => `(Parser.Tactic.grindParam| gen $decl:ident)
-          | .bwd false,     true  => `(Parser.Tactic.grindParam| ! ← $decl:ident)
-          | .bwd true,      true  => `(Parser.Tactic.grindParam| ! ← gen $decl:ident)
-          | .fwd,           true  => `(Parser.Tactic.grindParam| ! → $decl:ident)
-          | .leftRight,     true  => `(Parser.Tactic.grindParam| ! => $decl:ident)
-          | .rightLeft,     true  => `(Parser.Tactic.grindParam| ! <= $decl:ident)
-          | .default false, true  => `(Parser.Tactic.grindParam| ! $decl:ident)
-          | .default true,  true  => `(Parser.Tactic.grindParam| ! gen $decl:ident)
-        params := params.push param
-  for declName in trace.eagerCases.toList do
-    unless Grind.isBuiltinEagerCases declName do
-      let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
-      let param ← `(Parser.Tactic.grindParam| cases eager $decl)
-      params := params.push param
-  for declName in trace.cases.toList do
-    unless trace.eagerCases.contains declName || Grind.isBuiltinEagerCases declName do
-      let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
-      let param ← `(Parser.Tactic.grindParam| cases $decl)
-      params := params.push param
-  let result ← if let some fallback := fallback? then
-    `(tactic| grind $config:optConfig only on_failure $fallback)
-  else
-    `(tactic| grind $config:optConfig only)
-  return setGrindParams result params
-
-@[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
-  match stx with
-  | `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
-    let config ← elabGrindConfig config
-    discard <| evalGrindCore stx config only params fallback?
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic Lean.Parser.Tactic.grindTrace] def evalGrindTrace : Tactic := fun stx => do
-  match stx with
-  | `(tactic| grind?%$tk $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
-    let config ← elabGrindConfig configStx
-    let config := { config with trace := true }
-    let trace ← evalGrindCore stx config only params fallback?
-    let stx ← mkGrindOnly configStx fallback? trace
-    Tactic.TryThis.addSuggestion tk stx (origSpan? := ← getRef)
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic Lean.Parser.Tactic.cutsat] def evalCutsat : Tactic := fun stx => do
-  match stx with
-  | `(tactic| cutsat $config:optConfig) =>
-    let config ← elabCutsatConfig config
-    discard <| evalGrindCore stx { config with } none none none
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic Lean.Parser.Tactic.grobner] def evalGrobner : Tactic := fun stx => do
-  match stx with
-  | `(tactic| grobner $config:optConfig) =>
-    let config ← elabGrobnerConfig config
-    discard <| evalGrindCore stx { config with } none none none
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic
+public import Lean.Elab.Tactic.Grind.Main
+public import Lean.Elab.Tactic.Grind.Basic
diff --git a/src/Lean/Elab/Tactic/Grind/Basic.lean b/src/Lean/Elab/Tactic/Grind/Basic.lean
new file mode 100644
index 0000000000..aaed1ec4af
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Grind/Basic.lean
@@ -0,0 +1,273 @@
+/-
+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 Lean.Elab.Term
+public import Lean.Elab.Tactic.Basic
+public import Lean.Meta.Tactic.Grind.Types
+public section
+namespace Lean.Elab.Tactic.Grind
+open Meta
+
+structure Context extends Tactic.Context where
+  ctx    : Grind.Context
+  methods: Grind.Methods
+
+open Meta.Grind (Goal)
+
+structure State where
+  state : Grind.State
+  goals : List Goal
+
+structure SavedState where
+  term   : Term.SavedState
+  tactic : State
+
+abbrev GrindTacticM := ReaderT Context $ StateRefT State TermElabM
+
+abbrev GrindTactic  := Syntax → GrindTacticM Unit
+
+/-- Returns the list of goals. Goals may or may not already be assigned. -/
+def getGoals : GrindTacticM (List Goal) :=
+  return (← get).goals
+
+def setGoals (goals : List Goal) : GrindTacticM Unit :=
+  modify fun s => { s with goals }
+
+def pruneSolvedGoals : GrindTacticM Unit := do
+  let gs ← getGoals
+  let gs := gs.filter fun g => !g.inconsistent
+  setGoals gs
+
+def getUnsolvedGoals : GrindTacticM (List Goal) := do
+  pruneSolvedGoals
+  getGoals
+
+def getUnsolvedGoalMVarIds : GrindTacticM (List MVarId) := do
+  pruneSolvedGoals
+  let goals ← getGoals
+  return goals.map (·.mvarId)
+
+protected def saveState : GrindTacticM SavedState :=
+  return { term := (← Term.saveState), tactic := (← get) }
+
+def SavedState.restore (b : SavedState) (restoreInfo := false) : GrindTacticM Unit := do
+  b.term.restore restoreInfo
+  set b.tactic
+
+@[always_inline]
+instance : Monad GrindTacticM :=
+  let i := inferInstanceAs (Monad GrindTacticM)
+  { pure := i.pure, bind := i.bind }
+
+instance : Inhabited (GrindTacticM α) where
+  default := fun _ _ => default
+
+unsafe builtin_initialize grindTacElabAttribute : KeyedDeclsAttribute GrindTactic ←
+  mkElabAttribute GrindTactic `builtin_grind_tactic `grind_tactic
+    `Lean.Parser.Tactic.Grind `Lean.Elab.Tactic.Grind.GrindTactic "grind"
+
+def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : GrindTacticM Info :=
+  return Info.ofTacticInfo {
+    elaborator    := (← read).elaborator
+    mctxBefore    := mctxBefore
+    goalsBefore   := goalsBefore
+    stx           := stx
+    mctxAfter     := (← getMCtx)
+    goalsAfter    := (← getUnsolvedGoalMVarIds)
+  }
+
+def mkInitialTacticInfo (stx : Syntax) : GrindTacticM (GrindTacticM Info) := do
+  let mctxBefore  ← getMCtx
+  let goalsBefore ← getUnsolvedGoalMVarIds
+  return mkTacticInfo mctxBefore goalsBefore stx
+
+@[inline] def withTacticInfoContext (stx : Syntax) (x : GrindTacticM α) : GrindTacticM α := do
+  withInfoContext x (← mkInitialTacticInfo stx)
+
+structure EvalTacticFailure where
+  exception : Exception
+  state     : SavedState
+
+partial def evalGrindTactic (stx : Syntax) : GrindTacticM Unit := do
+  checkSystem "grind tactic execution"
+  profileitM Exception "grind tactic execution" (decl := stx.getKind) (← getOptions) <|
+  withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with
+    | .node _ k _    =>
+      if k == nullKind then
+        Term.withoutTacticIncrementality true <| withTacticInfoContext stx do
+          stx.getArgs.forM evalGrindTactic
+      else withTraceNode `Elab.step (fun _ => return stx) (tag := stx.getKind.toString) do
+        let evalFns := grindTacElabAttribute.getEntries (← getEnv) stx.getKind
+        let macros  := macroAttribute.getEntries (← getEnv) stx.getKind
+        if evalFns.isEmpty && macros.isEmpty then
+          throwErrorAt stx "Grind tactic `{stx.getKind}` has not been implemented"
+        let s ← Grind.saveState
+        expandEval s macros evalFns #[]
+    | .missing => pure ()
+    | _ => throwError m!"Unexpected grind tactic{indentD stx}"
+where
+    throwExs (failures : Array EvalTacticFailure) : GrindTacticM Unit := do
+     if h : 0 < failures.size  then
+       -- For macros we want to report the error from the first registered / last tried rule (#3770)
+       let fail := failures[failures.size - 1]
+       fail.state.restore (restoreInfo := true)
+       throw fail.exception
+     else
+       throwErrorAt stx "Unexpected syntax{indentD stx}"
+
+    @[inline] handleEx (s : SavedState) (failures : Array EvalTacticFailure) (ex : Exception) (k : Array EvalTacticFailure → GrindTacticM Unit) := do
+      match ex with
+      | .error .. =>
+        trace[Elab.tactic.backtrack] ex.toMessageData
+        let failures := failures.push ⟨ex, ← Grind.saveState⟩
+        s.restore (restoreInfo := true); k failures
+      | .internal id _ =>
+        if id == unsupportedSyntaxExceptionId then
+          -- We do not store `unsupportedSyntaxExceptionId`, see throwExs
+          s.restore (restoreInfo := true); k failures
+        else if id == abortTacticExceptionId then
+          for msg in (← Core.getMessageLog).toList do
+            trace[Elab.tactic.backtrack] msg.data
+          let failures := failures.push ⟨ex, ← Grind.saveState⟩
+          s.restore (restoreInfo := true); k failures
+        else
+          throw ex -- (*)
+
+    expandEval (s : SavedState) (macros : List _) (evalFns : List _)
+        (failures : Array EvalTacticFailure) : GrindTacticM Unit :=
+      match macros with
+      | [] => eval s evalFns failures
+      | m :: ms =>
+        try
+          withReader ({ · with elaborator := m.declName }) do
+            withTacticInfoContext stx do
+              let stx' ← adaptMacro m.value stx
+              evalGrindTactic stx'
+        catch ex => handleEx s failures ex (expandEval s ms evalFns)
+
+    eval (s : SavedState) (evalFns : List _) (failures : Array EvalTacticFailure) : GrindTacticM Unit := do
+      match evalFns with
+      | []              => throwExs failures
+      | evalFn::evalFns => do
+        try
+          Term.withoutTacticIncrementality true do
+          withReader ({ · with elaborator := evalFn.declName }) do
+          withTacticInfoContext stx do
+            evalFn.value stx
+        catch ex => handleEx s failures ex (eval s evalFns)
+
+def throwNoGoalsToBeSolved : GrindTacticM α :=
+  throwError "No goals to be solved"
+
+def done : GrindTacticM Unit := do
+  let gs ← getUnsolvedGoalMVarIds
+  unless gs.isEmpty do
+    Term.reportUnsolvedGoals gs
+    throwAbortTactic
+
+instance : MonadBacktrack SavedState GrindTacticM where
+  saveState := Grind.saveState
+  restoreState b := b.restore
+
+/--
+Non-backtracking `try`/`catch`.
+-/
+@[inline] protected def tryCatch {α} (x : GrindTacticM α) (h : Exception → GrindTacticM α) : GrindTacticM α := do
+  try x catch ex => h ex
+
+/--
+Backtracking `try`/`catch`. This is used for the `MonadExcept` instance for `GrindTacticM`.
+-/
+@[inline] protected def tryCatchRestore {α} (x : GrindTacticM α) (h : Exception → GrindTacticM α)
+    : GrindTacticM α := do
+  let b ← saveState
+  try x catch ex => b.restore; h ex
+
+instance : MonadExcept Exception GrindTacticM where
+  throw    := throw
+  tryCatch := Grind.tryCatchRestore
+
+/-- Execute `x` with error recovery disabled -/
+def withoutRecover (x : GrindTacticM α) : GrindTacticM α :=
+  withReader (fun ctx => { ctx with recover := false }) x
+
+/--
+Like `throwErrorAt`, but, if recovery is enabled, logs the error instead.
+-/
+def throwOrLogErrorAt (ref : Syntax) (msg : MessageData) : GrindTacticM Unit := do
+  if (← read).recover then
+    logErrorAt ref msg
+  else
+    throwErrorAt ref msg
+
+/--
+Like `throwError`, but, if recovery is enabled, logs the error instead.
+-/
+def throwOrLogError (msg : MessageData) : GrindTacticM Unit := do
+  throwOrLogErrorAt (← getRef) msg
+
+@[inline] protected def orElse (x : GrindTacticM α) (y : Unit → GrindTacticM α) : GrindTacticM α := do
+  try withoutRecover x catch _ => y ()
+
+instance : OrElse (GrindTacticM α) where
+  orElse := Grind.orElse
+
+instance : Alternative GrindTacticM where
+  failure := fun {_} => throwError "Failed"
+  orElse  := Grind.orElse
+
+/--
+Save the current tactic state for a token `stx`.
+This method is a no-op if `stx` has no position information.
+We use this method to save the tactic state at punctuation such as `;`
+-/
+def saveTacticInfoForToken (stx : Syntax) : GrindTacticM Unit := do
+  unless stx.getPos?.isNone do
+    withTacticInfoContext stx (pure ())
+
+/-- Elaborate `x` with `stx` on the macro stack -/
+@[inline]
+def withMacroExpansion (beforeStx afterStx : Syntax) (x : GrindTacticM α) : GrindTacticM α :=
+  withMacroExpansionInfo beforeStx afterStx do
+    withTheReader Term.Context (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
+
+/-- Adapt a syntax transformation to a regular tactic evaluator. -/
+def adaptExpander (exp : Syntax → GrindTacticM Syntax) : GrindTactic := fun stx => do
+  let stx' ← exp stx
+  withMacroExpansion stx stx' <| evalGrindTactic stx'
+
+/-- Return the first goal. -/
+def getMainGoal : GrindTacticM Goal := do
+  loop (← getGoals)
+where
+  loop : List Goal → GrindTacticM Goal
+    | [] => throwNoGoalsToBeSolved
+    | goal :: goals => do
+      if goal.inconsistent then
+        loop goals
+      else
+        setGoals (goal :: goals)
+        return goal
+
+/-- Execute `x` using the main goal local context and instances -/
+def withMainContext (x : GrindTacticM α) : GrindTacticM α := do
+  (← getMainGoal).mvarId.withContext x
+
+def tryTactic? (tac : GrindTacticM α) : GrindTacticM (Option α) := do
+  try
+    pure (some (← tac))
+  catch _ =>
+    pure none
+
+def tryTactic (tac : GrindTacticM α) : GrindTacticM Bool := do
+  try
+    discard tac
+    pure true
+  catch _ =>
+    pure false
+
+end Lean.Elab.Tactic.Grind
diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean
new file mode 100644
index 0000000000..4af355de16
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Grind/Main.lean
@@ -0,0 +1,380 @@
+/-
+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
+-/
+module
+prelude
+public import Init.Grind.Tactics
+public import Lean.Meta.Tactic.Grind.Main
+public import Lean.Meta.Tactic.TryThis
+public import Lean.Elab.Command
+public import Lean.Elab.Tactic.Basic
+public import Lean.Elab.Tactic.Config
+import Lean.Meta.Tactic.Grind.SimpUtil
+import Lean.Elab.MutualDef
+meta import Lean.Meta.Tactic.Grind.Parser
+public section
+namespace Lean.Elab.Tactic
+open Meta
+
+declare_config_elab elabGrindConfig Grind.Config
+declare_config_elab elabCutsatConfig Grind.CutsatConfig
+declare_config_elab elabGrobnerConfig Grind.GrobnerConfig
+
+open Command Term in
+@[builtin_command_elab Lean.Parser.Command.grindPattern]
+def elabGrindPattern : CommandElab := fun stx => do
+  match stx with
+  | `(grind_pattern $thmName:ident => $terms,*) => go thmName terms .global
+  | `(scoped grind_pattern $thmName:ident => $terms,*) => go thmName terms .scoped
+  | `(local grind_pattern $thmName:ident => $terms,*) => go thmName terms .local
+  | _ => throwUnsupportedSyntax
+where
+  go (thmName : TSyntax `ident) (terms : Syntax.TSepArray `term ",") (kind : AttributeKind) : CommandElabM Unit := liftTermElabM do
+    let declName ← resolveGlobalConstNoOverload thmName
+    discard <| addTermInfo thmName (← mkConstWithLevelParams declName)
+    let info ← getConstVal declName
+    forallTelescope info.type fun xs _ => do
+      let patterns ← terms.getElems.mapM fun term => do
+        let pattern ← Term.elabTerm term none
+        synthesizeSyntheticMVarsUsingDefault
+        let pattern ← instantiateMVars pattern
+        let pattern ← Grind.preprocessPattern pattern
+        return pattern.abstract xs
+      Grind.addEMatchTheorem declName xs.size patterns.toList .user kind (minIndexable := false)
+
+open Command in
+@[builtin_command_elab Lean.Parser.resetGrindAttrs]
+def elabResetGrindAttrs : CommandElab := fun _ => liftTermElabM do
+  Grind.resetCasesExt
+  Grind.resetEMatchTheoremsExt
+  Grind.resetInjectiveTheoremsExt
+  -- Remark: we do not reset symbol priorities because we would have to then set
+  -- `[grind symbol 0] Eq` after a `reset_grind_attr%` command.
+  -- Grind.resetSymbolPrioExt
+
+open Command Term in
+@[builtin_command_elab Lean.Parser.Command.initGrindNorm]
+def elabInitGrindNorm : CommandElab := fun stx =>
+  withExporting do  -- should generate public aux decls
+  match stx with
+  | `(init_grind_norm $pre:ident* | $post*) =>
+    Command.liftTermElabM do
+      let pre ← pre.mapM fun id => realizeGlobalConstNoOverloadWithInfo id
+      let post ← post.mapM fun id => realizeGlobalConstNoOverloadWithInfo id
+      -- Creates `Lean.Grind._simp_1` etc.. As we do not use this command in independent modules,
+      -- there is no chance of name conflicts.
+      withDeclNameForAuxNaming `Lean.Grind do
+        Grind.registerNormTheorems pre post
+  | _ => throwUnsupportedSyntax
+
+private def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name) : MetaM Unit := do
+  let minIndexable := false -- TODO: infer it
+  let kinds ← match s.getKindsFor (.decl declName) with
+    | [] => return ()
+    | [k] => pure m!"@{k.toAttribute minIndexable}"
+    | [.eqLhs gen, .eqRhs _]
+    | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute minIndexable}"
+    | ks =>
+      let ks := ks.map fun k => m!"@{k.toAttribute minIndexable}"
+      pure m!"{ks}"
+  logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`"
+
+def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool) : MetaM Grind.Params := do
+  let mut params := params
+  for p in ps do
+    match p with
+    | `(Parser.Tactic.grindParam| - $id:ident) =>
+      let declName ← realizeGlobalConstNoOverloadWithInfo id
+      if let some declName ← Grind.isCasesAttrCandidate? declName false then
+        Grind.ensureNotBuiltinCases declName
+        params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) }
+      else if (← Grind.isInjectiveTheorem declName) then
+        params := { params with inj := params.inj.erase (.decl declName) }
+      else
+        params := { params with ematch := (← params.ematch.eraseDecl declName) }
+    | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) =>
+      params ← processParam params p mod? id (minIndexable := false)
+    | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $id:ident) =>
+      params ← processParam params p mod? id (minIndexable := true)
+    | _ => throwError "unexpected `grind` parameter{indentD p}"
+  return params
+where
+  ensureNoMinIndexable (minIndexable : Bool) : MetaM Unit := do
+    if minIndexable then
+      throwError "redundant modifier `!` in `grind` parameter"
+
+  processParam (params : Grind.Params)
+      (p : TSyntax `Lean.Parser.Tactic.grindParam)
+      (mod? : Option (TSyntax `Lean.Parser.Attr.grindMod))
+      (id : TSyntax `ident)
+      (minIndexable : Bool)
+      : MetaM Grind.Params := do
+    let mut params := params
+    let declName ← try
+      realizeGlobalConstNoOverloadWithInfo id
+    catch err =>
+      if (← resolveLocalName id.getId).isSome then
+        throwErrorAt id "redundant parameter `{id}`, `grind` uses local hypotheses automatically"
+      else
+        throw err
+    let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer
+    match kind with
+    | .ematch .user =>
+      unless only do
+        withRef p <| Grind.throwInvalidUsrModifier
+      ensureNoMinIndexable minIndexable
+      let s ← Grind.getEMatchTheorems
+      let thms := s.find (.decl declName)
+      let thms := thms.filter fun thm => thm.kind == .user
+      if thms.isEmpty then
+        throwErrorAt p "invalid use of `usr` modifier, `{.ofConstName declName}` does not have patterns specified with the command `grind_pattern`"
+      for thm in thms do
+        params := { params with extra := params.extra.push thm }
+    | .ematch kind =>
+      params ← withRef p <| addEMatchTheorem params id declName kind minIndexable
+    | .cases eager =>
+      ensureNoMinIndexable minIndexable
+      withRef p <| Grind.validateCasesAttr declName eager
+      params := { params with casesTypes := params.casesTypes.insert declName eager }
+    | .intro =>
+      if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
+        for ctor in info.ctors do
+          params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
+      else
+        throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
+    | .inj =>
+      let thm ← Grind.mkInjectiveTheorem declName
+      params := { params with inj := params.inj.insert thm }
+    | .ext =>
+      throwError "`[grind ext]` cannot be set using parameters"
+    | .infer =>
+      if let some declName ← Grind.isCasesAttrCandidate? declName false then
+        params := { params with casesTypes := params.casesTypes.insert declName false }
+        if let some info ← isInductivePredicate? declName then
+          -- If it is an inductive predicate,
+          -- we also add the constructors (intro rules) as E-matching rules
+          for ctor in info.ctors do
+            params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
+      else
+        params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
+    | .symbol prio =>
+      ensureNoMinIndexable minIndexable
+      params := { params with symPrios := params.symPrios.insert declName prio }
+    return params
+
+  addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name)
+      (kind : Grind.EMatchTheoremKind)
+      (minIndexable : Bool) (suggest : Bool := false) : MetaM Grind.Params := do
+    let info ← getAsyncConstInfo declName
+    match info.kind with
+    | .thm | .axiom | .ctor =>
+      match kind with
+      | .eqBoth gen =>
+        ensureNoMinIndexable minIndexable
+        let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios
+        let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios
+        if params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
+           params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then
+          warnRedundantEMatchArg params.ematch declName
+        return { params with extra := params.extra.push thm₁ |>.push thm₂ }
+      | _ =>
+        if kind matches .eqLhs _ | .eqRhs _ then
+          ensureNoMinIndexable minIndexable
+        let thm ← if suggest && !Grind.backward.grind.inferPattern.get (← getOptions) then
+          Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true)
+        else
+          Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
+        if params.ematch.containsWithSamePatterns thm.origin thm.patterns then
+          warnRedundantEMatchArg params.ematch declName
+        return { params with extra := params.extra.push thm }
+    | .defn =>
+      if (← isReducible declName) then
+        throwError "`{.ofConstName declName}` is a reducible definition, `grind` automatically unfolds them"
+      if !kind.isEqLhs && !kind.isDefault then
+        throwError "invalid `grind` parameter, `{.ofConstName declName}` is a definition, the only acceptable (and redundant) modifier is '='"
+      ensureNoMinIndexable minIndexable
+      let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
+        | throwError "failed to generate equation theorems for `{.ofConstName declName}`"
+      return { params with extra := params.extra ++ thms.toPArray' }
+    | _ =>
+      throwError "invalid `grind` parameter, `{.ofConstName declName}` is not a theorem, definition, or inductive type"
+
+def mkGrindParams (config : Grind.Config) (only : Bool) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
+  let params ← Grind.mkParams config
+  let ematch ← if only then pure default else Grind.getEMatchTheorems
+  let inj ← if only then pure default else Grind.getInjectiveTheorems
+  let casesTypes ← if only then pure default else Grind.getCasesTypes
+  let params := { params with ematch, casesTypes, inj }
+  let params ← elabGrindParams params ps only
+  trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}"
+  return params
+
+def grind
+    (mvarId : MVarId) (config : Grind.Config)
+    (only : Bool)
+    (ps   :  TSyntaxArray ``Parser.Tactic.grindParam)
+    (fallback : Grind.Fallback) : TacticM Grind.Trace := do
+  mvarId.withContext do
+    let params ← mkGrindParams config only ps
+    let type ← mvarId.getType
+    let mvar' ← mkFreshExprSyntheticOpaqueMVar type
+    let result ← Grind.main mvar'.mvarId! params fallback
+    if result.hasFailed then
+      throwError "`grind` failed\n{← result.toMessageData}"
+    trace[grind.debug.proof] "{← instantiateMVars mvar'}"
+    -- `grind` proofs are often big, if `abstractProof` is true, we create an auxiliary theorem.
+    let e ← if !config.abstractProof then
+      instantiateMVarsProfiling mvar'
+    else if (← isProp type) then
+      mkAuxTheorem type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
+    else
+      let auxName ← Term.mkAuxName `grind
+      mkAuxDefinition auxName type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
+    mvarId.assign e
+    return result.trace
+
+private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit) := do
+  let some fallback := fallback? | return (pure ())
+  let type := mkApp (mkConst ``Grind.GoalM) (mkConst ``Unit)
+  let value ← withLCtx {} {} do Term.elabTermAndSynthesize fallback type
+  let auxDeclName ← if let .const declName _ := value then
+    pure declName
+  else
+    let auxDeclName ← Term.mkAuxName `_grind_fallback
+    let decl := Declaration.defnDecl {
+      name := auxDeclName
+      levelParams := []
+      type, value, hints := .opaque, safety := .safe
+    }
+    modifyEnv (addMeta · auxDeclName)
+    addAndCompile decl
+    pure auxDeclName
+  unsafe evalConst (Grind.GoalM Unit) auxDeclName
+
+def evalGrindCore
+    (ref : Syntax)
+    (config : Grind.Config)
+    (only : Option Syntax)
+    (params : Option (Syntax.TSepArray `Lean.Parser.Tactic.grindParam ","))
+    (fallback? : Option Term)
+    : TacticM Grind.Trace := do
+  let fallback ← elabFallback fallback?
+  let only := only.isSome
+  let params := if let some params := params then params.getElems else #[]
+  if Grind.grind.warning.get (← getOptions) then
+    logWarningAt ref "The `grind` tactic is new and its behavior may change in the future. This project has used `set_option grind.warning true` to discourage its use."
+  withMainContext do
+    let result ← grind (← getMainGoal) config only params fallback
+    replaceMainGoal []
+    return result
+
+/-- Position for the `[..]` child syntax in the `grind` tactic. -/
+def grindParamsPos := 3
+
+/-- Position for the `only` child syntax in the `grind` tactic. -/
+def grindOnlyPos := 2
+
+def isGrindOnly (stx : TSyntax `tactic) : Bool :=
+  stx.raw.getKind == ``Parser.Tactic.grind && !stx.raw[grindOnlyPos].isNone
+
+def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `tactic :=
+  if params.isEmpty then
+    ⟨stx.raw.setArg grindParamsPos (mkNullNode)⟩
+  else
+    let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
+    ⟨stx.raw.setArg grindParamsPos (mkNullNode paramsStx)⟩
+
+def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
+  stx.raw[grindParamsPos][1].getSepArgs
+
+def mkGrindOnly
+    (config : TSyntax ``Lean.Parser.Tactic.optConfig)
+    (fallback? : Option Term)
+    (trace : Grind.Trace)
+    : MetaM (TSyntax `tactic) := do
+  let mut params := #[]
+  let mut foundFns : NameSet := {}
+  for { origin, kind, minIndexable } in trace.thms.toList do
+    if let .decl declName := origin then
+      if let some declName ← isEqnThm? declName then
+        unless foundFns.contains declName do
+          foundFns := foundFns.insert declName
+          let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+          let param ← `(Parser.Tactic.grindParam| $decl:ident)
+          params := params.push param
+      else
+        let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+        let param ← match kind, minIndexable with
+          | .eqLhs false,   _     => `(Parser.Tactic.grindParam| = $decl:ident)
+          | .eqLhs true,    _     => `(Parser.Tactic.grindParam| = gen $decl:ident)
+          | .eqRhs false,   _     => `(Parser.Tactic.grindParam| =_ $decl:ident)
+          | .eqRhs true,    _     => `(Parser.Tactic.grindParam| =_ gen $decl:ident)
+          | .eqBoth false,  _     => `(Parser.Tactic.grindParam| _=_ $decl:ident)
+          | .eqBoth true,   _     => `(Parser.Tactic.grindParam| _=_ gen $decl:ident)
+          | .eqBwd,         _     => `(Parser.Tactic.grindParam| ←= $decl:ident)
+          | .user,          _     => `(Parser.Tactic.grindParam| usr $decl:ident)
+          | .bwd false,     false => `(Parser.Tactic.grindParam| ← $decl:ident)
+          | .bwd true,      false => `(Parser.Tactic.grindParam| ← gen $decl:ident)
+          | .fwd,           false => `(Parser.Tactic.grindParam| → $decl:ident)
+          | .leftRight,     false => `(Parser.Tactic.grindParam| => $decl:ident)
+          | .rightLeft,     false => `(Parser.Tactic.grindParam| <= $decl:ident)
+          | .default false, false => `(Parser.Tactic.grindParam| $decl:ident)
+          | .default true,  false => `(Parser.Tactic.grindParam| gen $decl:ident)
+          | .bwd false,     true  => `(Parser.Tactic.grindParam| ! ← $decl:ident)
+          | .bwd true,      true  => `(Parser.Tactic.grindParam| ! ← gen $decl:ident)
+          | .fwd,           true  => `(Parser.Tactic.grindParam| ! → $decl:ident)
+          | .leftRight,     true  => `(Parser.Tactic.grindParam| ! => $decl:ident)
+          | .rightLeft,     true  => `(Parser.Tactic.grindParam| ! <= $decl:ident)
+          | .default false, true  => `(Parser.Tactic.grindParam| ! $decl:ident)
+          | .default true,  true  => `(Parser.Tactic.grindParam| ! gen $decl:ident)
+        params := params.push param
+  for declName in trace.eagerCases.toList do
+    unless Grind.isBuiltinEagerCases declName do
+      let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+      let param ← `(Parser.Tactic.grindParam| cases eager $decl)
+      params := params.push param
+  for declName in trace.cases.toList do
+    unless trace.eagerCases.contains declName || Grind.isBuiltinEagerCases declName do
+      let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+      let param ← `(Parser.Tactic.grindParam| cases $decl)
+      params := params.push param
+  let result ← if let some fallback := fallback? then
+    `(tactic| grind $config:optConfig only on_failure $fallback)
+  else
+    `(tactic| grind $config:optConfig only)
+  return setGrindParams result params
+
+@[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
+  match stx with
+  | `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+    let config ← elabGrindConfig config
+    discard <| evalGrindCore stx config only params fallback?
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.grindTrace] def evalGrindTrace : Tactic := fun stx => do
+  match stx with
+  | `(tactic| grind?%$tk $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+    let config ← elabGrindConfig configStx
+    let config := { config with trace := true }
+    let trace ← evalGrindCore stx config only params fallback?
+    let stx ← mkGrindOnly configStx fallback? trace
+    Tactic.TryThis.addSuggestion tk stx (origSpan? := ← getRef)
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.cutsat] def evalCutsat : Tactic := fun stx => do
+  match stx with
+  | `(tactic| cutsat $config:optConfig) =>
+    let config ← elabCutsatConfig config
+    discard <| evalGrindCore stx { config with } none none none
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.grobner] def evalGrobner : Tactic := fun stx => do
+  match stx with
+  | `(tactic| grobner $config:optConfig) =>
+    let config ← elabGrobnerConfig config
+    discard <| evalGrindCore stx { config with } none none none
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean
index ac46dd787b..eecd8af144 100644
--- a/src/Lean/Elab/Term/TermElabM.lean
+++ b/src/Lean/Elab/Term/TermElabM.lean
@@ -203,35 +203,6 @@ structure State where
   goals : List MVarId
   deriving Inhabited
 
-/--
-  Snapshots are used to implement the `save` tactic.
-  This tactic caches the state of the system, and allows us to "replay"
-  expensive proofs efficiently. This is only relevant implementing the
-  LSP server.
--/
-structure Snapshot where
-  core   : Core.State
-  «meta» : Meta.State
-  term   : Term.State
-  tactic : Tactic.State
-  stx    : Syntax
-
-/--
-  Key for the cache used to implement the `save` tactic.
--/
-structure CacheKey where
-  mvarId : MVarId -- TODO: should include all goals
-  pos    : String.Pos
-  deriving BEq, Hashable, Inhabited
-
-/--
-  Cache for the `save` tactic.
--/
-structure Cache where
-   pre  : PHashMap CacheKey Snapshot := {}
-   post : PHashMap CacheKey Snapshot := {}
-   deriving Inhabited
-
 section Snapshot
 open Language
 
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..ad491b0de1 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {