diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 4867b143eb..0414b261c2 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -775,7 +775,7 @@ private def cacheResult (cacheKey : SynthInstanceCacheKey) (abstResult? : Option
     else
       modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some abstResult) }
 
-def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
+def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
   withTraceNode `Meta.synthInstance
@@ -801,6 +801,9 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
       cacheResult cacheKey abstResult? result?
       return result?
 
+def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
+  synthInstanceCore? type maxResultSize?
+
 /--
   Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if
   instance cannot be synthesized right now because `type` contains metavariables. -/
diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index 230125ed19..43a6ca843e 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -33,6 +33,7 @@ import Lean.Meta.Tactic.Grind.MBTC
 import Lean.Meta.Tactic.Grind.Lookahead
 import Lean.Meta.Tactic.Grind.LawfulEqCmp
 import Lean.Meta.Tactic.Grind.ReflCmp
+import Lean.Meta.Tactic.Grind.SynthInstance
 
 namespace Lean
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean
index 2a4e88bc89..f1d9a492c9 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean
@@ -7,6 +7,8 @@ prelude
 import Init.Grind.Ring.Field
 import Init.Grind.Ring.Envelope
 import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.SynthInstance
+import Lean.Meta.Tactic.Grind.Arith.Insts
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
 
 namespace Lean.Meta.Grind.Arith.CommRing
@@ -23,16 +25,12 @@ def denoteNumCore (u : Level) (type : Expr) (semiringInst : Expr) (negFn : Expr)
 private def internalizeFn (fn : Expr) : GoalM Expr := do
   shareCommon (← canon fn)
 
-private def getUnaryFn (type : Expr)(u : Level) (instDeclName : Name) (declName : Name) : GoalM Expr := do
-  let instType := mkApp (mkConst instDeclName [u]) type
-  let .some inst ← trySynthInstance instType
-    | throwError "`grind ring` failed to find instance{indentExpr instType}"
+private def getUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) : GoalM Expr := do
+  let inst ← synthInstance <| mkApp (mkConst instDeclName [u]) type
   internalizeFn <| mkApp2 (mkConst declName [u]) type inst
 
-private def getBinHomoFn (type : Expr)(u : Level) (instDeclName : Name) (declName : Name) : GoalM Expr := do
-  let instType := mkApp3 (mkConst instDeclName [u, u, u]) type type type
-  let .some inst ← trySynthInstance instType
-    | throwError "`grind ring` failed to find instance{indentExpr instType}"
+private def getBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) : GoalM Expr := do
+  let inst ← synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
   internalizeFn <| mkApp4 (mkConst declName [u, u, u]) type type type inst
 
 -- Remark: we removed consistency checks such as the one that ensures `HAdd` instance matches `Semiring.toAdd`
@@ -57,9 +55,7 @@ private def getInvFn (type : Expr) (u : Level) : GoalM Expr := do
   getUnaryFn type u ``Inv ``Inv.inv
 
 private def getPowFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM Expr := do
-  let instType := mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
-  let .some inst ← trySynthInstance instType |
-    throwError "failed to find instance for ring power operator{indentExpr instType}"
+  let inst ← synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
   let inst' := mkApp2 (mkConst ``Grind.Semiring.toHPow [u]) type semiringInst
   unless (← withDefault <| isDefEq inst inst') do
     throwError "instance for power operator{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}"
@@ -74,7 +70,7 @@ private def getIntCastFn (type : Expr) (u : Level) (ringInst : Expr) : GoalM Exp
   -- does not guarantee that an `IntCast α` will be available.
   -- When both are present we verify that they are defeq,
   -- and otherwise fall back to the field of the `Ring α` instance that we already have.
-  let inst ← match (← trySynthInstance instType).toOption with
+  let inst ← match (← synthInstance? instType) with
   | none => pure inst'
   | some inst =>
     unless (← withDefault <| isDefEq inst inst') do
@@ -91,7 +87,7 @@ private def getNatCastFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM
   -- does not guarantee that an `NatCast α` will be available.
   -- When both are present we verify that they are defeq,
   -- and otherwise fall back to the field of the `Semiring α` instance that we already have.
-  let inst ← match (← trySynthInstance instType).toOption with
+  let inst ← match (← synthInstance? instType) with
   | none => pure inst'
   | some inst =>
     unless (← withDefault <| isDefEq inst inst') do
@@ -121,20 +117,16 @@ def getRingId? (type : Expr) : GoalM (Option Nat) := do
 where
   go? : GoalM (Option Nat) := do
     let u ← getDecLevel type
-    let semiring := mkApp (mkConst ``Grind.Semiring [u]) type
-    let .some semiringInst ← trySynthInstance semiring | return none
-    let ring := mkApp (mkConst ``Grind.Ring [u]) type
-    let .some ringInst ← trySynthInstance ring | return none
-    let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type
-    let .some commSemiringInst ← trySynthInstance commSemiring | return none
     let commRing := mkApp (mkConst ``Grind.CommRing [u]) type
-    let .some commRingInst ← trySynthInstance commRing | return none
+    let some commRingInst ← synthInstance? commRing | return none
+    let ringInst := mkApp2 (mkConst ``Grind.CommRing.toRing [u]) type commRingInst
+    let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
+    let commSemiringInst := mkApp2 (mkConst ``Grind.CommRing.toCommSemiring [u]) type semiringInst
     trace_goal[grind.ring] "new ring: {type}"
     let charInst? ← getIsCharInst? u type semiringInst
     let noZeroDivInst? ← getNoZeroDivInst? u type
     trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
-    let field := mkApp (mkConst ``Grind.Field [u]) type
-    let fieldInst? : Option Expr ← LOption.toOption <$> trySynthInstance field
+    let fieldInst? ← synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
     let addFn ← getAddFn type u
     let mulFn ← getMulFn type u
     let subFn ← getSubFn type u
@@ -169,19 +161,18 @@ def getSemiringId? (type : Expr) : GoalM (Option Nat) := do
 where
   go? : GoalM (Option Nat) := do
     let u ← getDecLevel type
-    let semiring := mkApp (mkConst ``Grind.Semiring [u]) type
-    let .some semiringInst ← trySynthInstance semiring | return none
     let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type
-    let .some commSemiringInst ← trySynthInstance commSemiring | return none
+    let some commSemiringInst ← synthInstance? commSemiring | return none
+    let semiringInst := mkApp2 (mkConst ``Grind.CommSemiring.toSemiring [u]) type commSemiringInst
     let toQFn ← internalizeFn <| mkApp2 (mkConst ``Grind.Ring.OfSemiring.toQ [u]) type semiringInst
     let addFn ← getAddFn type u
     let mulFn ← getMulFn type u
     let powFn ← getPowFn type u semiringInst
     let natCastFn ← getNatCastFn type u semiringInst
     let add := mkApp (mkConst ``Add [u]) type
-    let .some addInst ← trySynthInstance add | return none
+    let some addInst ← synthInstance? add | return none
     let addRightCancel := mkApp2 (mkConst ``Grind.AddRightCancel [u]) type addInst
-    let addRightCancelInst? ← LOption.toOption <$> trySynthInstance addRightCancel
+    let addRightCancelInst? ← synthInstance? addRightCancel
     let q ← shareCommon (← canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
     let some ringId ← getRingId? q
       | throwError "`grind` unexpected failure, failure to initialize ring{indentExpr q}"
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean
index 9f5bb5eedd..c7030ebe5c 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.ToIntLemmas
+import Lean.Meta.Tactic.Grind.SynthInstance
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 
@@ -20,38 +21,38 @@ private def checkDecl (declName : Name) : MetaM Unit := do
   unless (← getEnv).contains declName do
     throwMissingDecl declName
 
-private def mkOfNatThm? (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) : MetaM (Option Expr) := do
+private def mkOfNatThm? (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) : GoalM (Option Expr) := do
   -- ∀ n, OfNat α n
   let ofNat := mkForall `n .default (mkConst ``Nat) (mkApp2 (mkConst ``OfNat [u]) type (mkBVar 0))
