test:

and mark places where it is not safe to use the cheaper and more
efficient tests.

src/Lean/Expr.lean

@@ -708,7 +708,7 @@ def mkSimpleThunk (type : Expr) : Expr :=
   .lit l
 
 /--
-Return the "raw" natural number `.lit (.natVal n)`.
+Returns the "raw" natural number `.lit (.natVal n)`.
 This is not the default representation used by the Lean frontend.
 See `mkNatLit`.
 -/
@@ -716,13 +716,21 @@ See `mkNatLit`.
   mkLit (.natVal n)
 
 /--
-Return a natural number literal used in the frontend. It is a `OfNat.ofNat` application.
+Returns `instOfNatNat n : OfNat Nat n`
+-/
+def mkInstOfNatNat (n : Expr) : Expr :=
+  mkApp (mkConst ``instOfNatNat) n
+
+def mkNatLitCore (n : Expr) : Expr :=
+  mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Nat) n (mkInstOfNatNat n)
+
+/--
+Returns a natural number literal used in the frontend. It is a `OfNat.ofNat` application.
 Recall that all theorems and definitions containing numeric literals are encoded using
 `OfNat.ofNat` applications in the frontend.
 -/
 @[match_pattern, expose] def mkNatLit (n : Nat) : Expr :=
-  let r := mkRawNatLit n
-  mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Nat) r (mkApp (mkConst ``instOfNatNat) r)
+  mkNatLitCore (mkRawNatLit n)
 
 /-- Return the string literal `.lit (.strVal s)` -/
 @[match_pattern, expose] def mkStrLit (s : String) : Expr :=

src/Lean/Meta/Basic.lean

@@ -2480,6 +2480,14 @@ abbrev isDefEqGuarded (t s : Expr) : MetaM Bool :=
 def isDefEqNoConstantApprox (t s : Expr) : MetaM Bool :=
   approxDefEq <| isDefEq t s
 
+/-- Similar to `isDefEq`, but ensures default transparency is used. -/
+def isDefEqD (t s : Expr) : MetaM Bool :=
+  withDefault <| isDefEq t s
+
+/-- Similar to `isDefEq`, but ensures that only reducible definitions and instances can be reduced. -/
+def isDefEqI (t s : Expr) : MetaM Bool :=
+  withReducibleAndInstances <| isDefEq t s
+
 /--
 Returns `true` if `mvarId := val` was successfully assigned.
 This method uses the same assignment validation performed by `isDefEq`, but it does not check whether the types match.

src/Lean/Meta/IntInstTesters.lean

@@ -14,6 +14,11 @@ namespace Lean.Meta
 /-!
 Functions for testing whether expressions are canonical `Int` instances.
 -/
+namespace Structural
+/-!
+**Note**: Structural tests are *syntactic*. They are more efficient, but
+should be used only in modules that have perform some kind of canonicalization.
+-/
 
 def isInstOfNatInt (e : Expr) : MetaM Bool := do
   let_expr instOfNat _ ← e | return false
@@ -69,4 +74,50 @@ def isInstPowInt (e : Expr) : MetaM Bool := do
 def isInstHPowInt (e : Expr) : MetaM Bool := do
   let_expr instHPow _ _ i ← e | return false
   isInstPowInt i
+end Structural
+
+namespace DefEq
+
+def isInstNegInt (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstNegInt e) then return true
+  isDefEqI e Int.mkInstNeg
+
+def isInstAddInt (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstAddInt e) then return true
+  isDefEqI e Int.mkInstAdd
+
+def isInstHAddInt (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstHAddInt e) then return true
+  isDefEqI e Int.mkInstHAdd
+
+def isInstSubInt (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstSubInt e) then return true
+  isDefEqI e Int.mkInstSub
+
+def isInstHSubInt (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstHSubInt e) then return true
+  isDefEqI e Int.mkInstHSub
+
+def isInstMulInt (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstMulInt e) then return true
+  isDefEqI e Int.mkInstMul
+
+def isInstHMulInt (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstHMulInt e) then return true
+  isDefEqI e Int.mkInstHMul
+
+def isInstLTInt (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstLTInt e) then return true
+  isDefEqI e Int.mkInstLT
+
+def isInstLEInt (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstLEInt e) then return true
+  isDefEqI e Int.mkInstLE
+
+def isInstDvdInt (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstDvdInt e) then return true
+  isDefEqI e (mkConst ``Int.instDvd)
+
+end DefEq
+
 end Lean.Meta

