fix: mark `Grind.nestedDecidable` as an abbreviation This PR fixes a performance issue where proof terms produced by `grind` could trigger kernel deterministic timeouts. `grind` canonicalizes nested `Decidable` instances under the identity wrapper `Grind.nestedDecidable`, leaving the kernel to check `t =?= Grind.nestedDecidable t`. The kernel does not see the `[reducible]` attribute, and its lazy-delta heuristic unfolded `t` instead of the wrapper. When `t` is an instance such as `UInt32.decLe` applied to a symbolic argument and a large literal (e.g., `97 ≤ c.val + 4294967264` coming from `Char`/`UInt32` wraparound), the check descended through `BitVec` and `Fin` into `Nat.ble` on a `2^32`-sized literal with a free variable inside, where the fast numeral path does not apply, and effectively never terminated. Marking `nestedDecidable` as an abbreviation stores the `abbrev` reducibility hint in the declaration itself, which the kernel does honor, so the wrapper side is unfolded first and the check succeeds immediately. The `unfoldReducible` preprocessor now treats `Grind.nestedDecidable` as a `grind` gadget that must not be unfolded: like `Grind.EqMatch` and `Grind.MatchCond`, it is an `abbrev` that must survive until the corresponding propagators consume it. Reported by Paul Reichert.

diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean
index 1e31369..0189c6b 100644
--- a/src/Init/Grind/Util.lean
+++ b/src/Init/Grind/Util.lean

@@ -18,7 +18,9 @@
 /-- A helper gadget for annotating nested decidable instances in goals. -/
 -- Remark: we currently have special gadgets for the two most common subsingletons in Lean, and are the only
 -- currently supported in `grind`. We may add a generic `nestedSubsingleton` inn the future.
-@[expose] def nestedDecidable {p : Prop} (h : Decidable p) : Decidable p := h
+-- **Note**: We mark it as an abbreviation to ensure the kernel will not get confused when checking
+-- that `t =?= Grind.nestedDecidable t`
+abbrev nestedDecidable {p : Prop} (h : Decidable p) : Decidable p := h
 
 /--
 Gadget for marking `match`-expressions that should not be reduced by the `grind` simplifier, but the discriminants should be normalized.
@@ -69,7 +71,9 @@
   subst h; apply HEq.refl
 
 theorem nestedDecidable_congr (p q : Prop) (h : p = q) (hp : Decidable p) (hq : Decidable q) : @nestedDecidable p hp ≍ @nestedDecidable q hq := by
-  subst h; cases hp <;> cases hq <;> simp <;> contradiction
+  subst h; cases hp <;> cases hq <;> unfold nestedDecidable <;> try simp
+  next h1 h2 => exact False.elim (h1 h2)
+  next h1 h2 => exact False.elim (h2 h1)
 
 @[app_unexpander nestedProof]
 meta def nestedProofUnexpander : PrettyPrinter.Unexpander := fun stx => do

diff --git a/src/Lean/Meta/Sym/AlphaShareCommon.lean b/src/Lean/Meta/Sym/AlphaShareCommon.lean
index f3a6039..051b5ae 100644
--- a/src/Lean/Meta/Sym/AlphaShareCommon.lean
+++ b/src/Lean/Meta/Sym/AlphaShareCommon.lean

@@ -55,12 +55,12 @@
 
 /--
 Returns `true` if `declName` is the name of a grind helper declaration that
-should not be unfolded by `unfoldReducible`. `Grind.EqMatch` and `Grind.MatchCond`
+should not be unfolded by `unfoldReducible`. `Grind.EqMatch`, `Grind.MatchCond`, `Grind.nestedReducible`
 are `abbrev`s, but they are gadgets that must survive until the corresponding
 propagators consume them.
 -/
 def isGrindGadget (declName : Name) : Bool :=
-  declName == ``Grind.EqMatch || declName == ``Grind.MatchCond
+  declName == ``Grind.EqMatch || declName == ``Grind.MatchCond || declName == ``Grind.nestedDecidable
 
 /--
 Returns `true` if `declName` is a reducible constant that the `unfoldReducible`

diff --git a/tests/elab/grind_nestedDecidable_kernel_issue.lean b/tests/elab/grind_nestedDecidable_kernel_issue.lean
new file mode 100644
index 0000000..e67a361
--- /dev/null
+++ b/tests/elab/grind_nestedDecidable_kernel_issue.lean

@@ -0,0 +1,40 @@
+module
+set_option warn.sorry false
+/-!
+Paul Reichert's examples: `grind` + kernel interaction through `Grind.nestedDecidable`.
+
+`grind` canonicalizes `Decidable` instances under the identity wrapper
+`Grind.nestedDecidable`, assuming `X =?= nestedDecidable X` is free. The elaborator
+unfolds the reducible wrapper instantly, but the kernel does not take `[reducible]` hint.
+We fix the issue by tagging `Grind.nestedDecidable` as an abbreviation which tags in the
+kernel as an abbreviation.
+-/
+
+set_option maxHeartbeats 1000 -- for the health of your machines
+
+/-!
+
+Grind's literal normalization produces `97 ≤ c.val + 4294967264` and cutsat closes the goal,
+but `decide_eq_true_eq`'s metavariable type check
+```lean
+Decidable (97 ≤ c.val + 4294967264) =?= Decidable ('a'.val ≤ {val := c.val + ('A'.val - 'a'.val), ...}.val)
+```
+fails at implicit transparency because we made `UInt32.toBitVec` semireducible.
+Grind then keeps the `decide` layer, canonicalizes instances under `Grind.nestedDecidable`,
+and leaves it to the kernel to verify that `X =?= nestedDecidable X` is true with
+`X = 'a'.val.decLe (c.val + ('A'.val - 'a'.val))`.
+This leads to the exact problem shown previously.
+-/
+
+section
+set_option allowUnsafeReducibility true
+attribute [local semireducible] UInt32.toBitVec -- or `Char.ofNat`
+
+set_option maxHeartbeats 5000 in
+example (c : Char) : c.toUpper.isLower = false := by
+  simp only [Char.isLower, Char.toUpper]
+  split
+  · grind only  -- (kernel) deterministic timeout
+  · sorry
+
+end