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

@@ -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

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