-  let .some ofNatInst ← trySynthInstance ofNat
+  let some ofNatInst ← synthInstance? ofNat
     | reportMissingToIntAdapter type ofNat; return none
   let toIntOfNat := mkApp4 (mkConst ``Grind.ToInt.OfNat [u]) type ofNatInst rangeExpr toIntInst
-  let .some toIntOfNatInst ← trySynthInstance toIntOfNat
+  let some toIntOfNatInst ← synthInstance? toIntOfNat
     | reportMissingToIntAdapter type toIntOfNat; return none
   return mkApp5 (mkConst ``Grind.ToInt.ofNat_eq [u]) type rangeExpr toIntInst ofNatInst toIntOfNatInst
 
 /-- Helper function for `mkSimpleOpThm?` and `mkPowThm?` -/
-private def mkSimpleOpThmCore? (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) (op : Expr) (opSuffix : Name) (thmName : Name) : MetaM (Option Expr) := do
-  let .some opInst ← trySynthInstance op | return none
+private def mkSimpleOpThmCore? (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) (op : Expr) (opSuffix : Name) (thmName : Name) : GoalM (Option Expr) := do
+  let some opInst ← synthInstance? op | return none
   let toIntOpName := ``Grind.ToInt ++ opSuffix
   checkDecl toIntOpName
   let toIntOp := mkApp4 (mkConst toIntOpName [u]) type opInst rangeExpr toIntInst
