[Merged by Bors] - feat(Algebra/BigOperators/Group/Finset) : Finset.prod_disjoint_filters

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -426,6 +426,13 @@ lemma prod_filter_not_mul_prod_filter (s : Finset α) (p : α → Prop) [Decidab
     (∏ x ∈ s.filter fun x ↦ ¬p x, f x) * ∏ x ∈ s.filter p, f x = ∏ x ∈ s, f x := by
   rw [mul_comm, prod_filter_mul_prod_filter_not]
 
+@[to_additive]
+theorem prod_disjoint_filters (p q : α → Prop) [DecidableEq α] [DecidablePred p] [DecidablePred q] :
+    (∏ x ∈ s with (Xor' (p x) (q x)), f x) =
+      (∏ x ∈ s with (p x ∧ ¬ q x), f x) * (∏ x ∈ s with (q x ∧ ¬ p x), f x) := by
+  rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]
+  rfl
+
 section ToList
 
 @[to_additive (attr := simp)]

Mathlib/Data/Finset/Filter.lean

@@ -214,6 +214,15 @@ lemma _root_.Set.pairwiseDisjoint_filter [DecidableEq β] (f : α → β) (s : S
   obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = j := by simpa using hj hx
   contradiction
 
+theorem disjoint_filter_and_not_filter :
+    Disjoint (s.filter (fun x ↦ p x ∧ ¬q x)) (s.filter (fun x ↦ q x ∧ ¬p x)) := by
+  intro _ htp htq
+  simp [bot_eq_empty, le_eq_subset, subset_empty]
+  by_contra hn
+  rw [← not_nonempty_iff_eq_empty, not_not] at hn
+  obtain ⟨_, hx⟩ := hn
+  exact (mem_filter.mp (htq hx)).2.2 (mem_filter.mp (htp hx)).2.1
+
 variable {p q}
 
 lemma filter_inj : s.filter p = t.filter p ↔ ∀ ⦃a⦄, p a → (a ∈ s ↔ a ∈ t) := by