diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean
index 10e0431629..1e0ab14a30 100644
--- a/src/Init/Data/Array/Count.lean
+++ b/src/Init/Data/Array/Count.lean
@@ -63,7 +63,7 @@ theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + coun
   rcases xs with ⟨xs⟩
   simp [List.length_eq_countP_add_countP (p := p)]
 
-@[grind _=_]
+@[grind =]
 theorem countP_eq_size_filter {xs : Array α} : countP p xs = (filter p xs).size := by
   rcases xs with ⟨xs⟩
   simp [List.countP_eq_length_filter]
diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean
index f17ba363ef..10d3625df8 100644
--- a/src/Init/Data/List/Count.lean
+++ b/src/Init/Data/List/Count.lean
@@ -13,7 +13,7 @@ public section
 /-!
 # Lemmas about `List.countP` and `List.count`.
 
-Because we mark `countP_eq_length_filter` and `count_eq_countP` with `@[grind _=_]`,
+Because we mark `countP_eq_length_filter` with `@[grind =]`,
 we don't need many other `@[grind]` annotations here.
 -/
 
@@ -66,7 +66,7 @@ theorem length_eq_countP_add_countP (p : α → Bool) {l : List α} : length l =
       · rfl
       · simp [h]
 
-@[grind _=_]  -- This to quite aggressive, as it introduces `filter` based reasoning whenever we see `countP`.
+@[grind =]  -- This to quite aggressive, as it introduces `filter` based reasoning whenever we see `countP`.
 theorem countP_eq_length_filter {l : List α} : countP p l = (filter p l).length := by
   induction l with
   | nil => rfl