src/Lean/Meta/NatInstTesters.lean

@@ -14,6 +14,11 @@ namespace Lean.Meta
 /-!
 Functions for testing whether expressions are canonical `Nat` instances.
 -/
+namespace Structural
+/-!
+**Note**: Structural tests are *syntactic*. They are more efficient, but
+should be used only in modules that have perform some kind of canonicalization.
+-/
 
 def isInstOfNatNat (e : Expr) : MetaM Bool := do
   let_expr instOfNatNat _ ← e | return false
@@ -66,5 +71,34 @@ def isInstLENat (e : Expr) : MetaM Bool := do
 def isInstDvdNat (e : Expr) : MetaM Bool := do
   let_expr Nat.instDvd ← e | return false
   return true
+end Structural
+
+namespace DefEq
+
+def isInstAddNat (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstAddNat e) then return true
+  isDefEqI e Nat.mkInstAdd
+
+def isInstHAddNat (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstHAddNat e) then return true
+  isDefEqI e Nat.mkInstHAdd
+
+def isInstMulNat (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstMulNat e) then return true
+  isDefEqI e Nat.mkInstMul
+
+def isInstHMulNat (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstHMulNat e) then return true
+  isDefEqI e Nat.mkInstHMul
+
+def isInstLTNat (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstLTNat e) then return true
+  isDefEqI e Nat.mkInstLT
+
+def isInstLENat (e : Expr) : MetaM Bool := do
+  if (← Structural.isInstLENat e) then return true
+  isDefEqI e Nat.mkInstLE
+
+end DefEq
 
 end Lean.Meta

src/Lean/Meta/Offset.lean

@@ -19,6 +19,7 @@ private abbrev withInstantiatedMVars (e : Expr) (k : Expr → OptionT MetaM α)
   else
     k eNew
 
+open Structural in -- TODO FIX
 /--
   Evaluate simple `Nat` expressions.
   Remark: this method assumes the given expression has type `Nat`. -/

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.lean

@@ -14,6 +14,10 @@ import Lean.Meta.NatInstTesters
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 
+/-
+**Note**: It is safe to use (the more efficient) structural instances tests here because `grind` uses the canonicalizer.
+-/
+open Structural in
 builtin_grind_propagator propagatePower ↑HPow.hPow := fun e => do
   -- **Note**: We are not checking whether the `^` instance is the expected ones.
   let_expr HPow.hPow α n α' _ a b := e | return ()

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean

@@ -101,7 +101,7 @@ private def DvdCnstr.assertCore (c : DvdCnstr) : GoalM Unit := do
 
 def propagateIntDvd (e : Expr) : GoalM Unit := do
   let_expr Dvd.dvd _ inst a b ← e | return ()
-  unless (← isInstDvdInt inst) do return ()
+  unless (← Structural.isInstDvdInt inst) do return ()
   let some d ← getIntValue? a
     | reportIssue! "non-linear divisibility constraint found{indentExpr e}"; return ()
   if (← isEqTrue e) then
@@ -113,7 +113,7 @@ def propagateIntDvd (e : Expr) : GoalM Unit := do
 
 def propagateNatDvd (e : Expr) : GoalM Unit := do
   let_expr Dvd.dvd _ inst d₀ a := e | return ()
-  unless (← isInstDvdNat inst) do return ()
+  unless (← Structural.isInstDvdNat inst) do return ()
   let some d ← getNatValue? d₀
     | reportIssue! "non-linear divisibility constraint found{indentExpr e}"; return ()
   if (← isEqTrue e) then

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -217,7 +217,7 @@ where
 
   go (e : Expr) : StateT PropagateMul.State GoalM Unit := do
     let_expr HMul.hMul _ _ _ i a b := e | goVar e
