chore: fix grind annotation on DHashMap.contains_iff_mem (#8700)

The original annotations produced patterns that matched too often.

src/Std/Data/DHashMap/Lemmas.lean

@@ -51,10 +51,14 @@ theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
 
 -- While setting up the API, often use this in the reverse direction,
 -- but prefer this direction for users.
-@[simp, grind _=_]
+@[simp, grind =]
 theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
   Iff.rfl
 
+-- We need to specify the pattern for the reverse direction manually,
+-- as the default heuristic leaves the `DHashMap α β` argument as a wildcard.
+grind_pattern contains_iff_mem => @Membership.mem α (DHashMap α β) _ m a
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
     m.contains a = m.contains b :=
   Raw₀.contains_congr _ m.2 hab

src/Std/Data/ExtDHashMap/Lemmas.lean

@@ -51,10 +51,15 @@ theorem not_insert_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
 theorem mem_iff_contains [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a :=
   Iff.rfl
 
-@[simp, grind _=_]
+@[simp, grind =]
 theorem contains_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a ↔ a ∈ m :=
   Iff.rfl
 
+-- We need to specify the pattern for the reverse direction manually,
+-- as the default heuristic leaves the `ExtDHashMap α β` argument as a wildcard.
+grind_pattern contains_iff_mem => @Membership.mem α (ExtDHashMap α β) _ m a
+
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m.contains a = m.contains b :=
   m.inductionOn fun _ => DHashMap.contains_congr hab