diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index f149e36f631b..e32609ee869c 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -527,6 +527,14 @@ theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.ca
 
 @[simp, grind =] theorem val_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
 
+/-
+**Note**
+The current pattern inference heuristic includes the implicit term `n + m` as pattern of the pattern,
+but arithmetic is problematic in patterns because it is an interpreted symbol. For example,
+we will fail to match `@val n (castNat 0 i)`. Thus, we mark the implicit subterm with `no_index`
+-/
+grind_pattern val_castAdd => @val (no_index _) (castAdd m i)
+
 @[deprecated val_castAdd (since := "2025-11-21")]
 theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
 
@@ -637,7 +645,15 @@ theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i)
 
 theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := rfl
 
-@[simp, grind =] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
+@[simp] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
+
+/-
+**Note**
+The current pattern inference heuristic includes the implicit term `n + m` as pattern of the pattern,
+but arithmetic is problematic in patterns because it is an interpreted symbol. For example,
+we will fail to match `@val n (addNat i 0)`. Thus, we mark the implicit subterm with `no_index`
+-/
+grind_pattern val_addNat => @val (no_index _) (addNat i m)
 
 @[deprecated val_addNat (since := "2025-11-21")]
 theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 2f18f450fab4..4ba54603c4c6 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -1751,6 +1751,12 @@ def isFalse (e : Expr) : Bool :=
 def isTrue (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``True
 
+def isBoolFalse (e : Expr) : Bool :=
+  e.cleanupAnnotations.isConstOf ``false
+
+def isBoolTrue (e : Expr) : Bool :=
+  e.cleanupAnnotations.isConstOf ``true
+
 /--
 `getForallArity type` returns the arity of a `forall`-type. This function consumes nested annotations,
 and performs pending beta reductions. It does **not** use whnf.
diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean
index a672aa0d08f5..0c2e790df5f5 100644
--- a/src/Lean/Meta/Offset.lean
+++ b/src/Lean/Meta/Offset.lean
@@ -105,7 +105,7 @@ private def isNatZero (e : Expr) : MetaM Bool := do
   | some v => return v == 0
   | _      => return false
 
-private def mkOffset (e : Expr) (offset : Nat) : MetaM Expr := do
+def mkOffset (e : Expr) (offset : Nat) : MetaM Expr := do
   if offset == 0 then
     return e
   else if (← isNatZero e) then
diff --git a/src/Lean/Meta/Sym.lean b/src/Lean/Meta/Sym.lean
index daa49fd597b1..0a18bea77267 100644
--- a/src/Lean/Meta/Sym.lean
+++ b/src/Lean/Meta/Sym.lean
@@ -24,7 +24,9 @@ public import Lean.Meta.Sym.InferType
 public import Lean.Meta.Sym.Simp
 public import Lean.Meta.Sym.Util
 public import Lean.Meta.Sym.Eta
+public import Lean.Meta.Sym.Canon
 public import Lean.Meta.Sym.Grind
+public import Lean.Meta.Sym.SynthInstance
 
 /-!
 # Symbolic computation support.
diff --git a/src/Lean/Meta/Sym/Canon.lean b/src/Lean/Meta/Sym/Canon.lean
new file mode 100644
index 000000000000..ace691a1bd33
--- /dev/null
+++ b/src/Lean/Meta/Sym/Canon.lean
@@ -0,0 +1,433 @@
+/-
+Copyright (c) 2026 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.Meta.Sym.SymM
+import Lean.Meta.Sym.ExprPtr
+import Lean.Meta.SynthInstance
+import Lean.Meta.Sym.SynthInstance
+import Lean.Meta.IntInstTesters
+import Lean.Meta.NatInstTesters
+import Lean.Meta.Sym.Eta
+import Lean.Meta.WHNF
+import Init.Grind.Util
+namespace Lean.Meta.Sym
+namespace Canon
+
+builtin_initialize registerTraceClass `sym.debug.canon
+
+/-!
+# Type-directed canonicalizer
+
+Canonicalizes expressions by normalizing types and instances. At the top level, it traverses
+applications, foralls, lambdas, and let-bindings, classifying each argument as a type, instance,
+implicit, or value using `shouldCanon`. Values are recursively visited but not normalized.
+Types and instances receive targeted reductions.
+
+## Reductions (applied only in type positions)
+
+- **Eta**: `fun x => f x` → `f`
+- **Projection**: `⟨a, b⟩.1` → `a` (structure projections, not class projections)
+- **Match/ite/cond**: reduced when discriminant is a constructor or literal
+- **Nat arithmetic**: ground evaluation (`2 + 1` → `3`) and offset normalization
+  (`n.succ + 1` → `n + 2`)
+
+## Instance canonicalization
+
+Instances are re-synthesized via `synthInstance`. The instance type is first normalized
+using the type-level reductions above, so that `OfNat (Fin (2+1)) 0` and `OfNat (Fin 3) 0`
+produce the same canonical instance.
+
+## Two caches
+
+The canonicalizer maintains separate caches for type-level and value-level contexts.
+The same expression may canonicalize differently depending on whether it appears in a
+type position (where reductions are applied) or a value position (where it is only traversed).
+Caches are keyed by `Expr` (structural equality), not pointer equality, because
+the canonicalizer runs before `shareCommon` and enters binders using locally nameless
+representation.
+
+## Future work
+
+If needed we should add support for user-defined extensions.
+-/
+
+structure Context where
+  /-- `true` if we are visiting a type. -/
+  insideType : Bool := false
+
+abbrev CanonM := ReaderT Context SymM
+
+/--
+Auxiliary function for normalizing the arguments of `OfNat.ofNat` during canonicalization.
+This is needed because satellite solvers create `Nat` and `Int` numerals using the
+APIs `mkNatLit` and `mkIntLit`, which produce terms of the form
+`@OfNat.ofNat Nat <num> inst` and `@OfNat.ofNat Int <num> inst`.
+This becomes a problem when a term in the input goal has already been canonicalized
+and its type is not exactly `Nat` or `Int`. For example, in issue #9477, we have:
+```
+structure T where
+upper_bound : Nat
+def T.range (a : T) := 0...a.upper_bound
+theorem range_lower (a : T) : a.range.lower = 0 := by rfl
+```
+Here, the `0` in `range_lower` is actually represented as:
+```
+(@OfNat.ofNat
+  (Std.PRange.Bound (Std.PRange.RangeShape.lower (Std.PRange.RangeShape.mk Std.PRange.BoundShape.closed Std.PRange.BoundShape.open)) Nat)
+  (nat_lit 0)
+  (instOfNatNat (nat_lit 0)))
+```
+Without this normalization step, the satellite solver would need to handle multiple
+representations for `(0 : Nat)` and `(0 : Int)`, complicating reasoning.
+-/
+-- Remark: This is not a great solution. We should consider writing a custom canonicalizer for
+-- `OfNat.ofNat` and other constants with built-in support in `grind`.
+private def normOfNatArgs? (args : Array Expr) : MetaM (Option (Array Expr)) := do
+  if h : args.size = 3 then
+    let mut args : Vector Expr 3 := h ▸ args.toVector
+    let mut modified := false
+    if args[1].isAppOf ``OfNat.ofNat then
+      -- If nested `OfNat.ofNat`, convert to raw nat literal
+      let some val ← getNatValue? args[1] | pure ()
+      args := args.set 1 (mkRawNatLit val)
+      modified := true
+    let inst := args[2]
+    if (← Structural.isInstOfNatNat inst) && !args[0].isConstOf ``Nat then
+      return some (args.set 0 Nat.mkType |>.toArray)
+    else if (← Structural.isInstOfNatInt inst) && !args[0].isConstOf ``Int then
+      return some (args.set 0 Int.mkType |>.toArray)
+    else if modified then
+      return some args.toArray
+  return none
+
+abbrev withCaching (e : Expr) (k : CanonM Expr) : CanonM Expr := do
+  if (← read).insideType then
+    if let some r := (← get).canon.cacheInType.get? e then
+      return r
+    else
+      let r ← k
+      modify fun s => { s with canon.cacheInType := s.canon.cacheInType.insert e r }
+      return r
+  else
+    if let some r := (← get).canon.cache.get? e then
+      return r
+    else
+      let r ← k
+      modify fun s => { s with canon.cache := s.canon.cache.insert e r }
+      return r
+
+def isTrueCond (e : Expr) : Bool :=
+  match_expr e with
+  | True => true
+  | Eq _ a b => a.isBoolTrue && b.isBoolTrue
+  | _ => false
+
+def isFalseCond (e : Expr) : Bool :=
+  match_expr e with
+  | False => true
+  | Eq _ a b => a.isBoolFalse && b.isBoolTrue
+  | _ => false
+
+/--
+Return type for the `shouldCanon` function.
+-/
+inductive ShouldCanonResult where
+  | /- Nested types (and type formers) are canonicalized. -/
+    canonType
+  | /- Nested instances are canonicalized. -/
+    canonInst
+  | /- Implicit argument that is not an instance nor a type. -/
+    canonImplicit
+  | /-
+    Term is not a proof, type (former), nor an instance.
+    Thus, it must be recursively visited by the canonicalizer.
+    -/
+    visit
+  deriving Inhabited
+
+instance : Repr ShouldCanonResult where
+  reprPrec r _ := private match r with
+    | .canonType => "canonType"
+    | .canonInst => "canonInst"
+    | .canonImplicit => "canonImplicit"
+    | .visit => "visit"
+
+/--
+See comments at `ShouldCanonResult`.
+-/
+def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM ShouldCanonResult := do
+  if h : i < pinfos.size then
+    let pinfo := pinfos[i]
+    if pinfo.isInstance then
+      return .canonInst
+    else if pinfo.isProp then
+      return .visit
+    else if pinfo.isImplicit then
+      if (← isTypeFormer arg) then
+        return .canonType
+      else
+        return .canonImplicit
+  if (← isProp arg) then
+    return .visit
+  else if (← isTypeFormer arg) then
+    return .canonType
+  else
+    return .visit
+
+/--
+Reduce a projection function application (e.g., `@Sigma.fst _ _ ⟨a, b⟩` → `a`).
+Class projections are not reduced — they are support elements handled by instance synthesis.
+-/
+def reduceProjFn? (info : ProjectionFunctionInfo) (e : Expr) : SymM (Option Expr) := do
+  if info.fromClass then
+    return none
+  let some e ← unfoldDefinition? e | return none
+  match (← reduceProj? e.getAppFn) with
+  | some f => return some <| mkAppN f e.getAppArgs
+  | none   => return none
+
+def isNat (e : Expr) := e.isConstOf ``Nat
+
+/-- Returns `true` if `e` is a Nat arithmetic expression that should be normalized
+(ground evaluation or offset normalization). -/
+def isNatArithApp (e : Expr) : Bool :=
+  match_expr e with
+  | Nat.zero => true
+  | Nat.succ _ => true
+  | HAdd.hAdd α _ _ _ _ _ => isNat α
+  | HMul.hMul α _ _ _ _ _ => isNat α
+  | HSub.hSub α _ _ _ _ _ => isNat α
+  | HDiv.hDiv α _ _ _ _ _ => isNat α
+  | HMod.hMod α _ _ _ _ _ => isNat α
+  | _ => false
+
+/-- Check that `e` is definitionally equal to `inst` at instance transparency.
+Returns `inst` on success, `e` with a reported issue on failure. -/
+def checkDefEqInst (e : Expr) (inst : Expr) : SymM Expr := do
+  unless (← isDefEqI e inst) do
+    reportIssue! "failed to canonicalize instance{indentExpr e}\nsynthesized instance is not definitionally equal{indentExpr inst}"
+    return e
+  return inst
+
+/-- Canonicalize `e`. Applies targeted reductions in type positions; recursively visits value positions. -/
+partial def canon (e : Expr) : CanonM Expr := do
+  match e with
+  | .forallE ..    => withCaching e <| canonForall #[] e
+  | .lam ..        => withCaching e <| canonLambda e
+  | .letE ..       => withCaching e <| canonLet #[] e
+  | .app ..        => withCaching e <| canonApp e
+  | .proj ..       => withCaching e <| canonProj e
+  | .mdata _ b     => return e.updateMData! (← canon b)
+  | _              => return e
+where
+  canonInsideType (e : Expr) : CanonM Expr := do
+    if (← read).insideType then
+      canon e
+    else if (← isProp e) then
+      /-
+      If the body is a proposition (like `a ∈ m → ...`), normalizing inside it could change the
+      shape of the proposition and confuse grind's proposition handling.
+      -/
+      canon e
+    else
+      withReader (fun ctx => { ctx with insideType := true }) <| canon e
+
+  /--
+  Similar to `canonInsideType`, but skips the `isProp` check.
+  Use only when `e` is known not to be a proposition.
+  -/
+  canonInsideType' (e : Expr) : CanonM Expr := do
+    if (← read).insideType then
+      canon e
+    else
+      withReader (fun ctx => { ctx with insideType := true }) <| canon e
+
+  canonInst (e : Expr) : CanonM Expr := do
+    if let some inst := (← get).canon.cacheInsts.get? e then
+      checkDefEqInst e inst
+    else
+      /-
+      We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
+      the same instances.
+      -/
+      let type ← inferType e
+      let type' ← canonInsideType' type
+      let some inst ← Sym.synthInstance? type' |
+        reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type'}"
+        return e
+      let inst ← checkDefEqInst e inst
+      -- Remark: we cache result using the type **before** canonicalization.
+      modify fun s => { s with canon.cacheInsts := s.canon.cacheInsts.insert e inst }
+      return inst
+
+  canonLambda (e : Expr) : CanonM Expr := do
+    if (← read).insideType then
+      canonLambdaLoop #[] (etaReduce e)
+    else
+      canonLambdaLoop #[] e
+
+  canonLambdaLoop (fvars : Array Expr) (e : Expr) : CanonM Expr := do
+    match e with
+    | .lam n d b c =>
+      withLocalDecl n c (← canonInsideType (d.instantiateRev fvars)) fun x =>
+        canonLambdaLoop (fvars.push x) b
+    | e =>
+      mkLambdaFVars fvars (← canon (e.instantiateRev fvars))
+
+  canonForall (fvars : Array Expr) (e : Expr) : CanonM Expr := do
+    match e with
+    | .forallE n d b c =>
+      withLocalDecl n c (← canonInsideType (d.instantiateRev fvars)) fun x =>
+        canonForall (fvars.push x) b
+    | e =>
+      mkForallFVars fvars (← canonInsideType (e.instantiateRev fvars))
+
+  canonLet (fvars : Array Expr) (e : Expr) : CanonM Expr := do
+    match e with
+    | .letE n t v b nondep =>
+      withLetDecl n (← canonInsideType (t.instantiateRev fvars)) (← canon (v.instantiateRev fvars)) (nondep := nondep) fun x =>
+        canonLet (fvars.push x) b
+    | e =>
+      mkLetFVars (generalizeNondepLet := false) fvars (← canon (e.instantiateRev fvars))
+
+  canonAppDefault (e : Expr) : CanonM Expr := e.withApp fun f args => do
+    if f.isConstOf ``Grind.nestedProof && args.size == 2 then
+      let prop := args[0]!
+      let prop' ← canon prop
+      let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
+      return e'
+    else if f.isConstOf ``Grind.nestedDecidable && args.size == 2 then
+      let prop := args[0]!
+      let prop' ← canon prop
+      let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
+      return e'
+    else
+      let mut modified := false
+      let args ← if f.isConstOf ``OfNat.ofNat then
+        let some args ← normOfNatArgs? args | pure args
+        modified := true
+        pure args
+      else
+        pure args
+      let mut f := f
+      let f' ← canon f
+      unless isSameExpr f f' do
+        f := f'
+        modified := true
+      let pinfos := (← getFunInfo f).paramInfo
+      let mut args := args.toVector
+      for h : i in *...args.size do
+        let arg := args[i]
+        trace[sym.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
+        let arg' ← match (← shouldCanon pinfos i arg) with
+          | .canonType =>
+            /-
+            The type may have nested propositions and terms that may need to be canonicalized too.
+            So, we must recurse over it. See issue #10232
+            -/
+            canonInsideType' arg
+          | .canonImplicit => canon arg
+          | .visit => canon arg
+          | .canonInst =>
+            if arg.isAppOfArity ``Grind.nestedDecidable 2 then
+              let prop := arg.appFn!.appArg!
+              let prop' ← canon prop
+              if isSameExpr prop prop' then pure arg else pure (mkApp2 arg.appFn!.appFn! prop' arg.appArg!)
+            else
+              canonInst arg
+        unless isSameExpr arg arg' do
+          args := args.set i arg'
+          modified := true
+      return if modified then mkAppN f args.toArray else e
+
+  canonIte (f : Expr) (α c inst a b : Expr) : CanonM Expr := do
+    let c ← canon c
+    if isTrueCond c then canon a
+    else if isFalseCond c then canon b
+    else return mkApp5 f (← canonInsideType α) c (← canonInst inst) (← canon a) (← canon b)
+
+  canonCond (f : Expr) (α c a b : Expr) : CanonM Expr := do
+    let c ← canon c
+    if c.isBoolTrue then canon a
+    else if c.isBoolFalse then canon b
+    else return mkApp4 f (← canonInsideType α) c (← canon a) (← canon b)
+
+  postReduce (e : Expr) : CanonM Expr := do
+    if isNatArithApp e then
+      if let some e ← evalNat e |>.run then
+        return mkNatLit e
+      else if let some (e, k) ← isOffset? e |>.run then
+        mkOffset e k
+      else
+        return e
+    else
+      let f := e.getAppFn
+      let .const declName _ := f | return e
+      if let some info ← getProjectionFnInfo? declName then
+        return (← reduceProjFn? info e).getD e
+      else
+        return e
+
+  /-- Canonicalize `e` and apply post reductions. -/
+  canonAppAndPost (e : Expr) : CanonM Expr := do
+    let e ← canonAppDefault e
+    postReduce e
+
+  canonMatch (e : Expr) : CanonM Expr := do
+    if let .reduced e ← reduceMatcher? e then
+      canon e
+    else
+      let e ← canonAppDefault e
+      -- Remark: try again, discriminants may have been simplified.
+      if let .reduced e ← reduceMatcher? e then
+        canon e
+      else
+        return e
+
+  canonApp (e : Expr) : CanonM Expr := do
+    if (← read).insideType then
+      match_expr e with
+      | f@ite α c i a b => canonIte f α c i a b
+      | f@cond α c a b => canonCond f α c a b
+      -- Remark: We currently don't normalize dependent-if-then-else occurring in types.
+      | _ =>
+        let f := e.getAppFn
+        let .const declName _ := f | canonAppAndPost e
+        if (← isMatcher declName) then
+          canonMatch e
+        else
+          canonAppAndPost e
+    else
+      canonAppDefault e
+
+  canonProj (e : Expr) : CanonM Expr := do
+    let e := e.updateProj! (← canon e.projExpr!)
+    if (← read).insideType then
+      return (← reduceProj? e).getD e
+    else
+      return e
+
+/--
+Returns `true` if `shouldCannon pinfos i arg` is not `.visit`.
+This is a helper function used to implement mbtc.
+-/
+public def isSupport (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Bool := do
+  let r ← Canon.shouldCanon pinfos i arg
+  return !r matches .visit
+
+end Canon
+
+/--
+Canonicalize `e` by normalizing types, instances, and support arguments.
+Types receive targeted reductions (eta, projection, match/ite, Nat arithmetic).
+Instances are re-synthesized. Values are traversed but not reduced.
+Runs at reducible transparency.
+-/
+public def canon (e : Expr) : SymM Expr := do profileitM Exception "sym canon" (← getOptions) do
+  withReducible do Canon.canon e {}
+
+end Lean.Meta.Sym
diff --git a/src/Lean/Meta/Sym/SymM.lean b/src/Lean/Meta/Sym/SymM.lean
index 080466d27d3a..130b7208b28e 100644
--- a/src/Lean/Meta/Sym/SymM.lean
+++ b/src/Lean/Meta/Sym/SymM.lean
@@ -147,6 +147,14 @@ structure Context where
   sharedExprs : SharedExprs
   config      : Config := {}
 
+structure Canon.State where
+  /-- Cache for value-level canonicalization (no type reductions applied). -/
+  cache       : Std.HashMap Expr Expr := {}
+  /-- Cache for type-level canonicalization (reductions applied). -/
+  cacheInType : Std.HashMap Expr Expr := {}
+  /-- Cache mapping instances to their canonical synthesized instances. -/
+  cacheInsts  : Std.HashMap Expr Expr := {}
+
 /-- Mutable state for the symbolic computation framework. -/
 structure State where
   /-- `ShareCommon` (aka `Hash-consing`) state. -/
@@ -191,6 +199,7 @@ structure State where
   within a `sym =>` block and reported when a tactic fails.
   -/
   issues : List MessageData := []
+  canon : Canon.State := {}
   debug : Bool := false
 
 abbrev SymM := ReaderT Context <| StateRefT State MetaM
diff --git a/src/Lean/Meta/Sym/SynthInstance.lean b/src/Lean/Meta/Sym/SynthInstance.lean
new file mode 100644
index 000000000000..7ab0223e39d0
--- /dev/null
+++ b/src/Lean/Meta/Sym/SynthInstance.lean
@@ -0,0 +1,76 @@
+/-
+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.Meta.Sym.SymM
+import Lean.Meta.SynthInstance
+public section
+namespace Lean.Meta.Sym
+/--
+Some modules in grind use builtin instances defined directly in core (e.g., `lia`),
+while others synthesize them using `synthInstance` (e.g., `ring`).
+This inconsistency is problematic, as it may introduce mismatches and result in
+two different representations for the same term.
+
+The following table is used to bypass synthInstance for the builtin cases.
+-/
+private def builtinInsts : Std.HashMap Expr Expr :=
+  let nat := Nat.mkType
+  let int := Int.mkType
+  let us  := [Level.zero, Level.zero, Level.zero]
+  Std.HashMap.ofList [
+    (mkApp3 (mkConst ``HAdd us) nat nat nat, Nat.mkInstHAdd),
+    (mkApp3 (mkConst ``HSub us) nat nat nat, Nat.mkInstHSub),
+    (mkApp3 (mkConst ``HMul us) nat nat nat, Nat.mkInstHMul),
+    (mkApp3 (mkConst ``HDiv us) nat nat nat, Nat.mkInstHDiv),
+    (mkApp3 (mkConst ``HMod us) nat nat nat, Nat.mkInstHMod),
+    (mkApp3 (mkConst ``HPow us) nat nat nat, Nat.mkInstHPow),
+    (mkApp  (mkConst ``LT [0]) nat, Nat.mkInstLT),
+    (mkApp  (mkConst ``LE [0]) nat, Nat.mkInstLE),
+
+    (mkApp3 (mkConst ``HAdd us) int int int, Int.mkInstHAdd),
+    (mkApp3 (mkConst ``HSub us) int int int, Int.mkInstHSub),
+    (mkApp3 (mkConst ``HMul us) int int int, Int.mkInstHMul),
+    (mkApp3 (mkConst ``HDiv us) int int int, Int.mkInstHDiv),
+    (mkApp3 (mkConst ``HMod us) int int int, Int.mkInstHMod),
+    (mkApp3 (mkConst ``HPow us) int nat int, Int.mkInstHPow),
+    (mkApp  (mkConst ``LT [0]) int, Int.mkInstLT),
+    (mkApp  (mkConst ``LE [0]) int, Int.mkInstLE),
+  ]
+
+/--
+Some modules in grind use builtin instances defined directly in core (e.g., `lia`).
+Users may provide nonstandard instances that are definitionally equal to the ones in core.
+Given a type, such as `HAdd Int Int Int`, this function returns the instance defined in
+core.
+-/
+def getBuiltinInstance? (type : Expr) : Option Expr :=
+  builtinInsts[type]?
+
+def synthInstanceMeta? (type : Expr) : MetaM (Option Expr) := do profileitM Exception "sym typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
+  if let some inst := getBuiltinInstance? type then
+    return inst
+  catchInternalId isDefEqStuckExceptionId
+    (synthInstanceCore? type none)
+    (fun _ => pure none)
+
+abbrev synthInstance? (type : Expr) : SymM (Option Expr) :=
+  synthInstanceMeta? type
+
+def synthInstance (type : Expr) : SymM Expr := do
+  let some inst ← synthInstance? type
+    | throwError "`sym` failed to find instance{indentExpr type}"
+  return inst
+
+/--
+Helper function for instantiating a type class `type`, and
+then using the result to perform `isDefEq x val`.
+-/
+def synthInstanceAndAssign (x type : Expr) : SymM Bool := do
+  let some val ← synthInstance? type | return false
+  isDefEq x val
+
+end Lean.Meta.Sym
diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index f616f8f125f2..37e9a9b5f764 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -12,7 +12,6 @@ public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Cases
 public import Lean.Meta.Tactic.Grind.Injection
 public import Lean.Meta.Tactic.Grind.Core
-public import Lean.Meta.Tactic.Grind.Canon
 public import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
 public import Lean.Meta.Tactic.Grind.Inv
 public import Lean.Meta.Tactic.Grind.Proof
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.lean b/src/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.lean
index da182d7f4861..82ee4a2e0392 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.lean
@@ -6,8 +6,11 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Basic
-import Lean.Meta.Tactic.Grind.SynthInstance
 import Init.Grind.FieldNormNum
+import Lean.Meta.Tactic.Grind.SynthInstance
+import Lean.Meta.AppBuilder
+import Lean.Meta.LitValues
+import Lean.Util.SafeExponentiation
 namespace Lean.Meta.Grind.Arith
 namespace FieldNormNum
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean b/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean
index 6f74c39c4e70..7c6b53635b26 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean
@@ -8,8 +8,13 @@ prelude
 public import Init.Grind.Ring.Basic
 public import Init.Simproc
 public import Lean.Meta.Tactic.Grind.SynthInstance
+public import Init.Simproc
+public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
+import Lean.Meta.LitValues
 import Init.Grind.Ring.Field
+import Lean.Meta.DecLevel
 import Lean.Meta.Tactic.Grind.Arith.FieldNormNum
+import Lean.Util.SafeExponentiation
 public section
 namespace Lean.Meta.Grind.Arith
 
diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean
deleted file mode 100644
index 8773833a5b0e..000000000000
--- a/src/Lean/Meta/Tactic/Grind/Canon.lean
+++ /dev/null
@@ -1,272 +0,0 @@
-/-
-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 Lean.Meta.Tactic.Grind.Types
-import Init.Grind.Util
-import Lean.Meta.IntInstTesters
-import Lean.Meta.NatInstTesters
-import Lean.Meta.Tactic.Grind.SynthInstance
-public section
-namespace Lean.Meta.Grind
-namespace Canon
-
-/-!
-A canonicalizer module for the `grind` tactic. The canonicalizer defined in `Meta/Canonicalizer.lean` is
-not suitable for the `grind` tactic. It was designed for tactics such as `omega`, where the goal is
-to detect when two structurally different atoms are definitionally equal.
-
-The `grind` tactic, on the other hand, uses congruence closure. Moreover, types, type formers, proofs, and instances
-are considered supporting elements and are not factored into congruence detection.
-
-This module minimizes the number of `isDefEq` checks by comparing two terms `a` and `b` only if they are instances,
-types, or type formers and are the `i`-th arguments of two different `f`-applications. This approach is
-sufficient for the congruence closure procedure used by the `grind` tactic.
-
-To further optimize `isDefEq` checks, instances are compared using `TransparencyMode.instances`, which reduces
-the number of constants that need to be unfolded. If diagnostics are enabled, instances are compared using
-the default transparency mode too for sanity checking, and discrepancies are reported.
-Types and type formers are always checked using default transparency.
-
-Remark:
-The canonicalizer minimizes issues with non-canonical instances and structurally different but definitionally equal types,
-but it does not solve all problems. For example, consider a situation where we have `(a : BitVec n)`
-and `(b : BitVec m)`, along with instances `inst1 n : Add (BitVec n)` and `inst2 m : Add (BitVec m)` where `inst1`
-and `inst2` are structurally different. Now consider the terms `a + a` and `b + b`. After canonicalization, the two
-additions will still use structurally different (and definitionally different) instances: `inst1 n` and `inst2 m`.
-Furthermore, `grind` will not be able to infer that  `a + a ≍ b + b` even if we add the assumptions `n = m` and `a ≍ b`.
--/
-
-@[inline] private def get' : GoalM State :=
-  return (← get).canon
-
-@[inline] private def modify' (f : State → State) : GoalM Unit :=
-  modify fun s => { s with canon := f s.canon }
-
-/--
-Helper function for canonicalizing `e` occurring as the `i`th argument of an `f`-application.
-Remark: `isInst` is `true` if element is an instance.
--/
-private def canonElemCore (f : Expr) (i : Nat) (e : Expr) (isInst := false) : GoalM Expr := do
-  let s ← get'
-  let key := { f, i, arg := e : CanonArgKey }
-  if let some c := s.canonArg.find? key then
-    return c
-  let c ← go
-  modify' fun s => { s with canonArg := s.canonArg.insert key c }
-  return c
-where
-  checkDefEq (e c : Expr) : GoalM Bool := do
-    if (← isDefEq e c) then
-      trace_goal[grind.debug.canon] "found {e} ===> {c}"
-      return true
-    return false
-
-  go : GoalM Expr := do
-    let eType ← inferType e
-    if isInst then
-      /-
-      **Note**: Recall that some `grind` modules (e.g., `lia`) rely on instances defined directly in core.
-      This test ensures we use them as the canonical representative.
-      -/
-      if let some c := getBuiltinInstance? eType then
-        if (← checkDefEq e c) then
-          return c
-    let s ← get'
-    let key := (f, i)
-    let cs := s.argMap.find? key |>.getD []
-    for (c, cType) in cs do
-      /-
-      We first check the types
-      The following checks are a performance bottleneck.
-      For example, in the test `grind_ite.lean`, there are many checks of the form:
-      ```
-      w_4 ∈ assign.insert v true → Prop =?= w_1 ∈ assign.insert v false → Prop
-      ```
-      where `grind` unfolds the definition of `DHashMap.insert` and `TreeMap.insert`.
-      -/
-      if (← isDefEqD eType cType) then
-        if (← checkDefEq e c) then
-          return c
-    trace_goal[grind.debug.canon] "({f}, {i}) ↦ {e}"
-    modify' fun s => { s with argMap := s.argMap.insert key ((e, eType)::cs) }
-    return e
-
-private abbrev canonType (f : Expr) (i : Nat) (e : Expr) :=
-  withDefault <| canonElemCore f i e
-
-private abbrev canonInst (f : Expr) (i : Nat) (e : Expr) :=
-  withReducibleAndInstances <| canonElemCore f i e (isInst := true)
-
-private abbrev canonImplicit (f : Expr) (i : Nat) (e : Expr) :=
-  withReducible <| canonElemCore f i e
-
-/--
-Return type for the `shouldCanon` function.
--/
-private inductive ShouldCanonResult where
-  | /- Nested types (and type formers) are canonicalized. -/
-    canonType
-  | /- Nested instances are canonicalized. -/
-    canonInst
-  | /- Implicit argument that is not an instance nor a type. -/
-    canonImplicit
-  | /-
-    Term is not a proof, type (former), nor an instance.
-    Thus, it must be recursively visited by the canonicalizer.
-    -/
-    visit
-  deriving Inhabited
-
-private instance : Repr ShouldCanonResult where
-  reprPrec r _ := private match r with
-    | .canonType => "canonType"
-    | .canonInst => "canonInst"
-    | .canonImplicit => "canonImplicit"
-    | .visit => "visit"
-
-/--
-See comments at `ShouldCanonResult`.
--/
-private def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM ShouldCanonResult := do
-  if h : i < pinfos.size then
-    let pinfo := pinfos[i]
-    if pinfo.isInstance then
-      return .canonInst
-    else if pinfo.isProp then
-      return .visit
-    else if pinfo.isImplicit then
-      if (← isTypeFormer arg) then
-        return .canonType
-      else
-        return .canonImplicit
-  if (← isProp arg) then
-    return .visit
-  else if (← isTypeFormer arg) then
-    return .canonType
-  else
-    return .visit
-
-/--
-Returns `true` if `shouldCannon pinfos i arg` is not `.visit`.
-This is a helper function used to implement mbtc.
--/
-def isSupport (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Bool := do
-  let r ← shouldCanon pinfos i arg
-  return !r matches .visit
-
-/--
-Auxiliary function for normalizing the arguments of `OfNat.ofNat` during canonicalization.
-This is needed because satellite solvers create `Nat` and `Int` numerals using the
-APIs `mkNatLit` and `mkIntLit`, which produce terms of the form
-`@OfNat.ofNat Nat <num> inst` and `@OfNat.ofNat Int <num> inst`.
-This becomes a problem when a term in the input goal has already been canonicalized
-and its type is not exactly `Nat` or `Int`. For example, in issue #9477, we have:
-```
-structure T where
-upper_bound : Nat
-def T.range (a : T) := 0...a.upper_bound
-theorem range\_lower (a : T) : a.range.lower = 0 := by rfl
-```
-Here, the `0` in `range_lower` is actually represented as:
-```
-(@OfNat.ofNat
-  (Std.PRange.Bound (Std.PRange.RangeShape.lower (Std.PRange.RangeShape.mk Std.PRange.BoundShape.closed Std.PRange.BoundShape.open)) Nat)
-  (nat_lit 0)
-  (instOfNatNat (nat_lit 0)))
-```
-Without this normalization step, the satellite solver would need to handle multiple
-representations for `(0 : Nat)` and `(0 : Int)`, complicating reasoning.
--/
--- Remark: This is not a great solution. We should consider writing a custom canonicalizer for
--- `OfNat.ofNat` and other constants with built-in support in `grind`.
-private def normOfNatArgs? (args : Array Expr) : MetaM (Option (Array Expr)) := do
-  if h : args.size = 3 then
-    let mut args : Vector Expr 3 := h ▸ args.toVector
-    let mut modified := false
-    if args[1].isAppOf ``OfNat.ofNat then
-      -- If nested `OfNat.ofNat`, convert to raw nat literal
-      let some val ← getNatValue? args[1] | pure ()
-      args := args.set 1 (mkRawNatLit val)
-      modified := true
-    let inst := args[2]
-    if (← Structural.isInstOfNatNat inst) && !args[0].isConstOf ``Nat then
-      return some (args.set 0 Nat.mkType |>.toArray)
-    else if (← Structural.isInstOfNatInt inst) && !args[0].isConstOf ``Int then
-      return some (args.set 0 Int.mkType |>.toArray)
-    else if modified then
-      return some args.toArray
-  return none
-
-set_option compiler.ignoreBorrowAnnotation true in
-@[export lean_grind_canon]
-partial def canonImpl (e : Expr) : GoalM Expr := do profileitM Exception "grind canon" (← getOptions) do
-  trace_goal[grind.debug.canon] "{e}"
-  visit e |>.run' {}
-where
-  visit (e : Expr) : StateRefT (Std.HashMap ExprPtr Expr) GoalM Expr := do
-    unless e.isApp || e.isForall do return e
-    -- Check whether it is cached
-    if let some r := (← get).get? { expr := e } then
-      return r
-    let e' ← match e with
-      | .app .. => e.withApp fun f args => do
-        if f.isConstOf ``Grind.nestedProof && args.size == 2 then
-          let prop := args[0]!
-          let prop' ← visit prop
-          let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
-          pure e'
-        else if f.isConstOf ``Grind.nestedDecidable && args.size == 2 then
-          let prop := args[0]!
-          let prop' ← visit prop
-          let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
-          pure e'
-        else
-          let mut modified := false
-          let args ← if f.isConstOf ``OfNat.ofNat then
-            let some args ← normOfNatArgs? args | pure args
-            modified := true
-            pure args
-          else
-            pure args
-          let pinfos := (← getFunInfo f).paramInfo
-          let mut args := args.toVector
-          for h : i in *...args.size do
-            let arg := args[i]
-            trace_goal[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
-            let arg' ← match (← shouldCanon pinfos i arg) with
-              | .canonType =>
-                /-
-                The type may have nested propositions and terms that may need to be canonicalized too.
-                So, we must recurse over it. See issue #10232
-                -/
-                canonType f i (← visit arg)
-              | .canonImplicit => canonImplicit f i (← visit arg)
-              | .visit => visit arg
-              | .canonInst =>
-                if arg.isAppOfArity ``Grind.nestedDecidable 2 then
-                  let prop := arg.appFn!.appArg!
-                  let prop' ← visit prop
-                  if isSameExpr prop prop' then pure arg else pure (mkApp2 arg.appFn!.appFn! prop' arg.appArg!)
-                else
-                  canonInst f i arg
-            unless isSameExpr arg arg' do
-              args := args.set i arg'
-              modified := true
-          pure <| if modified then mkAppN f args.toArray else e
-      | .forallE _ d b _ =>
-        -- Recall that we have `ForallProp.lean`.
-        let d' ← visit d
-        -- Remark: users may not want to convert `p → q` into `¬p ∨ q`
-        let b' ← if b.hasLooseBVars then pure b else visit b
-        pure <| e.updateForallE! d' b'
-      | _ => unreachable!
-    modify fun s => s.insert { expr := e } e'
-    return e'
-
-end Canon
-
-end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/MBTC.lean b/src/Lean/Meta/Tactic/Grind/MBTC.lean
index 04fcb4e53734..cb35849acce4 100644
--- a/src/Lean/Meta/Tactic/Grind/MBTC.lean
+++ b/src/Lean/Meta/Tactic/Grind/MBTC.lean
@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.CastLike
 public section
 namespace Lean.Meta.Grind
@@ -66,7 +65,7 @@ private def mkKey (e : Expr) (i : Nat) : MetaM Key :=
       let arg := args[j]
       if i == j then
         args := args.set j mainMark
-      else if !(← Canon.isSupport info.paramInfo j arg) then
+      else if !(← Sym.Canon.isSupport info.paramInfo j arg) then
         args := args.set j otherMark
     let mask := mkAppN f args.toArray
     return { mask }
diff --git a/src/Lean/Meta/Tactic/Grind/OrderInsts.lean b/src/Lean/Meta/Tactic/Grind/OrderInsts.lean
index fd4d82db7e04..ce49ec1775bb 100644
--- a/src/Lean/Meta/Tactic/Grind/OrderInsts.lean
+++ b/src/Lean/Meta/Tactic/Grind/OrderInsts.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.SynthInstance
+public import Lean.Meta.Tactic.Grind.Types
 public section
 namespace Lean.Meta.Grind
 /-!
diff --git a/src/Lean/Meta/Tactic/Grind/SynthInstance.lean b/src/Lean/Meta/Tactic/Grind/SynthInstance.lean
index 0a6e8e71e6c2..f71e16619fed 100644
--- a/src/Lean/Meta/Tactic/Grind/SynthInstance.lean
+++ b/src/Lean/Meta/Tactic/Grind/SynthInstance.lean
@@ -5,71 +5,10 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Sym.SynthInstance
 public section
 namespace Lean.Meta.Grind
-/--
-Some modules in grind use builtin instances defined directly in core (e.g., `lia`),
-while others synthesize them using `synthInstance` (e.g., `ring`).
-This inconsistency is problematic, as it may introduce mismatches and result in
-two different representations for the same term.
 
-The following table is used to bypass synthInstance for the builtin cases.
--/
-private def builtinInsts : Std.HashMap Expr Expr :=
-  let nat := Nat.mkType
-  let int := Int.mkType
-  let us  := [Level.zero, Level.zero, Level.zero]
-  Std.HashMap.ofList [
-    (mkApp3 (mkConst ``HAdd us) nat nat nat, Nat.mkInstHAdd),
-    (mkApp3 (mkConst ``HSub us) nat nat nat, Nat.mkInstHSub),
-    (mkApp3 (mkConst ``HMul us) nat nat nat, Nat.mkInstHMul),
-    (mkApp3 (mkConst ``HDiv us) nat nat nat, Nat.mkInstHDiv),
-    (mkApp3 (mkConst ``HMod us) nat nat nat, Nat.mkInstHMod),
-    (mkApp3 (mkConst ``HPow us) nat nat nat, Nat.mkInstHPow),
-    (mkApp  (mkConst ``LT [0]) nat, Nat.mkInstLT),
-    (mkApp  (mkConst ``LE [0]) nat, Nat.mkInstLE),
-
-    (mkApp3 (mkConst ``HAdd us) int int int, Int.mkInstHAdd),
-    (mkApp3 (mkConst ``HSub us) int int int, Int.mkInstHSub),
-    (mkApp3 (mkConst ``HMul us) int int int, Int.mkInstHMul),
-    (mkApp3 (mkConst ``HDiv us) int int int, Int.mkInstHDiv),
-    (mkApp3 (mkConst ``HMod us) int int int, Int.mkInstHMod),
-    (mkApp3 (mkConst ``HPow us) int nat int, Int.mkInstHPow),
-    (mkApp  (mkConst ``LT [0]) int, Int.mkInstLT),
-    (mkApp  (mkConst ``LE [0]) int, Int.mkInstLE),
-  ]
-
-/--
-Some modules in grind use builtin instances defined directly in core (e.g., `lia`).
-Users may provide nonstandard instances that are definitionally equal to the ones in core.
-Given a type, such as `HAdd Int Int Int`, this function returns the instance defined in
-core.
--/
-def getBuiltinInstance? (type : Expr) : Option Expr :=
-  builtinInsts[type]?
-
-def synthInstanceMeta? (type : Expr) : MetaM (Option Expr) := do profileitM Exception "grind typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
-  if let some inst := getBuiltinInstance? type then
-    return inst
-  catchInternalId isDefEqStuckExceptionId
-    (synthInstanceCore? type none)
-    (fun _ => pure none)
-
-abbrev synthInstance? (type : Expr) : GoalM (Option Expr) :=
-  synthInstanceMeta? type
-
-def synthInstance (type : Expr) : GoalM Expr := do
-  let some inst ← synthInstance? type
-    | throwError "`grind` failed to find instance{indentExpr type}"
-  return inst
-
-/--
-Helper function for instantiating a type class `type`, and
-then using the result to perform `isDefEq x val`.
--/
-def synthInstanceAndAssign (x type : Expr) : GoalM Bool := do
-  let some val ← synthInstance? type | return false
-  isDefEq x val
+export Sym (synthInstance synthInstance? synthInstanceMeta? synthInstanceAndAssign)
 
 end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 80fe5ceceb9b..6b4e740c1ff5 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -5,15 +5,16 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+public import Init.Data.Queue
+public import Init.Grind.Config
 public import Lean.Meta.Sym.SymM
 public import Lean.Meta.Tactic.Grind.Attr
 public import Lean.Meta.Tactic.Grind.CheckResult
-public import Init.Data.Queue
+public import Lean.Meta.Sym.Canon
+meta import Init.Data.String.Basic
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.Match.MatchEqsExt
-public import Init.Grind.Config
 import Init.Data.Nat.Linear
-meta import Init.Data.String.Basic
 import Init.Omega
 import Lean.Util.ShareCommon
 public section
@@ -715,12 +716,6 @@ structure CanonArgKey where
   arg : Expr
   deriving BEq, Hashable
 
-/-- Canonicalizer state. See `Canon.lean` for additional details. -/
-structure Canon.State where
-  argMap     : PHashMap (Expr × Nat) (List (Expr × Expr)) := {}
-  canonArg   : PHashMap CanonArgKey Expr := {}
-  deriving Inhabited
-
 /-- Trace information for a case split. -/
 structure CaseTrace where
   expr   : Expr
@@ -920,7 +915,6 @@ accumulated facts.
 structure GoalState where
   /-- Next local declaration index to process. -/
   nextDeclIdx  : Nat := 0
-  canon        : Canon.State := {}
   enodeMap     : ENodeMap := default
   exprs        : PArray Expr := {}
   parents      : ParentMap := {}
@@ -1733,10 +1727,7 @@ def withoutModifyingState (x : GoalM α) : GoalM α := do
   finally
     set saved
 
-set_option compiler.ignoreBorrowAnnotation true in
-/-- Canonicalizes nested types, type formers, and instances in `e`. -/
-@[extern "lean_grind_canon"] -- Forward definition
-opaque canon (e : Expr) : GoalM Expr
+export Sym (canon)
 
 /-!
 `Action` is the *control interface* for `grind`’s search steps. It is defined in
diff --git a/tests/elab/grind_12140.lean b/tests/elab/grind_12140.lean
index 90007fc83ee7..d3f3a9a319be 100644
--- a/tests/elab/grind_12140.lean
+++ b/tests/elab/grind_12140.lean
@@ -19,27 +19,11 @@ heterogeneous equalities (e.g., `0 : Fin 3` and `0 : Fin 2` merged via `HEq`),
 
 /--
 error: `grind` failed
-case grind.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
+case grind.1
 n : Nat
 ih : (Foo.mk n).num = 0
 h : ¬(Foo.mk (n + 1)).num = 0
-h_1 : n + 1 = Nat.zero + 1
-h_2 : 1 = Nat.zero + 1
-h_3 : 1 = Nat.zero.succ + 1
-h_4 : 1 = (n + 1).succ + 1
-h_5 : 1 = (Nat.zero + 2).succ + 1
-h_6 : (n + 2).succ + 1 = (Nat.zero + 2).succ + 1
-h_7 : 2 = Nat.zero + 2
-h_8 : 1 = (Nat.zero + 3).succ + 1
-h_9 : (n + 3).succ + 1 = (Nat.zero + 3).succ + 1
-h_10 : 3 = Nat.zero + 3
-h_11 : 1 = (Nat.zero + 4).succ + 1
-h_12 : (n + 4).succ + 1 = (Nat.zero + 4).succ + 1
-h_13 : 4 = Nat.zero + 4
-h_14 : 1 = (Nat.zero + 5).succ + 1
-h_15 : (n + 5).succ + 1 = (Nat.zero + 5).succ + 1
-h_16 : 5 = Nat.zero + 5
-h_17 : 1 = (Nat.zero + 6).succ + 1
+h_1 : 1 = n + 1
 ⊢ False
 -/
 #guard_msgs in
diff --git a/tests/elab/grind_9572.lean b/tests/elab/grind_9572.lean
index 0bfc0c5aacda..f1951a1325db 100644
--- a/tests/elab/grind_9572.lean
+++ b/tests/elab/grind_9572.lean
@@ -12,22 +12,22 @@ l : List Nat
 h :
   ¬List.Pairwise
       (fun x y =>
-        (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
-          (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
+        (if x ^ i ≤ n then List.map (List.cons x) (f x) else []).Disjoint
+          (if y ^ i ≤ n then List.map (List.cons y) (f y) else []))
       l
 ⊢ False
 [grind] Goal diagnostics
   [facts] Asserted facts
     [prop] ¬List.Pairwise
             (fun x y =>
-              (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
-                (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
+              (if x ^ i ≤ n then List.map (List.cons x) (f x) else []).Disjoint
+                (if y ^ i ≤ n then List.map (List.cons y) (f y) else []))
             l
   [eqc] False propositions
     [prop] List.Pairwise
           (fun x y =>
-            (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
-              (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
+            (if x ^ i ≤ n then List.map (List.cons x) (f x) else []).Disjoint
+              (if y ^ i ≤ n then List.map (List.cons y) (f y) else []))
           l
 -/
 #guard_msgs in
diff --git a/tests/elab/grind_array_attach.lean b/tests/elab/grind_array_attach.lean
index 1b781b134e37..dce4f2da3588 100644
--- a/tests/elab/grind_array_attach.lean
+++ b/tests/elab/grind_array_attach.lean
@@ -6,7 +6,8 @@ reprove pmap_empty pmap_push attach_empty attachWith_empty by grind
 reprove map_pmap pmap_map attach_push attachWith_push pmap_eq_map_attach pmap_eq_attachWith by grind
 reprove attach_map_val attach_map_subtype_val attachWith_map_val attachWith_map_subtype_val by grind
 reprove pmap_attach pmap_attachWith by grind
-reprove attach_map attachWith_map map_attachWith map_attachWith_eq_pmap map_attach_eq_pmap by grind
+-- Removed attachWith_map
+reprove attach_map map_attachWith map_attachWith_eq_pmap map_attach_eq_pmap by grind
 reprove pmap_pmap pmap_append pmap_append' attach_append attachWith_append by grind
 reprove pmap_reverse reverse_pmap attachWith_reverse reverse_attachWith attach_reverse reverse_attach by grind
 reprove back?_pmap back?_attachWith back?_attach by grind
@@ -19,7 +20,8 @@ reprove pmap_empty pmap_push attach_empty attachWith_empty by grind
 reprove map_pmap pmap_map attach_push attachWith_push pmap_eq_map_attach pmap_eq_attachWith by grind
 reprove attach_map_val attach_map_subtype_val attachWith_map_val attachWith_map_subtype_val by grind
 reprove pmap_attach pmap_attachWith by grind
-reprove attach_map attachWith_map map_attachWith map_attachWith_eq_pmap map_attach_eq_pmap by grind
+-- Removed attachWith_map
+reprove attach_map map_attachWith map_attachWith_eq_pmap map_attach_eq_pmap by grind
 reprove pmap_pmap pmap_append pmap_append' attach_append attachWith_append by grind
 reprove pmap_reverse reverse_pmap attachWith_reverse reverse_attachWith attach_reverse reverse_attach by grind
 reprove back?_pmap back?_attachWith back?_attach by grind
@@ -36,7 +38,8 @@ reprove pmap_nil pmap_cons attach_nil attachWith_nil by grind
 reprove map_pmap pmap_map attach_cons attachWith_cons pmap_eq_map_attach pmap_eq_attachWith by grind
 reprove attach_map_val attach_map_subtype_val attachWith_map_val attachWith_map_subtype_val by grind
 reprove pmap_attach pmap_attachWith by grind
-reprove attach_map attachWith_map map_attachWith map_attachWith_eq_pmap map_attach_eq_pmap by grind
+-- Removed attachWith_map
+reprove attach_map map_attachWith map_attachWith_eq_pmap map_attach_eq_pmap by grind
 reprove pmap_pmap pmap_append pmap_append' attach_append attachWith_append by grind
 reprove pmap_reverse reverse_pmap attachWith_reverse reverse_attachWith attach_reverse reverse_attach by grind
 reprove getLast?_pmap getLast?_attachWith getLast?_attach by grind
diff --git a/tests/elab/grind_indexmap_trace.lean b/tests/elab/grind_indexmap_trace.lean
index d1d33a2438d9..b18ebe259841 100644
--- a/tests/elab/grind_indexmap_trace.lean
+++ b/tests/elab/grind_indexmap_trace.lean
@@ -149,7 +149,7 @@ info: Try these:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #bd4f
+    cases #bcd5
     · cases #54dd
       · instantiate only
       · instantiate only
@@ -164,7 +164,7 @@ info: Try these:
         · instantiate only
           instantiate only [= HashMap.contains_insert]
   [apply] finish only [= mem_indices_of_mem, insert, =_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos,
-    = HashMap.contains_insert, #bd4f, #54dd, #2eb4, #cc2e]
+    = HashMap.contains_insert, #bcd5, #54dd, #2eb4, #cc2e]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) :
@@ -176,7 +176,7 @@ info: Try these:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #bd4f
+    cases #bcd5
     · cases #54dd
       · instantiate only
       · instantiate only
@@ -191,7 +191,7 @@ info: Try these:
         · instantiate only
           instantiate only [= HashMap.contains_insert]
   [apply] finish only [= mem_indices_of_mem, insert, =_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos,
-    = HashMap.contains_insert, #bd4f, #54dd, #2eb4, #cc2e]
+    = HashMap.contains_insert, #bcd5, #54dd, #2eb4, #cc2e]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) :
@@ -203,21 +203,27 @@ example (m : IndexMap α β) (a a' : α) (b : β) :
   grind =>
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #bd4f
+    cases #bcd5
     · cases #54dd
       · instantiate only
       · instantiate only
         instantiate only [= HashMap.contains_insert]
     · cases #2eb4
-      · cases #cc2e <;> finish only [= HashMap.contains_insert]
-      · cases #54dd <;> finish only [= HashMap.contains_insert]
+      · cases #cc2e
+        · instantiate only
+        · instantiate only
+          instantiate only [= HashMap.contains_insert]
+      · cases #54dd
+        · instantiate only
+        · instantiate only
+          instantiate only [= HashMap.contains_insert]
 
 example (m : IndexMap α β) (a a' : α) (b : β) :
     a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
   grind =>
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #bd4f
+    cases #bcd5
     · cases #54dd
       · instantiate only
       · instantiate only