From 14b595e9529dcccc9d532f3a83d548f8441bc3a5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 10 Feb 2026 11:46:00 -0800
Subject: [PATCH] feat: better support for eta expanded terms in `grind`
 (#12415)

This PR improves the support for eta expanded terms in `grind` patterns.

Closes #12390
---
 src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean |  6 ++++-
 tests/lean/run/grind_12390.lean               | 24 +++++++++++++++++++
 2 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/grind_12390.lean

diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index b842c880ba..c6b94b5ee7 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -9,6 +9,7 @@ public import Lean.Meta.Tactic.Grind.Extension
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.TryThis
 import Lean.Meta.Sym.Util
+import Lean.Meta.Sym.Eta
 public section
 namespace Lean.Meta.Grind
 /-!
@@ -280,7 +281,10 @@ private theorem normConfig_zetaDelta : normConfig.zetaDelta = true := rfl
 def preprocessPattern (pat : Expr) (normalizePattern := true) : MetaM Expr := do
   let pat ← instantiateMVars pat
   let pat ← Sym.unfoldReducible pat
-  let pat ← if normalizePattern then normalize pat normConfig else pure pat
+  let pat ← if normalizePattern then
+    Sym.etaReduceAll (← normalize pat normConfig)
+  else
+    pure pat
   let pat ← detectOffsets pat
   let pat ← foldProjs pat
   return pat
diff --git a/tests/lean/run/grind_12390.lean b/tests/lean/run/grind_12390.lean
new file mode 100644
index 0000000000..abcb6edd58
--- /dev/null
+++ b/tests/lean/run/grind_12390.lean
@@ -0,0 +1,24 @@
+variable {α β : Type}
+
+axiom foo (f : α → β) : β
+
+axiom fooProp : β → Prop
+
+axiom fooProp_foo {f : α → β} : fooProp (foo (fun x ↦ f x))
+axiom fooProp_foo' {f : α → β} : fooProp (foo f)
+
+attribute [grind ←] fooProp_foo -- should work
+
+example {f : α → β} : fooProp (foo f) := by grind -- succeeds, using `fooProp_foo`
+
+/--
+info: Try these:
+  [apply] grind only [← fooProp_foo]
+  [apply] grind => instantiate only [← fooProp_foo]
+-/
+#guard_msgs in
+example {f : α → β} : fooProp (foo f) := by grind? -- succeeds, using `fooProp_foo`
+
+attribute [grind ←] fooProp_foo' -- succeeds
+
+example {f : α → β} : fooProp (foo f) := by grind