-  let .some toIntOpInst ← trySynthInstance toIntOp
+  let some toIntOpInst ← synthInstance? toIntOp
     | reportMissingToIntAdapter type toIntOp; return none
   checkDecl thmName
   return mkApp5 (mkConst thmName [u]) type rangeExpr toIntInst opInst toIntOpInst
 
 /-- Simpler version of `mkBinOpThms` for operators that have only one congruence theorem. -/
-private def mkSimpleOpThm? (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) (opBaseName : Name) (thmName : Name) : MetaM (Option Expr) := do
+private def mkSimpleOpThm? (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) (opBaseName : Name) (thmName : Name) : GoalM (Option Expr) := do
   let op := mkApp (mkConst opBaseName [u]) type
   mkSimpleOpThmCore? type u toIntInst rangeExpr op opBaseName thmName
 
 /-- Simpler version of `mkBinOpThms` for operators that have only one congruence theorem. -/
-private def mkPowThm? (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) : MetaM (Option Expr) := do
+private def mkPowThm? (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) : GoalM (Option Expr) := do
   let op := mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
   mkSimpleOpThmCore? type u toIntInst rangeExpr op `Pow ``Grind.ToInt.pow_congr
 
-private def mkBinOpThms (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) (range : Grind.IntInterval) (opBaseName : Name) (thmName : Name) : MetaM ToIntThms := do
+private def mkBinOpThms (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) (range : Grind.IntInterval) (opBaseName : Name) (thmName : Name) : GoalM ToIntThms := do
   let some c ← mkSimpleOpThm? type u toIntInst rangeExpr opBaseName thmName | return {}
   let opInst := c.appFn!.appArg!
   let toIntOpInst := c.appArg!
@@ -113,7 +114,7 @@ where
     let some u ← decLevel? u' | return none
     let rangeExpr ← mkFreshExprMVar (mkConst ``Grind.IntInterval)
     let toIntType := mkApp2 (mkConst ``Grind.ToInt [u]) type rangeExpr
-    let .some toIntInst ← trySynthInstance toIntType |
+    let some toIntInst ← synthInstance? toIntType |
       trace[grind.debug.cutsat.toInt] "failed to synthesize {indentExpr toIntType}"
       return none
     let rangeExpr ← instantiateMVars rangeExpr
@@ -128,18 +129,18 @@ where
     let ofDiseq := mkApp3 (mkConst ``Grind.ToInt.of_diseq [u]) type rangeExpr toIntInst
     let (ofLE?, ofNotLE?) ← do
       let toLE := mkApp (mkConst ``LE [u]) type
-      let .some leInst ← LOption.toOption <$> trySynthInstance toLE | pure (none, none)
+      let some leInst ← synthInstance? toLE | pure (none, none)
       let toIntLE := mkApp4 (mkConst ``Grind.ToInt.LE [u]) type leInst rangeExpr toIntInst
-      let .some toIntLEInst ← LOption.toOption <$> trySynthInstance toIntLE
+      let some toIntLEInst ← synthInstance? toIntLE
         | reportMissingToIntAdapter type toIntLE; pure (none, none)
       let ofLE := mkApp5 (mkConst ``Grind.ToInt.of_le [u]) type rangeExpr toIntInst leInst toIntLEInst
       let ofNotLE := mkApp5 (mkConst ``Grind.ToInt.of_not_le [u]) type rangeExpr toIntInst leInst toIntLEInst
       pure (some ofLE, some ofNotLE)
     let (ofLT?, ofNotLT?) ← do
       let toLT := mkApp (mkConst ``LT [u]) type
-      let .some ltInst ← LOption.toOption <$> trySynthInstance toLT | pure (none, none)
+      let some ltInst ← synthInstance? toLT | pure (none, none)
       let toIntLT := mkApp4 (mkConst ``Grind.ToInt.LT [u]) type ltInst rangeExpr toIntInst
-      let .some toIntLTInst ← LOption.toOption <$> trySynthInstance toIntLT
+      let some toIntLTInst ← synthInstance? toIntLT
         | reportMissingToIntAdapter type toIntLT; pure (none, none)
       let ofLT := mkApp5 (mkConst ``Grind.ToInt.of_lt [u]) type rangeExpr toIntInst ltInst toIntLTInst
       let ofNotLT := mkApp5 (mkConst ``Grind.ToInt.of_not_lt [u]) type rangeExpr toIntInst ltInst toIntLTInst
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean b/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean
new file mode 100644
index 0000000000..e6761a7278
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean
@@ -0,0 +1,26 @@
+/-
+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
+-/
+prelude
+import Lean.Meta.Tactic.Grind.SynthInstance
+
+namespace Lean.Meta.Grind.Arith
+
+def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : GoalM (Option (Expr × Nat)) := do withNewMCtxDepth do
+  let n ← mkFreshExprMVar (mkConst ``Nat)
+  let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type semiringInst n
+  let some charInst ← synthInstance? charType | pure none
+  let n ← instantiateMVars n
+  let some n ← evalNat n |>.run
+    | pure none
+  pure <| some (charInst, n)
+
+def getNoZeroDivInst? (u : Level) (type : Expr) : GoalM (Option Expr) := do
+  let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type
+  let some hmulInst ← synthInstance? hmulType | return none
+  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst
+  synthInstance? noZeroDivType
+
+end Lean.Meta.Grind.Arith
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
index 510c2bd078..be33e40a3d 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind.Ordered.Module
 import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.SynthInstance
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
 import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Arith.Linear.Util
@@ -75,28 +76,15 @@ where
   go? : GoalM (Option Nat) := do
     let u ← getDecLevel type
     let rec getInst? (declName : Name) : GoalM (Option Expr) := do
-      let instType := mkApp (mkConst declName [u]) type
-      return LOption.toOption (← trySynthInstance instType)
+      synthInstance? <| mkApp (mkConst declName [u]) type
     let rec getInst (declName : Name) : GoalM Expr := do
-      let instType := mkApp (mkConst declName [u]) type
-      let .some inst ← trySynthInstance instType
-        | throwError "`grind linarith` failed to find instance{indentExpr instType}"
-      return inst
+      synthInstance <| mkApp (mkConst declName [u]) type
     let rec getBinHomoInst (declName : Name) : GoalM Expr := do
-      let instType := mkApp3 (mkConst declName [u, u, u]) type type type
-      let .some inst ← trySynthInstance instType
-        | throwError "`grind linarith` failed to find instance{indentExpr instType}"
-      return inst
+      synthInstance <| mkApp3 (mkConst declName [u, u, u]) type type type
     let rec getHMulIntInst : GoalM Expr := do
-      let instType := mkApp3 (mkConst ``HMul [0, u, u]) Int.mkType type type
-      let .some inst ← trySynthInstance instType
-        | throwError "`grind linarith` failed to find instance{indentExpr instType}"
-      return inst
+      synthInstance <| mkApp3 (mkConst ``HMul [0, u, u]) Int.mkType type type
     let rec getHMulNatInst : GoalM Expr := do
-      let instType := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type
-      let .some inst ← trySynthInstance instType
-        | throwError "`grind linarith` failed to find instance{indentExpr instType}"
-      return inst
+      synthInstance <| mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type
     let rec checkToFieldDefEq? (parentInst? : Option Expr) (inst? : Option Expr) (toFieldName : Name) : GoalM (Option Expr) := do
       let some parentInst := parentInst? | return none
       let some inst := inst? | return none
@@ -113,12 +101,12 @@ where
       let heteroToField := mkApp2 (mkConst toHeteroName [u]) type toField
       ensureDefEq parentInst heteroToField
     let some intModuleInst ← getInst? ``Grind.IntModule | return none
-    let addCommGroupInst ← getInst ``Grind.AddCommGroup
-    let addCommMonoidInst ← getInst ``Grind.AddCommMonoid
+    let addCommGroupInst := mkApp2 (mkConst ``Grind.IntModule.toAddCommGroup [u]) type intModuleInst
+    let addCommMonoidInst := mkApp2 (mkConst ``Grind.AddCommGroup.toAddCommMonoid [u]) type addCommGroupInst
     let zeroInst ← getInst ``Zero
     let zero ← internalizeConst <| mkApp2 (mkConst ``Zero.zero [u]) type zeroInst
     let ofNatZeroType := mkApp2 (mkConst ``OfNat [u]) type (mkRawNatLit 0)
-    let some ofNatZeroInst := LOption.toOption (← trySynthInstance ofNatZeroType) | return none
+    let some ofNatZeroInst ← synthInstance? ofNatZeroType | return none
     -- `ofNatZero` is used internally, we don't need to internalize
     let ofNatZero ← preprocess <| mkApp3 (mkConst ``OfNat.ofNat [u]) type (mkRawNatLit 0) ofNatZeroInst
     ensureDefEq zero ofNatZero
@@ -132,8 +120,6 @@ where
     let zsmulFn ← internalizeFn <| mkApp4 (mkConst ``HMul.hMul [0, u, u]) Int.mkType type type zsmulInst
     let nsmulInst ← getHMulNatInst
     let nsmulFn ← internalizeFn <| mkApp4 (mkConst ``HMul.hMul [0, u, u]) Nat.mkType type type nsmulInst
-    ensureToFieldDefEq addCommGroupInst intModuleInst ``Grind.IntModule.toAddCommGroup
-    ensureToFieldDefEq addCommMonoidInst addCommGroupInst ``Grind.AddCommGroup.toAddCommMonoid
     ensureToFieldDefEq zeroInst addCommMonoidInst ``Grind.AddCommMonoid.toZero
     ensureToHomoFieldDefEq addInst addCommMonoidInst ``Grind.AddCommMonoid.toAdd ``instHAdd
     ensureToHomoFieldDefEq subInst addCommGroupInst ``Grind.AddCommGroup.toSub ``instHSub
@@ -142,8 +128,7 @@ where
     ensureToFieldDefEq nsmulInst intModuleInst ``Grind.IntModule.nsmul
     let preorderInst? ← getInst? ``Grind.Preorder
     let orderedAddInst? ← if let some preorderInst := preorderInst? then
-      let isOrderedType := mkApp3 (mkConst ``Grind.OrderedAdd [u]) type addInst preorderInst
-      pure <| LOption.toOption (← trySynthInstance isOrderedType)
+      synthInstance? <| mkApp3 (mkConst ``Grind.OrderedAdd [u]) type addInst preorderInst
     else
       pure none
     let preorderInst? := if orderedAddInst?.isNone then none else preorderInst?
@@ -161,11 +146,11 @@ where
       pure (none, none)
     let rec getHSMulFn? : GoalM (Option Expr) := do
       let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Int.mkType type type
-      let .some smulInst ← trySynthInstance smulType | return none
+      let some smulInst ← synthInstance? smulType | return none
       internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Int.mkType type smulInst smulInst
     let rec getHSMulNatFn? : GoalM (Option Expr) := do
       let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Nat.mkType type type
-      let .some smulInst ← trySynthInstance smulType | return none
+      let some smulInst ← synthInstance? smulType | return none
       internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Nat.mkType type smulInst smulInst
     let zsmulFn? ← getHSMulFn?
     let nsmulFn? ← getHSMulNatFn?
@@ -190,7 +175,7 @@ where
       let some semiringInst := semiringInst? | return none
       let some preorderInst := preorderInst? | return none
       let isOrdType := mkApp3 (mkConst ``Grind.OrderedRing [u]) type semiringInst preorderInst
-      let .some inst ← trySynthInstance isOrdType
+      let some inst ← synthInstance? isOrdType
         | reportIssue! "type has a `Preorder` and is a `Semiring`, but is not an ordered ring, failed to synthesize{indentExpr isOrdType}"
           return none
       return some inst
@@ -198,9 +183,8 @@ where
     let charInst? ← if let some semiringInst := semiringInst? then getIsCharInst? u type semiringInst else pure none
     let rec getNoNatZeroDivInst? : GoalM (Option Expr) := do
       let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type
-      let .some hmulInst ← trySynthInstance hmulNat | return none
-      let noNatZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst
-      return LOption.toOption (← trySynthInstance noNatZeroDivType)
+      let some hmulInst ← synthInstance? hmulNat | return none
+      synthInstance? <| mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst
     let noNatDivInst? ← getNoNatZeroDivInst?
     let id := (← get').structs.size
     let struct : Struct := {
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean b/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean
index 829f138c1c..be855616d2 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean
@@ -7,13 +7,14 @@ prelude
 import Init.Grind.Ring.Basic
 import Init.Simproc
 import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Grind.SynthInstance
 
 namespace Lean.Meta.Grind.Arith
 
 private def mkSemiringThm (declName : Name) (α : Expr) : MetaM (Option Expr) := do
   let some u ← getDecLevel? α | return none
   let semiring := mkApp (mkConst ``Grind.Semiring [u]) α
-  let .some semiringInst ← trySynthInstance semiring | return none
+  let some semiringInst ← synthInstanceMeta? semiring | return none
   return mkApp2 (mkConst declName [u]) α semiringInst
 
 /--
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Util.lean
index 21c0f9c2c0..1b0e8afd0d 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Util.lean
@@ -152,21 +152,6 @@ def isIntModuleVirtualParent (parent? : Option Expr) : Bool :=
   | none => false
   | some parent => parent == getIntModuleVirtualParent
 
-def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : MetaM (Option (Expr × Nat)) := do withNewMCtxDepth do
-  let n ← mkFreshExprMVar (mkConst ``Nat)
-  let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type semiringInst n
-  let .some charInst ← trySynthInstance charType | pure none
-  let n ← instantiateMVars n
-  let some n ← evalNat n |>.run
-    | pure none
-  pure <| some (charInst, n)
-
-def getNoZeroDivInst? (u : Level) (type : Expr) : MetaM (Option Expr) := do
-  let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type
-  let .some hmulInst ← trySynthInstance hmulType | return none
-  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst
-  LOption.toOption <$> trySynthInstance noZeroDivType
-
 @[specialize] def split (cs : PArray α) (getCoeff : α → Int) : PArray α × Array (Int × α) := Id.run do
   let mut cs' := {}
   let mut todo := #[]
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index ff36e11b90..e46676a38d 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -135,7 +135,7 @@ private def matchArg? (c : Choice) (pArg : Expr) (eArg : Expr) : OptionT GoalM C
     assign? c pArg.bvarIdx! eArg
   else if let some pArg := groundPattern? pArg then
     /-
-    We need to use `withReducibleAndIntances` because ground patterns are often instances.
+    We need to use `withReducibleAndInstances` because ground patterns are often instances.
     Here is an example
     ```
     instance : Max Nat where
