chore: minor fixes to grind_indexmap test case

tests/lean/run/grind_indexmap.lean

@@ -56,7 +56,7 @@ variable [LawfulBEq α] [LawfulHashable α]
 attribute [local grind _=_] IndexMap.WF
 
 private theorem getElem_indices_lt {h : a ∈ m} : m.indices[a] < m.size := by
-  have : m.indices[a]? = some m.indices[a] := by grind [getElem?_pos]
+  have : m.indices[a]? = some m.indices[a] := by grind
   grind
 
 grind_pattern getElem_indices_lt => m.indices[a]
@@ -77,7 +77,7 @@ instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
 @[local grind] private theorem WF' (i : Nat) (a : α) (h₁ : i < m.keys.size) (h₂ : a ∈ m) :
     m.keys[i] = a ↔ m.indices[a] = i := by
   have := m.WF i a
-  grind [getElem?_pos]
+  grind
 
 @[local grind] private theorem getElem_keys_getElem_indices
     {m : IndexMap α β} {a : α} {h : a ∈ m} :
@@ -93,8 +93,8 @@ instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
   m.values[i]
 
 instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
-  getElem?_def := by grind [getElem?_pos]
-  getElem!_def := by grind [getElem!_pos]
+  getElem?_def := by grind
+  getElem!_def := by grind
 
 @[inline] def insert [LawfulBEq α] (m : IndexMap α β) (a : α) (b : β) :
     IndexMap α β :=