From cdb994b776cd2d252238d79defa44ee33ceb6afe Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Mon, 8 Dec 2025 14:11:25 +1100
Subject: [PATCH] chore: remove `@[grind =]` from
 `List.countP_eq_length_filter` (#11542)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR removes `@[grind =]` from `List.countP_eq_length_filter` and
`Array.countP_eq_size_filter`, as users
[reported](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60countP_eq_length_filter.60.20grind.20attribute/near/561386848)[#lean4
> &#96;countP_eq_length_filter&#96; grind attribute @
💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60countP_eq_length_filter.60.20grind.20attribute/near/561386848)
this was problematic.
---
 src/Init/Data/Array/Count.lean       |  4 ++--
 src/Init/Data/List/Count.lean        |  7 ++++---
 tests/lean/run/grind_11081.lean      |  3 ++-
 tests/lean/run/grind_list_count.lean | 20 +++++++++-----------
 4 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean
index 905fa4d314..4431fd0cb6 100644
--- a/src/Init/Data/Array/Count.lean
+++ b/src/Init/Data/Array/Count.lean
@@ -62,12 +62,12 @@ 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 =]
 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]
 
-@[grind =]
+grind_pattern countP_eq_size_filter => xs.countP p, xs.filter p
+
 theorem countP_eq_size_filter' : countP p = size ∘ filter p := by
   funext xs
   apply countP_eq_size_filter
diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean
index 10d3625df8..9698637043 100644
--- a/src/Init/Data/List/Count.lean
+++ b/src/Init/Data/List/Count.lean
@@ -29,7 +29,7 @@ section countP
 
 variable {p q : α → Bool}
 
-@[simp] theorem countP_nil : countP p [] = 0 := rfl
+@[simp, grind =] theorem countP_nil : countP p [] = 0 := rfl
 
 protected theorem countP_go_eq_add {l} : countP.go p l n = n + countP.go p l 0 := by
   induction l generalizing n with
@@ -47,6 +47,7 @@ protected theorem countP_go_eq_add {l} : countP.go p l n = n + countP.go p l 0 :
 @[simp] theorem countP_cons_of_neg {l} (pa : ¬p a) : countP p (a :: l) = countP p l := by
   simp [countP, countP.go, pa]
 
+@[grind =]
 theorem countP_cons {a : α} {l : List α} : countP p (a :: l) = countP p l + if p a then 1 else 0 := by
   by_cases h : p a <;> simp [h]
 
@@ -66,7 +67,6 @@ 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`.
 theorem countP_eq_length_filter {l : List α} : countP p l = (filter p l).length := by
   induction l with
   | nil => rfl
@@ -75,7 +75,8 @@ theorem countP_eq_length_filter {l : List α} : countP p l = (filter p l).length
     then rw [countP_cons_of_pos h, ih, filter_cons_of_pos h, length]
     else rw [countP_cons_of_neg h, ih, filter_cons_of_neg h]
 
-@[grind =]
+grind_pattern countP_eq_length_filter => l.countP p, l.filter p
+
 theorem countP_eq_length_filter' : countP p = length ∘ filter p := by
   funext l
   apply countP_eq_length_filter
diff --git a/tests/lean/run/grind_11081.lean b/tests/lean/run/grind_11081.lean
index 27d2e5ac9c..97a07dceea 100644
--- a/tests/lean/run/grind_11081.lean
+++ b/tests/lean/run/grind_11081.lean
@@ -75,5 +75,6 @@ theorem countP_diff (hl : Subperm l₂ l₁) (p : α → Bool) :
     List.Perm.subperm_left,
     List.Sublist.subperm,
     List.Subperm.perm_of_length_le,
-    List.Perm.countP_congr
+    List.Perm.countP_congr,
+    List.countP_eq_length_filter
   ]
diff --git a/tests/lean/run/grind_list_count.lean b/tests/lean/run/grind_list_count.lean
index c7cdd99702..907ba6c8db 100644
--- a/tests/lean/run/grind_list_count.lean
+++ b/tests/lean/run/grind_list_count.lean
@@ -29,7 +29,7 @@ theorem countP_eq_length_filter' : countP p = length ∘ filter p := by
   grind
 
 theorem countP_le_length : countP p l ≤ l.length := by
-  grind
+  induction l with grind
 
 theorem countP_append {l₁ l₂ : List α} : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
   grind
@@ -44,11 +44,11 @@ theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
   induction l with grind
 
 theorem countP_eq_length {p} : countP p l = l.length ↔ ∀ a ∈ l, p a := by
-  induction l with grind
+  induction l with grind [countP_eq_length_filter]
 
 theorem countP_replicate {p : α → Bool} {a : α} {n : Nat} :
     countP p (replicate n a) = if p a then n else 0 := by
-  grind
+  induction n with grind
 
 theorem boole_getElem_le_countP {p : α → Bool} {l : List α} {i : Nat} (h : i < l.length) :
     (if p l[i] then 1 else 0) ≤ l.countP p := by
@@ -66,11 +66,9 @@ theorem countP_tail_le (l) : countP p l.tail ≤ countP p l := by grind
 
 -- See `Init.Data.List.Nat.Count` for `le_countP_tail : countP p l - 1 ≤ countP p l.tail`.
 
--- TODO Should we have `@[grind]` for `filter_filter`?
-
 theorem countP_filter {l : List α} :
     countP p (filter q l) = countP (fun a => p a && q a) l := by
-  grind [List.filter_filter]
+  induction l with grind
 
 theorem countP_true : (countP fun (_ : α) => true) = length := by
   funext l
@@ -81,23 +79,23 @@ theorem countP_false : (countP fun (_ : α) => false) = Function.const _ 0 := by
   induction l with grind
 
 theorem countP_map {p : β → Bool} {f : α → β} {l} : countP p (map f l) = countP (p ∘ f) l := by
-  grind
+  induction l with grind
 
 theorem length_filterMap_eq_countP {f : α → Option β} {l : List α} :
     (filterMap f l).length = countP (fun a => (f a).isSome) l := by
-  induction l with grind -- TODO
+  induction l with grind
 
 theorem countP_filterMap {p : β → Bool} {f : α → Option β} {l : List α} :
     countP p (filterMap f l) = countP (fun a => ((f a).map p).getD false) l := by
-  induction l with grind -- TODO
+  induction l with grind
 
 theorem countP_flatten {l : List (List α)} :
     countP p l.flatten = (l.map (countP p)).sum := by
-  grind
+  induction l with grind
 
 theorem countP_flatMap {p : β → Bool} {l : List α} {f : α → List β} :
     countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by
-  grind
+  induction l with grind
 
 theorem countP_reverse {l : List α} : countP p l.reverse = countP p l := by
   grind