@@ -348,7 +348,7 @@ private def synthesizeInsts (mvars : Array Expr) (bis : Array BinderInfo) : Opti
   for mvar in mvars, bi in bis do
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
-      unless (← synthesizeInstanceAndAssign mvar type) do
+      unless (← synthInstanceAndAssign mvar type) do
         reportIssue! "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
         failure
 
diff --git a/src/Lean/Meta/Tactic/Grind/Ext.lean b/src/Lean/Meta/Tactic/Grind/Ext.lean
index e98dda44f8..6abd7c192e 100644
--- a/src/Lean/Meta/Tactic/Grind/Ext.lean
+++ b/src/Lean/Meta/Tactic/Grind/Ext.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.SynthInstance
 
 namespace Lean.Meta.Grind
 /-! Extensionality theorems support. -/
@@ -20,7 +21,7 @@ def instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) : GoalM Unit := with
   for mvar in mvars, bi in bis do
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
-      unless (← synthesizeInstanceAndAssign mvar type) do
+      unless (← synthInstanceAndAssign mvar type) do
         reportIssue! "failed to synthesize instance when instantiating extensionality theorem `{thm.declName}` for {indentExpr e}"
         return ()
   -- Remark: `proof c mvars` has type `e`
diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
index 7f9f79c717..c48bf112c3 100644
--- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean
+++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
@@ -256,7 +256,7 @@ builtin_simproc_decl simpExists (Exists _) := fun e => do
     else
       let u := ex.constLevels!
       let nonempty := mkApp (mkConst ``Nonempty u) α