-    if (← isInstHMulInt i) then
+    if (← Structural.isInstHMulInt i) then
       go a; go b
     else
       goVar e
@@ -225,7 +225,7 @@ where
 private def propagateNonlinearDiv (x : Var) : GoalM Bool := do
   let e ← getVar x
   let_expr HDiv.hDiv _ _ _ i a b := e | return false
-  unless (← isInstHDivInt i) do return false
+  unless (← Structural.isInstHDivInt i) do return false
   let some (k, c) ← isExprEqConst? b | return false
   let c' ← if let some a ← getIntValue? a then
     pure { p := .add 1 x (.num (-(a/k))), h := .div k none c : EqCnstr }
@@ -240,7 +240,7 @@ private def propagateNonlinearDiv (x : Var) : GoalM Bool := do
 private def propagateNonlinearMod (x : Var) : GoalM Bool := do
   let e ← getVar x
   let_expr HMod.hMod _ _ _ i a b := e | return false
-  unless (← isInstHModInt i) do return false
+  unless (← Structural.isInstHModInt i) do return false
   let some (k, c) ← isExprEqConst? b | return false
   let c' ← if let some a ← getIntValue? a then
     pure { p := .add 1 x (.num (-(a%k))), h := .mod k none c : EqCnstr }
@@ -255,7 +255,7 @@ private def propagateNonlinearMod (x : Var) : GoalM Bool := do
 private def propagateNonlinearPow (x : Var) : GoalM Bool := do
   let e ← getVar x
   let_expr HPow.hPow _ _ _ i a b := e | return false
-  unless (← isInstHPowInt i) do return false
+  unless (← Structural.isInstHPowInt i) do return false
   let (ka, ca?) ← if let some ka ← getIntValue? a then
     pure (ka, none)
   else if let some (ka, ca) ← isExprEqConst? a then
@@ -590,7 +590,7 @@ private def expandDivMod (a : Expr) (b : Int) : GoalM Unit := do
 
 private def propagateDiv (e : Expr) : GoalM Unit := do
   let_expr HDiv.hDiv _ _ _ inst a b ← e | return ()
-  if (← isInstHDivInt inst) then
+  if (← Structural.isInstHDivInt inst) then
     if let some b ← getIntValue? b then
       expandDivMod a b
     else
@@ -599,7 +599,7 @@ private def propagateDiv (e : Expr) : GoalM Unit := do
 
 private def propagateMod (e : Expr) : GoalM Unit := do
   let_expr HMod.hMod _ _ _ inst a b ← e | return ()
-  if (← isInstHModInt inst) then
+  if (← Structural.isInstHModInt inst) then
     if let some b ← getIntValue? b then
       expandDivMod a b
     else
