fix: mbtc for nonlinear terms in grind cutsat (#10965)

This PR ensures that model-based theory combination in `grind cutsat`
considers nonlinear terms. Nonlinear multiplications such as `x * y` are
treated as uninterpreted symbols in `cutsat`.

Closes #10885

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

@@ -46,8 +46,35 @@ private def getAssignmentExt? (e : Expr) : GoalM (Option Rat) := do
 private def hasTheoryVar (e : Expr) : GoalM Bool := do
   cutsatExt.hasTermAtRoot e
 
+/-
+**Note**: cutsat is a procedure for linear integer arithmetic. Thus, morally a
+nonlinear multiplication, division, and modulo are **not** interpreted by cutsat.
+Thus, we enable model-theory combination for them. This is necessary for examples
+such as:
+```
+example {a b : Nat} (ha : 1 ≤ a) : (a - 1 + 1) * b = a * b := by grind
+```
+Note that we currently use a restrictive/cheaper version of mbtc. We only case-split
+on `a = b`, if they have the same assignment **and** occur as the `i`-th argument of
+the same function symbol. The latter reduces the number of case-splits we have to
+perform, but misses the following variant of the problem above.
+```
+example {a b : Nat} (ha : 1 ≤ a) : (a - 1 + 1) * b = b * a := by grind
+```
+If this becomes an issue in practice, we can add a flag for enabling the more
+expensive version of `mbtc`.
+-/
+
+private def isNonlinearTerm (e : Expr) : GoalM Bool :=
+  match_expr e with
+  | HMul.hMul _ _ _ _ a b => return (← getIntValue? a <|> getIntValue? b).isNone
+  | HDiv.hDiv _ _ _ _ _ b => return (← getIntValue? b).isNone
+  | HMod.hMod _ _ _ _ _ b => return (← getIntValue? b).isNone
+  | _ => return false
+
 private def isInterpreted (e : Expr) : GoalM Bool := do
-  if isInterpretedTerm e then return true
+  if isInterpretedTerm e then
+    return !(← isNonlinearTerm e)
   let f := e.getAppFn
   /-
   **Note**: `grind` normalizes terms, but some of them cannot be rewritten by `simp` because

tests/lean/run/grind_10885.lean

@@ -0,0 +1,11 @@
+example {a b : Nat} (ha : 1 ≤ a) : (a - 1 + 1) * b = a * b := by grind
+
+/--
+info: Try this:
+  [apply] ⏎
+    mbtc
+    cases #9501
+-/
+#guard_msgs in
+example {a b : Nat} (ha : 1 ≤ a) : (a - 1 + 1) * b = a * b := by
+  grind => finish? -- mbtc was applied consider nonlinear `*`