chore: revert Multiset and Finset API to use Prop instead of Bool (#1652)

Co-authored-by: Reid Barton <rwbarton@gmail.com>

Author: jcommelin

Mathlib/Algebra/BigOperators/Basic.lean

@@ -373,14 +373,11 @@ theorem prod_union [DecidableEq α] (h : Disjoint s₁ s₂) :
 #align finset.sum_union Finset.sum_union
 
 @[to_additive]
-theorem prod_filter_mul_prod_filter_not (s : Finset α) (p : α → Prop) [DecidablePred p]
-    [DecidablePred fun x => ¬p x] (f : α → β) :
+theorem prod_filter_mul_prod_filter_not
+    (s : Finset α) (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] (f : α → β) :
     ((∏ x in s.filter p, f x) * ∏ x in s.filter fun x => ¬p x, f x) = ∏ x in s, f x := by
-  classical
-  rw [← prod_union]
-  · conv in ∏ x in s, f x => rw [← filter_union_filter_neg_eq (p ·) s]
-    simp
-  · simpa using disjoint_filter_filter_neg s s (p ·)
+  have := Classical.decEq α
+  rw [← prod_union (disjoint_filter_filter_neg s s p), filter_union_filter_neg_eq]
 #align finset.prod_filter_mul_prod_filter_not Finset.prod_filter_mul_prod_filter_not
 #align finset.sum_filter_add_sum_filter_not Finset.sum_filter_add_sum_filter_not
 
@@ -1112,13 +1109,13 @@ theorem prod_bij_ne_one {s : Finset α} {t : Finset γ} {f : α → β} {g : γ
     (i_inj : ∀ a₁ a₂ h₁₁ h₁₂ h₂₁ h₂₂, i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
     (i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a h₁ h₂, b = i a h₁ h₂) (h : ∀ a h₁ h₂, f a = g (i a h₁ h₂)) :
     (∏ x in s, f x) = ∏ x in t, g x := by
-  classical refine'
-      calc
-        (∏ x in s, f x) = ∏ x in s.filter fun x => f x ≠ 1, f x := prod_filter_ne_one.symm
-        _ = ∏ x in t.filter fun x => g x ≠ 1, g x :=
-          prod_bij (fun a ha => i a (mem_filter.mp ha).1 $ by simpa using (mem_filter.mp ha).2)
-            _ _ _ _
-        _ = ∏ x in t, g x := prod_filter_ne_one
+  classical
+  calc
+    (∏ x in s, f x) = ∏ x in s.filter fun x => f x ≠ 1, f x := prod_filter_ne_one.symm
+    _ = ∏ x in t.filter fun x => g x ≠ 1, g x :=
+      prod_bij (fun a ha => i a (mem_filter.mp ha).1 $ by simpa using (mem_filter.mp ha).2)
+        ?_ ?_ ?_ ?_
+    _ = ∏ x in t, g x := prod_filter_ne_one
   · intros a ha
     refine' (mem_filter.mp ha).elim _
     intros h₁ h₂
@@ -1134,8 +1131,7 @@ theorem prod_bij_ne_one {s : Finset α} {t : Finset γ} {f : α → β} {g : γ
   · intros b hb
     refine' (mem_filter.mp hb).elim fun h₁ h₂ ↦ _
     obtain ⟨a, ha₁, ha₂, eq⟩ := i_surj b h₁ fun H ↦ by rw [H] at h₂; simp at h₂
-    refine' ⟨a, mem_filter.mpr ⟨ha₁, _⟩, eq⟩
-    classical exact decide_eq_true ha₂
+    exact ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩
 
 #align finset.prod_bij_ne_one Finset.prod_bij_ne_one
 #align finset.sum_bij_ne_zero Finset.sum_bij_ne_zero
@@ -1565,12 +1561,9 @@ theorem prod_cancels_of_partition_cancels (R : Setoid α) [DecidableRel R.r]
     (h : ∀ x ∈ s, (∏ a in s.filter fun y => y ≈ x, f a) = 1) : (∏ x in s, f x) = 1 := by
   rw [prod_partition R, ← Finset.prod_eq_one]
   intro xbar xbar_in_s
-  obtain ⟨x, x_in_s, xbar_eq_x⟩ := mem_image.mp xbar_in_s
-  rw [← xbar_eq_x, filter_congr]
-  · apply h x x_in_s
-  · intros
-    simp only [decide_eq_true_eq, ← Quotient.eq]
-    rfl
+  obtain ⟨x, x_in_s, rfl⟩ := mem_image.mp xbar_in_s
+  simp only [← Quotient.eq] at h
+  exact h x x_in_s
 #align finset.prod_cancels_of_partition_cancels Finset.prod_cancels_of_partition_cancels
 #align finset.sum_cancels_of_partition_cancels Finset.sum_cancels_of_partition_cancels
 

Mathlib/Algebra/FreeMonoid/Count.lean

@@ -26,12 +26,10 @@ variable {α : Type _} (p : α → Prop) [DecidablePred p]
 namespace FreeAddMonoid
 
 /-- `List.countp` as a bundled additive monoid homomorphism. -/
--- Porting note: changed the type of `p : α → Prop` to `p : α → Bool` to match the
--- change in `List.countp`
-def countp (p : α → Bool): FreeAddMonoid α →+ ℕ where
+def countp : FreeAddMonoid α →+ ℕ where
   toFun := List.countp p
-  map_zero' := List.countp_nil p
-  map_add' := List.countp_append p
+  map_zero' := List.countp_nil _
+  map_add' := List.countp_append _
 #align free_add_monoid.countp FreeAddMonoid.countp
 
 theorem countp_of (x : α): countp p (of x) = if p x = true then 1 else 0 := by
@@ -42,9 +40,8 @@ theorem countp_apply (l : FreeAddMonoid α) : countp p l = List.countp p l := rf
 #align free_add_monoid.countp_apply FreeAddMonoid.countp_apply
 
 /-- `List.count` as a bundled additive monoid homomorphism. -/
--- Porting note: changed from `countp (Eq x)` to match the definition of `List.count` and thus
--- we can prove `count_apply` by `rfl`
-def count [DecidableEq α] (x : α) : FreeAddMonoid α →+ ℕ := countp (· == x)
+-- Porting note: was (x = ·)
+def count [DecidableEq α] (x : α) : FreeAddMonoid α →+ ℕ := countp (· = x)
 #align free_add_monoid.count FreeAddMonoid.count
 
 theorem count_of [DecidableEq α] (x y : α) : count x (of y) = (Pi.single x 1 : α → ℕ) y := by
@@ -61,21 +58,17 @@ end FreeAddMonoid
 namespace FreeMonoid
 
 /-- `list.countp` as a bundled multiplicative monoid homomorphism. -/
--- Porting note: changed the type of `p : α → Prop` to `p : α → Bool` to match the
--- definition of `FreeAddMonoid.countp`
-def countp (p : α → Bool): FreeMonoid α →* Multiplicative ℕ :=
+def countp : FreeMonoid α →* Multiplicative ℕ :=
     AddMonoidHom.toMultiplicative (FreeAddMonoid.countp p)
 #align free_monoid.countp FreeMonoid.countp
 
--- Porting note: changed the type of `p : α → Prop` to `p : α → Bool` and `if` to `bif`
-theorem countp_of' (x : α) (p : α → Bool):
-    countp p (of x) = bif p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0 := by
-    simp [countp]
-    exact AddMonoidHom.toMultiplicative_apply_apply (FreeAddMonoid.countp p) (of x)
+theorem countp_of' (x : α) :
+    countp p (of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0 := by
+    erw [FreeAddMonoid.countp_of]
+    simp only [eq_iff_iff, iff_true, ofAdd_zero]; rfl
 #align free_monoid.countp_of' FreeMonoid.countp_of'
 
--- Porting note: changed `if` to `bif`
-theorem countp_of (x : α) : countp p (of x) = bif p x then Multiplicative.ofAdd 1 else 1 := by
+theorem countp_of (x : α) : countp p (of x) = if p x then Multiplicative.ofAdd 1 else 1 := by
   rw [countp_of', ofAdd_zero]
 #align free_monoid.countp_of FreeMonoid.countp_of
 
@@ -85,7 +78,7 @@ theorem countp_apply (l : FreeAddMonoid α) : countp p l = Multiplicative.ofAdd
 #align free_monoid.countp_apply FreeMonoid.countp_apply
 
 /-- `List.count` as a bundled additive monoid homomorphism. -/
-def count [DecidableEq α] (x : α) : FreeMonoid α →* Multiplicative ℕ := countp (· == x)
+def count [DecidableEq α] (x : α) : FreeMonoid α →* Multiplicative ℕ := countp (· = x)
 #align free_monoid.count FreeMonoid.count
 
 theorem count_apply [DecidableEq α] (x : α) (l : FreeAddMonoid α) :

Mathlib/Algebra/GCDMonoid/Finset.lean

@@ -230,18 +230,16 @@ all the `decide`s around. -/
 theorem gcd_eq_gcd_filter_ne_zero [DecidablePred fun x : β ↦ f x = 0] :
     s.gcd f = (s.filter fun x ↦ f x ≠ 0).gcd f := by
   classical
-    trans ((s.filter fun x ↦ f x = 0) ∪ s.filter fun x ↦ (¬decide (f x = 0) = true)).gcd f
+    trans ((s.filter fun x ↦ f x = 0) ∪ s.filter fun x ↦ (f x ≠ 0)).gcd f
     · rw [filter_union_filter_neg_eq]
     rw [gcd_union]
     refine' Eq.trans (_ : _ = GCDMonoid.gcd (0 : α) _) (_ : GCDMonoid.gcd (0 : α) _ = _)
-    · exact (gcd (filter (fun x => decide (f x ≠ 0)) s) f)
+    · exact (gcd (filter (fun x => (f x ≠ 0)) s) f)
     · refine' congr (congr rfl <| s.induction_on _ _) (by simp)
       · simp
       · intro a s _ h
         rw [filter_insert]
-        split_ifs with h1 <;>
-        · simp only [decide_eq_true_eq] at h1
-          simp [h, h1]
+        split_ifs with h1 <;> simp [h, h1]
     simp only [gcd_zero_left, normalize_gcd]
 #align finset.gcd_eq_gcd_filter_ne_zero Finset.gcd_eq_gcd_filter_ne_zero
 

Mathlib/Combinatorics/SetFamily/Compression/Down.lean

@@ -67,7 +67,6 @@ theorem mem_memberSubfamily : s ∈ 𝒜.memberSubfamily a ↔ insert a s ∈ 
   simp_rw [memberSubfamily, mem_image, mem_filter]
   refine' ⟨_, fun h => ⟨insert a s, ⟨h.1, by simp⟩, erase_insert h.2⟩⟩
   rintro ⟨s, ⟨hs1, hs2⟩, rfl⟩
-  rw [decide_eq_true_eq] at hs2
   rw [insert_erase hs2]
   exact ⟨hs1, not_mem_erase _ _⟩
 #align finset.mem_member_subfamily Finset.mem_memberSubfamily
@@ -100,7 +99,6 @@ theorem card_memberSubfamily_add_card_nonMemberSubfamily (a : α) (𝒜 : Finset
   by
   rw [memberSubfamily, nonMemberSubfamily, card_image_of_injOn]
   · conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun s => (a ∈ s))]
-    simp
   · apply (erase_injOn' _).mono
     simp
 #align
@@ -169,7 +167,6 @@ def compression (a : α) (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
       ((𝒜.image fun s => erase s a).filter fun s => s ∉ 𝒜) <|
     disjoint_left.2 fun s h₁ h₂ => by
       have := (mem_filter.1 h₂).2
-      rw [decide_eq_true_iff] at this
       exact this (mem_filter.1 h₁).1
 #align down.compression Down.compression
 
@@ -234,14 +231,9 @@ theorem card_compression (a : α) (𝒜 : Finset (Finset α)) : (𝓓 a 𝒜).ca
   rw [compression, card_disjUnion, image_filter,
     card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_disjoint_union]
   · conv_rhs => rw [← filter_union_filter_neg_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
-    congr
-    ext
-    simp
   · convert disjoint_filter_filter_neg 𝒜 𝒜 (fun s => (erase s a ∈ 𝒜))
-    ext
-    simp
   intro s hs
-  rw [mem_coe, mem_filter, Function.comp_apply, decide_eq_true_iff] at hs
+  rw [mem_coe, mem_filter, Function.comp_apply] at hs
   convert not_imp_comm.1 erase_eq_of_not_mem (ne_of_mem_of_not_mem hs.1 hs.2).symm
 #align down.card_compression Down.card_compression
 

Mathlib/Data/Finset/Basic.lean

@@ -70,7 +70,7 @@ This is then used to define `Fintype.card`, the size of a type.
 
 ### Finsets from functions
 
-* `Finset.filter`: Given a predicate `p : α → Bool`, `s.filter p` is
+* `Finset.filter`: Given a decidable predicate `p : α → Prop`, `s.filter p` is
   the finset consisting of those elements in `s` satisfying the predicate `p`.
 
 ### The lattice structure on subsets of finsets
@@ -2520,8 +2520,7 @@ end DecidablePiExists
 
 section Filter
 
--- Porting note: changed from `α → Prop`.
-variable (p q : α → Bool)
+variable (p q : α → Prop) [DecidablePred p] [DecidablePred q]
 
 /-- `filter p s` is the set of elements of `s` that satisfy `p`. -/
 def filter (s : Finset α) : Finset α :=
@@ -2563,14 +2562,14 @@ theorem filter_filter (s : Finset α) : (s.filter p).filter q = s.filter fun a =
     simp only [mem_filter, and_assoc, Bool.decide_and, Bool.decide_coe, Bool.and_eq_true]
 #align finset.filter_filter Finset.filter_filter
 
-theorem filter_true {s : Finset α} : Finset.filter (fun _ => true) s = s := by
+theorem filter_True {s : Finset α} : Finset.filter (fun _ => True) s = s := by
   ext; simp
-#align finset.filter_true Finset.filter_true
+#align finset.filter_true Finset.filter_True
 
 @[simp]
-theorem filter_false (s : Finset α) : filter (fun _ => false) s = ∅ :=
+theorem filter_False (s : Finset α) : filter (fun _ => False) s = ∅ :=
   ext fun a => by simp [mem_filter, and_false_iff]
-#align finset.filter_false Finset.filter_false
+#align finset.filter_false Finset.filter_False
 
 variable {p q}
 
@@ -2617,9 +2616,8 @@ theorem filter_subset_filter {s t : Finset α} (h : s ⊆ t) : s.filter p ⊆ t.
 theorem monotone_filter_left : Monotone (filter p) := fun _ _ => filter_subset_filter p
 #align finset.monotone_filter_left Finset.monotone_filter_left
 
--- Porting note: was `p q : α → Prop, h : p ≤ q`.
-theorem monotone_filter_right (s : Finset α) ⦃p q : α → Bool⦄
-    (h : ∀ a, p a → q a) : s.filter p ≤ s.filter q :=
+theorem monotone_filter_right (s : Finset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q]
+    (h : p ≤ q) : s.filter p ≤ s.filter q :=
   Multiset.subset_of_le (Multiset.monotone_filter_right s.val h)
 #align finset.monotone_filter_right Finset.monotone_filter_right
 
@@ -2649,25 +2647,28 @@ theorem filter_cons_of_neg (a : α) (s : Finset α) (ha : a ∉ s) (hp : ¬p a)
   eq_of_veq <| Multiset.filter_cons_of_neg s.val hp
 #align finset.filter_cons_of_neg Finset.filter_cons_of_neg
 
-theorem disjoint_filter {s : Finset α} {p q : α → Bool} :
+theorem disjoint_filter {s : Finset α} {p q : α → Prop} [DecidablePred p] [DecidablePred q] :
     Disjoint (s.filter p) (s.filter q) ↔ ∀ x ∈ s, p x → ¬q x := by
   constructor <;> simp (config := { contextual := true }) [disjoint_left]
 #align finset.disjoint_filter Finset.disjoint_filter
 
-theorem disjoint_filter_filter {s t : Finset α} {p q : α → Bool} :
+theorem disjoint_filter_filter {s t : Finset α}
+    {p q : α → Prop} [DecidablePred p] [DecidablePred q] :
     Disjoint s t → Disjoint (s.filter p) (t.filter q) :=
   Disjoint.mono (filter_subset _ _) (filter_subset _ _)
 #align finset.disjoint_filter_filter Finset.disjoint_filter_filter
 
-theorem disjoint_filter_filter' (s t : Finset α) {p q : α → Bool} (h : Disjoint p q) :
+theorem disjoint_filter_filter' (s t : Finset α)
+    {p q : α → Prop} [DecidablePred p] [DecidablePred q] (h : Disjoint p q) :
     Disjoint (s.filter p) (t.filter q) := by
   simp_rw [disjoint_left, mem_filter]
   rintro a ⟨_, hp⟩ ⟨_, hq⟩
   rw [Pi.disjoint_iff] at h
   simpa [hp, hq] using h a
 #align finset.disjoint_filter_filter' Finset.disjoint_filter_filter'
 
-theorem disjoint_filter_filter_neg (s t : Finset α) (p : α → Bool) :
+theorem disjoint_filter_filter_neg (s t : Finset α) (p : α → Prop)
+    [DecidablePred p] [∀ x, Decidable (¬p x)] :
     Disjoint (s.filter p) (t.filter fun a => ¬p a) := by
   simp_rw [decide_not, Bool.decide_coe, Bool.not_eq_true']
   exact disjoint_filter_filter' s t disjoint_compl_right
@@ -2839,16 +2840,12 @@ theorem filter_inter_filter_neg_eq (s t : Finset α) :
 
 theorem filter_union_filter_of_codisjoint (s : Finset α) (h : Codisjoint p q) :
     s.filter p ∪ s.filter q = s :=
-  (filter_or _ _ _).symm.trans <| filter_true_of_mem fun x _ => by
-    simpa [Bool.le_iff_imp] using h.top_le x
+  (filter_or _ _ _).symm.trans <| filter_true_of_mem fun x _ => h.top_le x trivial
 #align finset.filter_union_filter_of_codisjoint Finset.filter_union_filter_of_codisjoint
 
-theorem filter_union_filter_neg_eq (s : Finset α) :
+theorem filter_union_filter_neg_eq [∀ x, Decidable (¬p x)] (s : Finset α) :
     (s.filter p ∪ s.filter fun a => ¬p a) = s :=
-  filter_union_filter_of_codisjoint _ _ _ <| by
-    convert @codisjoint_hnot_right _ _ p
-    ext a
-    simp only [decide_not, hnot_eq_compl, Bool.decide_coe, Pi.compl_apply, Bool.compl_eq_bnot]
+  filter_union_filter_of_codisjoint _ _ _ <| @codisjoint_hnot_right _ _ p
 #align finset.filter_union_filter_neg_eq Finset.filter_union_filter_neg_eq
 
 end Filter

Mathlib/Data/Finset/Card.lean

@@ -282,7 +282,7 @@ theorem map_eq_of_subset {f : α ↪ α} (hs : s.map f ⊆ s) : s.map f = s :=
 
 theorem filter_card_eq {p : α → Prop} [DecidablePred p] (h : (s.filter p).card = s.card) (x : α)
     (hx : x ∈ s) : p x := by
-  rw [← eq_of_subset_of_card_le (s.filter_subset p) h.ge, mem_filter, decide_eq_true_eq] at hx
+  rw [← eq_of_subset_of_card_le (s.filter_subset p) h.ge, mem_filter] at hx
   exact hx.2
 #align finset.filter_card_eq Finset.filter_card_eq
 
@@ -459,7 +459,8 @@ theorem card_sdiff_add_card : (s \ t).card + t.card = (s ∪ t).card := by
 
 end Lattice
 
-theorem filter_card_add_filter_neg_card_eq_card (p : α → Bool) :
+theorem filter_card_add_filter_neg_card_eq_card
+    (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] :
     (s.filter p).card + (s.filter (fun a => ¬ p a)).card = s.card := by
   classical rw [← card_union_eq (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]
 #align finset.filter_card_add_filter_neg_card_eq_card

Mathlib/Data/Finset/Fold.lean

@@ -150,7 +150,7 @@ theorem fold_ite' {g : α → β} (hb : op b b = b) (p : α → Prop) [Decidable
       split_ifs with h
       · have : x ∉ Finset.filter p s := by simp [hx]
         simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
-      · have : x ∉ Finset.filter (fun i => !p i) s := by simp [hx]
+      · have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
         simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
 #align finset.fold_ite' Finset.fold_ite'
 

Mathlib/Data/Finset/NatAntidiagonal.lean

@@ -123,7 +123,7 @@ theorem filter_fst_eq_antidiagonal (n m : ℕ) :
 
 theorem filter_snd_eq_antidiagonal (n m : ℕ) :
     filter (fun x : ℕ × ℕ ↦ x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅ := by
-  have : (fun x : ℕ × ℕ ↦ (x.snd = m : Bool)) ∘ Prod.swap = fun x : ℕ × ℕ ↦ x.fst = m := by
+  have : (fun x : ℕ × ℕ ↦ (x.snd = m)) ∘ Prod.swap = fun x : ℕ × ℕ ↦ x.fst = m := by
     ext ; simp
   rw [← map_swap_antidiagonal]
   simp [filter_map, this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]