From ccc7157c08310f38ca67c49d5f8bbf8201ef6d68 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 29 Mar 2026 12:37:54 +0200
Subject: [PATCH] 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    | 4 ++--
 tests/elab/grind_13167.lean | 6 ++++++
 2 files changed, 8 insertions(+), 2 deletions(-)
 create mode 100644 tests/elab/grind_13167.lean

diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean
index 05a222b28e..f73dece770 100644
--- a/src/Init/Grind/Util.lean
+++ b/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
diff --git a/tests/elab/grind_13167.lean b/tests/elab/grind_13167.lean
new file mode 100644
index 0000000000..991b11efad
--- /dev/null
+++ 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]