@@ -645,7 +645,7 @@ private def internalizeIntTerm (e type : Expr) (parent? : Option Expr) (k : Supp
 
 private def propagateNatSub (e : Expr) : GoalM Unit := do
   let_expr HSub.hSub _ _ _ inst a b := e | return ()
-  unless (← isInstHSubNat inst) do return ()
+  unless (← Structural.isInstHSubNat inst) do return ()
   discard <| mkNatVar a
   discard <| mkNatVar b
   pushNewFact <| mkApp2 (mkConst ``Int.Linear.natCast_sub) a b

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean

@@ -130,7 +130,7 @@ private def reportNonNormalized (e : Expr) : GoalM Unit := do
 
 private def toPolyLe? (e : Expr) : GoalM (Option Poly) := do
   let_expr LE.le _ inst a b ← e | return none
-  unless (← isInstLEInt inst) do return none
+  unless (← Structural.isInstLEInt inst) do return none
   let some k ← getIntValue? b
     | reportNonNormalized e; return none
   unless k == 0 do

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean

@@ -29,6 +29,10 @@ def mkNatVar (e : Expr) : GoalM (Expr × Expr) := do
 
 private def intIte : Expr := mkApp (mkConst ``ite [1]) Int.mkType
 
+/-
+**Note**: It is safe to use (the more efficient) structural instances tests here because `grind` uses the canonicalizer.
+-/
+open Structural in
 private partial def natToInt' (e : Expr) : GoalM (Expr × Expr) := do
   match_expr e with
   | HAdd.hAdd _ _ _ inst a b =>
@@ -115,6 +119,10 @@ def assertNatCast (e : Expr) (x : Var) : GoalM Unit := do
 def isNatTerm (e : Expr) : GoalM Bool :=
   return (← get').natToIntMap.contains { expr := e }
 
+/-
+**Note**: It is safe to use (the more efficient) structural instances tests here because `grind` uses the canonicalizer.
+-/
+open Structural in
 private partial def isNonneg (e : Expr) : MetaM Bool := do
   match_expr e with
   | OfNat.ofNat _ _ _ =>

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean

@@ -15,6 +15,10 @@ dynamically convert expressions from other types into `Int` expressions
 and these expressions must be normalized inside of the cutsat module.
 -/
 
+/-
+**Note**: It is safe to use (the more efficient) structural instances tests here because `grind` uses the canonicalizer.
+-/
+open Structural in
 /-- Converts the given integer expression into `Int.Linear.Expr` -/
 partial def toLinearExpr (e : Expr) (generation : Nat := 0) : GoalM Int.Linear.Expr := do
   let toVar (e : Expr) := do

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -253,7 +253,7 @@ where
 
   go (e : Expr) : ProofM MulEqProof := do
     let_expr HMul.hMul _ _ _ i a b := e | goVar e
-    if !(← isInstHMulInt i) then goVar e else
+    if !(← Structural.isInstHMulInt i) then goVar e else
     let ha ← go a
     if let .const 0 h := ha then
       return .const 0 (mkApp3 (mkConst ``Int.Linear.mul_eq_zero_left) a b h)

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean

@@ -15,6 +15,11 @@ namespace Lean.Meta.Grind.Arith.Cutsat
 @[extern "lean_cutsat_propagate_nonlinear"]
 opaque propagateNonlinearTerm (y : Var) (x : Var) : GoalM Bool
 
+/-
+**Note**: It is safe to use (the more efficient) structural instances tests here because `grind` uses the canonicalizer.
+-/
+open Structural
+
 private def isNonlinearTerm (e : Expr) : MetaM Bool := do
   match_expr e with
   | HMul.hMul _ _ _ i _ _ => isInstHMulInt i

src/Lean/Meta/Tactic/Grind/Arith/EvalNum.lean

@@ -25,6 +25,10 @@ def checkExp (k : Nat) : OptionT GrindM Unit := do
     reportIssue! "exponent {k} exceeds threshold for exponentiation `(exp := {(← getConfig).exp})`"
     failure
 
+/-
+**Note**: It is safe to use (the more efficient) structural instances tests here because `grind` uses the canonicalizer.
+-/
+open Structural in
 mutual
 private partial def evalNatCore (e : Expr) : OptionT GrindM Nat := do
   match_expr e with

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

@@ -11,6 +11,7 @@ import Lean.Meta.FunInfo
 import Lean.Util.FVarSubset
 import Lean.Meta.IntInstTesters
 import Lean.Meta.NatInstTesters
+import Lean.Meta.Tactic.Grind.SynthInstance
 public section
 namespace Lean.Meta.Grind
 namespace Canon
@@ -67,9 +68,11 @@ private def isDefEqBounded (a b : Expr) (parent : Expr) : GoalM Bool := do
 
 /--
 Helper function for canonicalizing `e` occurring as the `i`th argument of an `f`-application.
-If `useIsDefEqBounded` is `true`, we try `isDefEqBounded` before returning false
+If `useIsDefEqBounded` is `true`, we try `isDefEqBounded` before returning false.
+
+Remark: `isInst` is `true` if element is an instance.
 -/
-private def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBounded : Bool) : GoalM Expr := do
+private def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBounded : Bool) (isInst := false) : GoalM Expr := do
   let s ← get'
   let key := { f, i, arg := e : CanonArgKey }
   /-
@@ -84,10 +87,36 @@ private def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIs
   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
