grind cannot match patterns if head expression is an e-class

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

I'm not entirely sure, if that's what causing grind to fail on the following example. But it looks like grind can only match e-matching patterns when the head expression is exactly the same as in pattern, but not when the head expression is different, yet still in the same equivalence class.

structure Foo where
  f : Nat → Nat

def foo : Foo where
  f := id

example : foo.f 2 = 2 := by simp only [foo, id]

example : foo.f 2 = 2 := by
  -- grind fails
  grind only [foo, id]

In the above grind, the e-matching pattern for @id.eq_1 : ∀ {α : Sort u} (a : α), id a = a is [@id #1 #0]. Even though foo.f and id are in the same equivalence class, grind still didn't use id.eq_1 to prove foo.f 2 = 2 (from foo.f = id and id 2 = 2).

A similar issue, but possibly different, is that grind cannot also prove the following:

structure Foo where
  f : Nat → Nat

def foo : Foo where
  f := id

example : foo.f 2 = id 2 := by simp only [foo]

example : foo.f 2 = id 2 := by
  -- grind fails
  grind only [foo]

Context

I've encountered the issue when working on Mathlib's Sym2:
#lean4 > grind cannot see past CoeFun

Versions

Lean 4.31.0-nightly-2026-04-14

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing both examples with Lean 4.31 nightly and inspect the grind entry point, focusing on e-matching when foo.f and id are equivalent. Done means grind only [foo, id] proves the first example and grind only [foo] proves the second.