test:

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

@@ -505,6 +505,10 @@ structure State where
 abbrev M := StateRefT State MetaM
 
 private def saveSymbol (h : HeadIndex) : M Unit := do
+  if let .const declName := h then
+    if declName == ``Grind.genHEqPattern || declName == ``Grind.genPattern then
+      -- We do not save gadgets in the list of symbols.
+      return ()
   unless (← get).symbolSet.contains h do
     modify fun s => { s with symbols := s.symbols.push h, symbolSet := s.symbolSet.insert h }
 
@@ -1109,7 +1113,7 @@ def mkEMatchEqTheoremsForDef? (declName : Name) (showInfo := false) : MetaM (Opt
 
 private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (useLhs := true) (showInfo := false) : MetaM Unit := do
   if wasOriginallyTheorem (← getEnv) declName then
-    ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs) (showInfo := showInfo)) attrKind
+    ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs) (gen := thmKind.gen) (showInfo := showInfo)) attrKind
   else if let some thms ← mkEMatchEqTheoremsForDef? declName (showInfo := showInfo) then
     unless useLhs do
       throwError "`{declName}` is a definition, you must only use the left-hand side for extracting patterns"

tests/lean/run/grind_ematch_gen_pattern.lean

@@ -1,6 +1,7 @@
 set_option grind.warning false
+reset_grind_attrs%
 
-@[grind] theorem pbind_some' {α β} {x : Option α} {a : α} {f : (a : α) → x = some a → Option β}
+@[grind gen] theorem pbind_some' {α β} {x : Option α} {a : α} {f : (a : α) → x = some a → Option β}
      (h : x = some a) : Option.pbind x f = f a h := by
   subst h; rfl
 
@@ -10,4 +11,96 @@ def f (x : Option Nat) (h : x ≠ none) : Nat :=
   | some a => a
 
 example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
+  grind only [gen pbind_some', f]
+
+-- Note that the following instance does not have hypotheses.
+/-- trace: [grind.ematch.instance] pbind_some': (b.pbind fun a h => some (2 * a)) = some (2 * a) -/
+#guard_msgs (trace) in
+example (a : Nat) (h : b = some a) : (b.pbind fun a h => some <| 2*a) = some (a + a) := by
+  set_option trace.grind.ematch.instance true in
+  grind only [gen pbind_some']
+
+/--
+trace: [grind.ematch.instance] pbind_some': (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯)
+[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a
+-/
+#guard_msgs (trace) in
+example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
+  set_option trace.grind.ematch.instance true in
+  grind [f]
+
+-- Many different instances are generated if the `gen` modifier is not used
+/--
+trace: [grind.ematch.instance] pbind_some': ∀ (h : b = some a), (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h : b = some (2 * a)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (2 * a + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯ + f b ⋯)
+[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a
+[grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 2 * f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (a + 2 * f b ⋯ + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 3 * f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (a + 3 * f b ⋯ + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 4 * f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (a + 4 * f b ⋯ + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (2 * a + f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (2 * a + f b ⋯ + f b ⋯)
+-/
+#guard_msgs (trace) in
+example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
+  set_option trace.grind.ematch.instance true in
   grind only [pbind_some', f]
+
+
+-- `Option.pbing_some` produces an instance with a `cast` that makes the result hard to use
+/--
+trace: [grind.ematch.instance] Option.pbind_some: (some a).pbind (cast ⋯ fun a h => some (a + f b ⋯)) =
+      cast ⋯ (fun a h => some (a + f b ⋯)) a ⋯
+[grind.ematch.instance] Option.pbind_some: (some (2 * a)).pbind (cast ⋯ fun a h => some (a + f b ⋯)) =
+      cast ⋯ (fun a h => some (a + f b ⋯)) (2 * a) ⋯
+-/
+#guard_msgs (trace) in
+example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
+  set_option trace.grind.ematch.instance true in
+  fail_if_success grind only [Option.pbind_some, f]
+  sorry
+
+/-- trace: [grind.ematch.instance] pbind_some': (b.pbind fun a h => some (2 * a)) = some (2 * a) -/
+#guard_msgs (trace) in
+example (a : Nat) (h : b = some a) : (b.pbind fun a h => some <| 2*a) = some (a + a) := by
+  set_option trace.grind.ematch.instance true in
+  grind only [= gen pbind_some']
+
+example (a : Nat) (h : b = some a) : (b.pbind fun a h => some <| 2*a) = some (a + a) := by
+  fail_if_success grind only [= pbind_some']
+  sorry
+
+reset_grind_attrs%
+
+@[grind = gen] theorem pbind_some'' {α β} {x : Option α} {a : α} {f : (a : α) → x = some a → Option β}
+     (h : x = some a) : Option.pbind x f = f a h := by
+  subst h; rfl
+
+/--
+trace: [grind.ematch.instance] pbind_some'': (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯)
+[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a
+-/
+#guard_msgs (trace) in
+example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
+  set_option trace.grind.ematch.instance true in
+  grind [f]
+
+reset_grind_attrs%
+
+@[grind =_ gen] theorem pbind_some''' {α β} {x : Option α} {a : α} {f : (a : α) → x = some a → Option β}
+     (h : x = some a) : f a h = Option.pbind x f := by
+  subst h; rfl
+
+/--
+trace: [grind.ematch.instance] pbind_some''': some (a + f b ⋯) = b.pbind fun a h => some (a + f b ⋯)
+[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a
+-/
+#guard_msgs (trace) in
+example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
+  set_option trace.grind.ematch.instance true in
+  grind [f]