+      -- We used to check `c.fvarsSubset e` because it is not
+      -- in general safe to replace `e` with `c` if `c` has more free variables than `e`.
+      -- However, we don't revert previously canonicalized elements in the `grind` tactic.
+      -- Moreover, we store the canonicalizer state in the `Goal` because we case-split
+      -- and different locals are added in different branches.
+      modify' fun s => { s with canon := s.canon.insert e c }
+      trace_goal[grind.debug.canon] "found {e} ===> {c}"
+      return true
+    if useIsDefEqBounded then
+      -- If `e` and `c` are not types, we use `isDefEqBounded`
+      if (← isDefEqBounded e c parent) then
+        modify' fun s => { s with canon := s.canon.insert e c }
+        trace_goal[grind.debug.canon] "found using `isDefEqBounded`: {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 eType ← inferType e
     let cs := s.argMap.find? key |>.getD []
     for (c, cType) in cs do
       /-
@@ -100,28 +129,20 @@ where
       where `grind` unfolds the definition of `DHashMap.insert` and `TreeMap.insert`.
       -/
       if (← isDefEqD eType cType) then
-        if (← isDefEq e c) then
-          -- We used to check `c.fvarsSubset e` because it is not
-          -- in general safe to replace `e` with `c` if `c` has more free variables than `e`.
-          -- However, we don't revert previously canonicalized elements in the `grind` tactic.
-          -- Moreover, we store the canonicalizer state in the `Goal` because we case-split
-          -- and different locals are added in different branches.
-          modify' fun s => { s with canon := s.canon.insert e c }
-          trace_goal[grind.debug.canon] "found {e} ===> {c}"
+        if (← checkDefEq e c) then
           return c
-        if useIsDefEqBounded then
-          -- If `e` and `c` are not types, we use `isDefEqBounded`
-          if (← isDefEqBounded e c parent) then
-            modify' fun s => { s with canon := s.canon.insert e c }
-            trace_goal[grind.debug.canon] "found using `isDefEqBounded`: {e} ===> {c}"
-            return c
     trace_goal[grind.debug.canon] "({f}, {i}) ↦ {e}"
     modify' fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key ((e, eType)::cs) }
     return e
 
