chore(Multiset,Finset): add filter_true/filter_false (#28838)

- Add `Multiset.filter_true` and `Multiset.filter_false`.
- Rename `Finset.filter_True` to `Finset.filter_true`.
- Rename `Finset.filter_False` to `Finset.filter_false`.
- Add `@[simp]` to `filter_true`/`filter_false`/`filter_eq_self`/`filter_eq_nil`.

Author: yury-harmonic

Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean

@@ -52,7 +52,7 @@ theorem decomposition_Q (n q : ℕ) :
       ∑ i : Fin (n + 1) with i.val < q, (P i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ (Fin.rev i) := by
   induction' q with q hq
   · simp only [Q_zero, HomologicalComplex.zero_f_apply, Nat.not_lt_zero,
-      Finset.filter_False, Finset.sum_empty]
+      Finset.filter_false, Finset.sum_empty]
   · by_cases hqn : q + 1 ≤ n + 1
     swap
     · rw [Q_is_eventually_constant (show n + 1 ≤ q by omega), hq]

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -297,7 +297,7 @@ theorem complete_graph_degree [DecidableEq V] (v : V) :
 
 @[simp]
 theorem bot_degree (v : V) : (⊥ : SimpleGraph V).degree v = 0 := by
-  simp_rw [degree, neighborFinset_eq_filter, bot_adj, filter_False]
+  simp_rw [degree, neighborFinset_eq_filter, bot_adj, filter_false]
   exact Finset.card_empty
 
 theorem IsRegularOfDegree.top [DecidableEq V] :

Mathlib/Data/DFinsupp/NeLocus.lean

@@ -52,7 +52,7 @@ theorem coe_neLocus : ↑(f.neLocus g) = { x | f x ≠ g x } :=
 theorem neLocus_eq_empty {f g : Π₀ a, N a} : f.neLocus g = ∅ ↔ f = g :=
   ⟨fun h ↦
     ext fun a ↦ not_not.mp (mem_neLocus.not.mp (Finset.eq_empty_iff_forall_notMem.mp h a)),
-    fun h ↦ h ▸ by simp only [neLocus, Ne, not_true, Finset.filter_False]⟩
+    fun h ↦ h ▸ by simp only [neLocus, Ne, not_true, Finset.filter_false]⟩
 
 @[simp]
 theorem nonempty_neLocus_iff {f g : Π₀ a, N a} : (f.neLocus g).Nonempty ↔ f ≠ g :=

Mathlib/Data/Finset/Filter.lean

@@ -141,15 +141,21 @@ theorem filter_congr_decidable (s : Finset α) (p : α → Prop) (h : DecidableP
     [DecidablePred p] : @filter α p h s = s.filter p := by congr
 
 @[simp]
-theorem filter_True {h} (s : Finset α) : @filter _ (fun _ => True) h s = s := by ext; simp
+theorem filter_true {h} (s : Finset α) : @filter _ (fun _ => True) h s = s := by ext; simp
+
+@[deprecated (since := "2025-08-24")] alias filter_True := filter_true
 
 @[simp]
-theorem filter_False {h} (s : Finset α) : @filter _ (fun _ => False) h s = ∅ := by ext; simp
+theorem filter_false {h} (s : Finset α) : @filter _ (fun _ => False) h s = ∅ := by ext; simp
+
+@[deprecated (since := "2025-08-24")] alias filter_False := filter_false
 
 variable {p q}
 
+@[simp]
 lemma filter_eq_self : s.filter p = s ↔ ∀ x ∈ s, p x := by simp [Finset.ext_iff]
 
+@[simp]
 theorem filter_eq_empty_iff : s.filter p = ∅ ↔ ∀ ⦃x⦄, x ∈ s → ¬p x := by simp [Finset.ext_iff]
 
 theorem filter_nonempty_iff : (s.filter p).Nonempty ↔ ∃ a ∈ s, p a := by

Mathlib/Data/Finsupp/NeLocus.lean

@@ -54,7 +54,7 @@ theorem coe_neLocus : ↑(f.neLocus g) = { x | f x ≠ g x } := by
 theorem neLocus_eq_empty {f g : α →₀ N} : f.neLocus g = ∅ ↔ f = g :=
   ⟨fun h =>
     ext fun a => not_not.mp (mem_neLocus.not.mp (Finset.eq_empty_iff_forall_notMem.mp h a)),
-    fun h => h ▸ by simp only [neLocus, Ne, not_true, Finset.filter_False]⟩
+    fun h => h ▸ by simp only [neLocus, Ne, not_true, Finset.filter_false]⟩
 
 @[simp]
 theorem nonempty_neLocus_iff {f g : α →₀ N} : (f.neLocus g).Nonempty ↔ f ≠ g :=

Mathlib/Data/Multiset/Filter.lean

@@ -96,15 +96,23 @@ theorem mem_of_mem_filter {a : α} {s} (h : a ∈ filter p s) : a ∈ s :=
 theorem mem_filter_of_mem {a : α} {l} (m : a ∈ l) (h : p a) : a ∈ filter p l :=
   mem_filter.2 ⟨m, h⟩
 
+@[simp]
 theorem filter_eq_self {s} : filter p s = s ↔ ∀ a ∈ s, p a :=
   Quot.inductionOn s fun _l =>
     Iff.trans ⟨fun h => filter_sublist.eq_of_length (congr_arg card h),
       congr_arg ofList⟩ <| by simp
 
+@[simp]
 theorem filter_eq_nil {s} : filter p s = 0 ↔ ∀ a ∈ s, ¬p a :=
   Quot.inductionOn s fun _l =>
     Iff.trans ⟨fun h => eq_nil_of_length_eq_zero (congr_arg card h), congr_arg ofList⟩ (by simp)
 
+@[simp]
+lemma filter_true (s : Multiset α) : s.filter (fun _ ↦ True) = s := by simp
+
+@[simp]
+lemma filter_false (s : Multiset α) : s.filter (fun _ ↦ False) = 0 := by simp
+
 theorem le_filter {s t} : s ≤ filter p t ↔ s ≤ t ∧ ∀ a ∈ s, p a :=
   ⟨fun h => ⟨le_trans h (filter_le _ _), fun _a m => of_mem_filter (mem_of_le h m)⟩, fun ⟨h, al⟩ =>
     filter_eq_self.2 al ▸ filter_le_filter p h⟩

Mathlib/Data/Nat/Count.lean

@@ -133,8 +133,7 @@ alias ⟨_, count_of_forall⟩ := count_iff_forall
 @[simp] theorem count_true (n : ℕ) : count (fun _ ↦ True) n = n := count_of_forall fun _ _ ↦ trivial
 
 theorem count_iff_forall_not {n : ℕ} : count p n = 0 ↔ ∀ m < n, ¬p m := by
-  simpa [count_eq_card_filter_range, mem_range] using
-    card_filter_eq_zero_iff (p := p) (s := range n)
+  simp [count_eq_card_filter_range]
 
 alias ⟨_, count_of_forall_not⟩ := count_iff_forall_not
 

Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

@@ -452,7 +452,7 @@ theorem linearIndependent_sum {v : ι ⊕ ι' → M} :
     -- Porting note: `g` must be specified.
     rw [Finset.sum_preimage' (g := fun x => g x • v x),
       Finset.sum_preimage' (g := fun x => g x • v x), ← Finset.sum_union, ← Finset.filter_or]
-    · simpa only [← mem_union, range_inl_union_range_inr, mem_univ, Finset.filter_True]
+    · simpa only [← mem_union, range_inl_union_range_inr, mem_univ, Finset.filter_true]
     · exact Finset.disjoint_filter.2 fun x _ hx =>
         disjoint_left.1 isCompl_range_inl_range_inr.disjoint hx
   rw [← eq_neg_iff_add_eq_zero] at this

Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean

@@ -95,7 +95,7 @@ theorem detp_mul :
 
 theorem mul_adjp_apply_eq : (A * adjp s A) i i = detp s A := by
   have key := sum_fiberwise_eq_sum_filter (ofSign s) univ (· i) fun σ ↦ ∏ k, A k (σ k)
-  simp_rw [mem_univ, filter_True] at key
+  simp_rw [mem_univ, filter_true] at key
   simp_rw [mul_apply, adjp_apply, mul_sum, detp, ← key]
   refine sum_congr rfl fun x hx ↦ sum_congr rfl fun σ hσ ↦ ?_
   rw [← prod_mul_prod_compl ({i} : Finset n), prod_singleton, (mem_filter.mp hσ).2]

Mathlib/Order/Partition/Finpartition.lean

@@ -732,7 +732,7 @@ theorem mem_atomise :
 
 theorem atomise_empty (hs : s.Nonempty) : (atomise s ∅).parts = {s} := by
   simp only [atomise, powerset_empty, image_singleton, notMem_empty, IsEmpty.forall_iff,
-    imp_true_iff, filter_True]
+    imp_true_iff, filter_true]
   exact erase_eq_of_notMem (notMem_singleton.2 hs.ne_empty.symm)
 
 theorem card_atomise_le : #(atomise s F).parts ≤ 2 ^ #F :=