-      if let .some nonemptyInst ← trySynthInstance nonempty then
+      if let some nonemptyInst ← synthInstanceMeta? nonempty then
         return .visit { expr := b, proof? := mkApp3 (mkConst ``Grind.exists_const u) α nonemptyInst b }
   return .continue
 
diff --git a/src/Lean/Meta/Tactic/Grind/LawfulEqCmp.lean b/src/Lean/Meta/Tactic/Grind/LawfulEqCmp.lean
index 6bafda34bd..106511db58 100644
--- a/src/Lean/Meta/Tactic/Grind/LawfulEqCmp.lean
+++ b/src/Lean/Meta/Tactic/Grind/LawfulEqCmp.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.SynthInstance
 
 /-!
 Support for type class `LawfulEqCmp`.
@@ -38,7 +39,7 @@ where
     let u ← getLevel α
     let some u ← decLevel? u | return none
     let lawfulEqCmp := mkApp2 (mkConst ``Std.LawfulEqCmp [u]) α op
-    let .some lawfulEqCmpInst ← trySynthInstance lawfulEqCmp | return none
+    let some lawfulEqCmpInst ← synthInstanceMeta? lawfulEqCmp | return none
     return some <| mkApp3 (mkConst ``Std.LawfulEqCmp.eq_of_compare [u]) α op lawfulEqCmpInst
 
 def propagateLawfulEqCmp (e : Expr) : GoalM Unit := do
