chore: use boolean predicates in List.filter (#5287)

src/Init/Data/Array/Lemmas.lean

@@ -687,7 +687,7 @@ theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
   | cons => split <;> simp [*]
 
 @[simp] theorem filter_filter (q) (l : Array α) :
-    filter p (filter q l) = filter (fun a => p a ∧ q a) l := by
+    filter p (filter q l) = filter (fun a => p a && q a) l := by
   apply ext'
   simp only [filter_data, List.filter_filter]
 

src/Init/Data/List/Count.lean

@@ -116,7 +116,7 @@ theorem IsSuffix.countP_le (s : l₁ <:+ l₂) : countP p l₁ ≤ countP p l₂
 theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le _
 
 theorem countP_filter (l : List α) :
-    countP p (filter q l) = countP (fun a => p a ∧ q a) l := by
+    countP p (filter q l) = countP (fun a => p a && q a) l := by
   simp only [countP_eq_length_filter, filter_filter]
 
 @[simp] theorem countP_true {l : List α} : (l.countP fun _ => true) = l.length := by

src/Init/Data/List/Lemmas.lean

@@ -1254,7 +1254,7 @@ theorem forall_mem_filter {l : List α} {p : α → Bool} {P : α → Prop} :
 
 @[deprecated forall_mem_filter (since := "2024-07-25")] abbrev forall_mem_filter_iff := @forall_mem_filter
 
-@[simp] theorem filter_filter (q) : ∀ l, filter p (filter q l) = filter (fun a => p a ∧ q a) l
+@[simp] theorem filter_filter (q) : ∀ l, filter p (filter q l) = filter (fun a => p a && q a) l
   | [] => rfl
   | a :: l => by by_cases hp : p a <;> by_cases hq : q a <;> simp [hp, hq, filter_filter _ l]