-private abbrev canonType (parent f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore parent f i e (useIsDefEqBounded := false)
-private abbrev canonInst (parent f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore parent f i e (useIsDefEqBounded := true)
-private abbrev canonImplicit (parent f : Expr) (i : Nat) (e : Expr) := withReducible <| canonElemCore parent f i e (useIsDefEqBounded := true)
+private abbrev canonType (parent f : Expr) (i : Nat) (e : Expr) :=
+  withDefault <| canonElemCore parent f i e (useIsDefEqBounded := false)
+
+private abbrev canonInst (parent f : Expr) (i : Nat) (e : Expr) :=
+  withReducibleAndInstances <| canonElemCore parent f i e (useIsDefEqBounded := true) (isInst := true)
+
+private abbrev canonImplicit (parent f : Expr) (i : Nat) (e : Expr) :=
+  withReducible <| canonElemCore parent f i e (useIsDefEqBounded := true)
 
 /--
 Return type for the `shouldCanon` function.
@@ -212,9 +233,9 @@ private def normOfNatArgs? (args : Array Expr) : MetaM (Option (Array Expr)) :=
       args := args.set 1 (mkRawNatLit val)
       modified := true
     let inst := args[2]
-    if (← isInstOfNatNat inst) && !args[0].isConstOf ``Nat then
+    if (← Structural.isInstOfNatNat inst) && !args[0].isConstOf ``Nat then
       return some (args.set 0 Nat.mkType |>.toArray)
-    else if (← isInstOfNatInt inst) && !args[0].isConstOf ``Int then
+    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

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

@@ -10,7 +10,7 @@ import Lean.Meta.SynthInstance
 public section
 namespace Lean.Meta.Grind
 /--
-Some modules in grind use builtin instances defined directly in core (e.g., `cutsat`),
+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.
@@ -41,8 +41,17 @@ private def builtinInsts : Std.HashMap Expr Expr :=
     (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 := builtinInsts[type]? then
+  if let some inst := getBuiltinInstance? type then
     return inst
   catchInternalId isDefEqStuckExceptionId
     (synthInstanceCore? type none)

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

@@ -55,14 +55,6 @@ because of the symmetric case. By using `eqCongrSymmPlaceholderProof`, we retain
 -/
 def eqCongrSymmPlaceholderProof := mkConst (Name.mkSimple "[eq_congr_symm]")
 
-/-- Similar to `isDefEq`, but ensures default transparency is used. -/
-def isDefEqD (t s : Expr) : MetaM Bool :=
-  withDefault <| isDefEq t s
-
-/-- Similar to `isDefEq`, but ensures that only reducible definitions and instances can be reduced. -/
-def isDefEqI (t s : Expr) : MetaM Bool :=
-  withReducibleAndInstances <| isDefEq t s
-
 /--
 Returns `true` if `e` is `True`, `False`, or a literal value.
 See `Lean.Meta.LitValues` for supported literals.

src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean

@@ -137,28 +137,28 @@ where
       else addAsVar e
     | Int.neg a => return .neg (← toLinearExpr a)
     | Neg.neg _ i a =>
-      if (← isInstNegInt i) then return .neg (← toLinearExpr a)
+      if (← DefEq.isInstNegInt i) then return .neg (← toLinearExpr a)
       else addAsVar e
     | Int.add a b => return .add (← toLinearExpr a) (← toLinearExpr b)
     | Add.add _ i a b =>
-      if (← isInstAddInt i) then return .add (← toLinearExpr a) (← toLinearExpr b)
+      if (← DefEq.isInstAddInt i) then return .add (← toLinearExpr a) (← toLinearExpr b)
       else addAsVar e
     | HAdd.hAdd _ _ _ i a b =>
-      if (← isInstHAddInt i) then return .add (← toLinearExpr a) (← toLinearExpr b)
+      if (← DefEq.isInstHAddInt i) then return .add (← toLinearExpr a) (← toLinearExpr b)
       else addAsVar e
     | Int.sub a b => return .sub (← toLinearExpr a) (← toLinearExpr b)
     | Sub.sub _ i a b =>
-      if (← isInstSubInt i) then return .sub (← toLinearExpr a) (← toLinearExpr b)
+      if (← DefEq.isInstSubInt i) then return .sub (← toLinearExpr a) (← toLinearExpr b)
       else addAsVar e
     | HSub.hSub _ _ _ i a b =>
-      if (← isInstHSubInt i) then return .sub (← toLinearExpr a) (← toLinearExpr b)
+      if (← DefEq.isInstHSubInt i) then return .sub (← toLinearExpr a) (← toLinearExpr b)
       else addAsVar e
     | Int.mul a b => mul a b
     | Mul.mul _ i a b =>
-      if (← isInstMulInt i) then mul a b
+      if (← DefEq.isInstMulInt i) then mul a b
       else addAsVar e
     | HMul.hMul _ _ _ i a b =>
-      if (← isInstHMulInt i) then mul a b
+      if (← DefEq.isInstHMulInt i) then mul a b
       else addAsVar e
     | _ => addAsVar e
 
@@ -183,22 +183,22 @@ partial def leCnstr? (e : Expr) : M (Option (Int.Linear.Expr × Int.Linear.Expr)
   | Int.lt a b =>
     return (.add (← toLinearExpr a) (.num 1), ← toLinearExpr b)
   | LE.le _ i a b =>
-    guard (← isInstLEInt i)
+    guard (← DefEq.isInstLEInt i)
     return (← toLinearExpr a, ← toLinearExpr b)
   | LT.lt _ i a b =>
-    guard (← isInstLTInt i)
+    guard (← DefEq.isInstLTInt i)
     return (.add (← toLinearExpr a) (.num 1), ← toLinearExpr b)
   | GE.ge _ i a b =>
-    guard (← isInstLEInt i)
+    guard (← DefEq.isInstLEInt i)
     return (← toLinearExpr b, ← toLinearExpr a)
   | GT.gt _ i a b =>
-    guard (← isInstLTInt i)
+    guard (← DefEq.isInstLTInt i)
     return (.add (← toLinearExpr b) (.num 1), ← toLinearExpr a)
   | _ => failure
 
 partial def dvdCnstr? (e : Expr) : M (Option (Int × Int.Linear.Expr)) := OptionT.run do
   let_expr Dvd.dvd _ inst k b ← e | failure
-  guard (← isInstDvdInt inst)
+  guard (← DefEq.isInstDvdInt inst)
   let some k ← getIntValue? k | failure
   return (k, ← toLinearExpr b)
 

src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean

@@ -112,22 +112,25 @@ where
         | none => addAsVar e
     match_expr e with
     | OfNat.ofNat _ n i =>
-      if (← isInstOfNatNat i) then toLinearExpr n
+      if (← Structural.isInstOfNatNat i) then
+        toLinearExpr n
+      else if (← isDefEqI i (mkInstOfNatNat n)) then
+        toLinearExpr n
       else addAsVar e
     | Nat.succ a => return inc (← toLinearExpr a)
     | Nat.add a b => return add (← toLinearExpr a) (← toLinearExpr b)
     | Add.add _ i a b =>
-      if (← isInstAddNat i) then return add (← toLinearExpr a) (← toLinearExpr b)
+      if (← DefEq.isInstAddNat i) then return add (← toLinearExpr a) (← toLinearExpr b)
       else addAsVar e
     | HAdd.hAdd _ _ _ i a b =>
-      if (← isInstHAddNat i) then return add (← toLinearExpr a) (← toLinearExpr b)
+      if (← DefEq.isInstHAddNat i) then return add (← toLinearExpr a) (← toLinearExpr b)
       else addAsVar e
     | Nat.mul a b => mul a b
     | Mul.mul _ i a b =>
-      if (← isInstMulNat i) then mul a b
+      if (← DefEq.isInstMulNat i) then mul a b
       else addAsVar e
     | HMul.hMul _ _ _ i a b =>
-      if (← isInstHMulNat i) then mul a b
+      if (← DefEq.isInstHMulNat i) then mul a b
       else addAsVar e
     | _ => addAsVar e
 
@@ -141,16 +144,16 @@ partial def toLinearCnstr? (e : Expr) : M (Option LinearCnstr) := OptionT.run do
   | Nat.lt a b =>
     return { eq := false, lhs := (← toLinearExpr a).inc, rhs := (← toLinearExpr b) }
   | LE.le _ i a b =>
-    guard (← isInstLENat i)
+    guard (← DefEq.isInstLENat i)
     return { eq := false, lhs := (← toLinearExpr a), rhs := (← toLinearExpr b) }
   | LT.lt _ i a b =>
-    guard (← isInstLTNat i)
+    guard (← DefEq.isInstLTNat i)
     return { eq := false, lhs := (← toLinearExpr a).inc, rhs := (← toLinearExpr b) }
   | GE.ge _ i a b =>
-    guard (← isInstLENat i)
+    guard (← DefEq.isInstLENat i)
     return { eq := false, lhs := (← toLinearExpr b), rhs := (← toLinearExpr a) }
   | GT.gt _ i a b =>
-    guard (← isInstLTNat i)
+    guard (← DefEq.isInstLTNat i)
     return { eq := false, lhs := (← toLinearExpr b).inc, rhs := (← toLinearExpr a) }
   | _ => failure
 

tests/lean/run/grind_11745.lean

@@ -0,0 +1,15 @@
+class Preorder (α : Type u) extends LE α
+
+instance instPreorderInt : Preorder Int where
+
+example (c x : Int) (mx : @LE.le Int instPreorderInt.toLE x c) : x ≤ c := by
+  grind -order
+
+example (c x : Int) (mx : @LE.le Int instPreorderInt.toLE (x + (-1) * c) 0) : x ≤ c := by
+  grind -order
+
+example (c x : Int) (mx : @LE.le Int instPreorderInt.toLE x c) : x ≤ c := by
+  lia -order
+
+example (c x : Int) (mx : @LE.le Int instPreorderInt.toLE (x + (-1) * c) 0) : x ≤ c := by
+  lia -order