diff --git a/src/Lean/Meta/Tactic/Grind/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Propagate.lean
index 31b5efd365..e51e36ab6c 100644
--- a/src/Lean/Meta/Tactic/Grind/Propagate.lean
+++ b/src/Lean/Meta/Tactic/Grind/Propagate.lean
@@ -174,11 +174,8 @@ builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
       for thm in (← getExtTheorems α) do
         instantiateExtTheorem thm e
 
-private def getLawfulBEqInst? (u : List Level) (α : Expr) (binst : Expr) : MetaM (Option Expr) := do
-  let lawfulBEq := mkApp2 (mkConst ``LawfulBEq u) α binst
-  let .some linst ← trySynthInstance lawfulBEq | return none
-  return some linst
-
+private def getLawfulBEqInst? (u : List Level) (α : Expr) (binst : Expr) : GoalM (Option Expr) := do
+  synthInstance? <| mkApp2 (mkConst ``LawfulBEq u) α binst
 /-
 Note about `BEq.beq`
 Given `a b : α` in a context where we have `[BEq α] [LawfulBEq α]`
diff --git a/src/Lean/Meta/Tactic/Grind/ReflCmp.lean b/src/Lean/Meta/Tactic/Grind/ReflCmp.lean
index 0b18b0128e..7a94d70657 100644
--- a/src/Lean/Meta/Tactic/Grind/ReflCmp.lean
+++ b/src/Lean/Meta/Tactic/Grind/ReflCmp.lean
@@ -5,6 +5,7 @@ Authors: Kim Morrison
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.SynthInstance
 
 /-!
 Support for type class `ReflCmp`.
