feat: refine pattern selection and fix test

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -788,8 +788,9 @@ def mkEMatchTheoremWithKind?
     return (← mkEMatchEqBwdTheoremCore origin levelParams proof)
   let type ← inferType proof
   /-
-  Remark: we should not use `forallTelescopeReducing` here because it may unfold a definition/abstraction,
-  and then select a suboptimal pattern. Here is an example. Suppose we have
+  Remark: we should not use `forallTelescopeReducing` (with default reducibility) here
+  because it may unfold a definition/abstraction, and then select a suboptimal pattern.
+  Here is an example. Suppose we have
   ```
   def State.le (σ₁ σ₂ : State) : Prop := ∀ ⦃x : Var⦄ ⦃v : Val⦄, σ₁.find? x = some v → σ₂.find? x = some v
 
@@ -800,8 +801,10 @@ def mkEMatchTheoremWithKind?
   @[grind] theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ := by
   ```
   We do not want `State.le` to be unfolded and the abstraction exposed.
+
+  That said, we must still reduce `[reducible]` definitions since `grind` unfolds them.
   -/
-  forallTelescope type fun xs type => do
+  withReducible <| forallTelescopeReducing type fun xs type => withDefault do
     let searchPlaces ← match kind with
       | .fwd =>
         let ps ← getPropTypes xs

tests/lean/run/grind_eq_pattern.lean

@@ -1,4 +1,17 @@
+%reset_grind_attrs
+
+/--
+info: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend ? ? ? ? #2 #0]
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.pattern true in
 attribute [grind] List.append_ne_nil_of_left_ne_nil
+
+/--
+info: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend ? ? ? ? #1 #2]
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.pattern true in
 attribute [grind] List.append_ne_nil_of_right_ne_nil
 /--
 info: [grind.ematch.pattern] List.getLast?_eq_some_iff: [@List.getLast? #2 #1, @some ? #0]
@@ -13,7 +26,6 @@ info: [grind.assert] xs.getLast? = b?
 [grind.assert] xs = []
 [grind.assert] (xs.getLast? = some 10) = ∃ ys, xs = ys ++ [10]
 [grind.assert] xs = w ++ [10]
-[grind.assert] ¬w = [] → ¬w ++ [10] = []
 [grind.assert] ¬w ++ [10] = []
 -/
 #guard_msgs (info) in