diff --git a/Mathlib/Algebra/BigOperators/Group/Finset.lean b/Mathlib/Algebra/BigOperators/Group/Finset.lean
index c235e6c2bd74a3..34cd0b147e8193 100644
--- a/Mathlib/Algebra/BigOperators/Group/Finset.lean
+++ b/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_filter_xor (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)]
diff --git a/Mathlib/Data/Finset/Filter.lean b/Mathlib/Data/Finset/Filter.lean
index d42d8d22414fa2..746efb17234052 100644
--- a/Mathlib/Data/Finset/Filter.lean
+++ b/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