@@ -38,7 +39,7 @@ where
     let u ← getLevel α
     let some u ← decLevel? u | return none
     let reflCmp := mkApp2 (mkConst ``Std.ReflCmp [u]) α op
-    let .some reflCmpInst ← trySynthInstance reflCmp | return none
+    let some reflCmpInst ← synthInstanceMeta? reflCmp | return none
     return some <| mkApp3 (mkConst ``Std.ReflCmp.cmp_eq_of_eq [u]) α op reflCmpInst
 
 def propagateReflCmp (e : Expr) : GoalM Unit := do
diff --git a/src/Lean/Meta/Tactic/Grind/SynthInstance.lean b/src/Lean/Meta/Tactic/Grind/SynthInstance.lean
new file mode 100644
index 0000000000..b7f18100c4
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/SynthInstance.lean
@@ -0,0 +1,33 @@
+/-
+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
+-/
+prelude
+import Lean.Meta.SynthInstance
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind
+
+def synthInstanceMeta? (type : Expr) : MetaM (Option Expr) := do profileitM Exception "grind typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
+  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
+
+end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index b0ea64a1f8..bf580c0f64 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -1539,14 +1539,6 @@ def getExtTheorems (type : Expr) : GoalM (Array Ext.ExtTheorem) := do
     modify fun s => { s with extThms := s.extThms.insert { expr := type } thms }
     return thms
 
-/--
-Helper function for instantiating a type class `type`, and
-then using the result to perform `isDefEq x val`.
--/
-def synthesizeInstanceAndAssign (x type : Expr) : MetaM Bool := do
-  let .some val ← trySynthInstance type | return false
-  isDefEq x val
-
 /-- Add a new lookahead candidate. -/
 def addLookaheadCandidate (sinfo : SplitInfo) : GoalM Unit := do
   trace_goal[grind.lookahead.add] "{sinfo.getExpr}"