fix: expose grind gadgets abstractFn and simpMatchDiscrsOnly (#13177)

This PR adds `@[expose]` to `Lean.Grind.abstractFn` and
`Lean.Grind.simpMatchDiscrsOnly` so that the kernel can unfold them when
type-checking `grind`-produced proofs inside `module` blocks. Other
similar gadgets (`nestedDecidable`, `PreMatchCond`, `alreadyNorm`) were
already exposed; these two were simply missed.

Closes https://github.com/leanprover/lean4/issues/13167

src/Init/Grind/Util.lean

@@ -30,13 +30,13 @@ simpMatchDiscrsOnly (match 0 with | 0 => true | _ => false) = true
 ```
 using `eq_self`.
 -/
-def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
+@[expose] def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
 
 /--
 Gadget for protecting lambda abstractions created by `abstractGroundMismatches?`
 from beta reduction during preprocessing. See `ProveEq.lean` for details.
 -/
-def abstractFn {α : Sort u} (a : α) : α := a
+@[expose] def abstractFn {α : Sort u} (a : α) : α := a
 
 /-- Gadget for representing offsets `t+k` in patterns. -/
 def offset (a b : Nat) : Nat := a + b

tests/elab/grind_13167.lean

@@ -0,0 +1,6 @@
+module
+
+-- https://github.com/leanprover/lean4/issues/13167
+theorem Option.bind_pmap {α β γ} {p : α → Prop} (f : ∀ a, p a → β) (x : Option α) (g : β → Option γ) (H) :
+    pmap f x H >>= g = x.pbind fun a h ↦ g (f a (H _ h)) := by
+  grind [cases Option, pmap]