From ed1a8a0388eaba24956bf1eac9a29ac36e5f314a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sun, 22 Sep 2024 18:19:50 +0000
Subject: [PATCH] feat: `Fintype.prod_ite_mem` (#17017)

This specializes the existing `Finset.prod_ite_mem`.

From LeanAPAP
---
 Mathlib/Algebra/BigOperators/Group/Finset.lean     | 4 ++++
 Mathlib/Algebra/Module/BigOperators.lean           | 2 +-
 Mathlib/Combinatorics/SetFamily/FourFunctions.lean | 2 +-
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset.lean b/Mathlib/Algebra/BigOperators/Group/Finset.lean
index d4e712285b4a5..c418a20c2dc75 100644
--- a/Mathlib/Algebra/BigOperators/Group/Finset.lean
+++ b/Mathlib/Algebra/BigOperators/Group/Finset.lean
@@ -2008,6 +2008,10 @@ lemma prod_ite_eq_ite_exists (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p
 
 variable [DecidableEq ι]
 
+@[to_additive]
+lemma prod_ite_mem (s : Finset ι) (f : ι → α) : ∏ i, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i := by
+  simp
+
 /-- See also `Finset.prod_dite_eq`. -/
 @[to_additive "See also `Finset.sum_dite_eq`."] lemma prod_dite_eq (i : ι) (f : ∀ j, i = j → α) :
     ∏ j, (if h : i = j then f j h else 1) = f i rfl := by
diff --git a/Mathlib/Algebra/Module/BigOperators.lean b/Mathlib/Algebra/Module/BigOperators.lean
index 6c34557954a88..8b68d57357fd4 100644
--- a/Mathlib/Algebra/Module/BigOperators.lean
+++ b/Mathlib/Algebra/Module/BigOperators.lean
@@ -54,6 +54,6 @@ lemma sum_piFinset_apply (f : κ → α) (s : Finset κ) (i : ι) :
   classical
   rw [Finset.sum_comp]
   simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum,
-    sum_ite_mem, inter_self]
+    Finset.sum_ite_mem, inter_self]
 
 end Fintype
diff --git a/Mathlib/Combinatorics/SetFamily/FourFunctions.lean b/Mathlib/Combinatorics/SetFamily/FourFunctions.lean
index 2c7b78ec4d1b5..d3bd37943cd19 100644
--- a/Mathlib/Combinatorics/SetFamily/FourFunctions.lean
+++ b/Mathlib/Combinatorics/SetFamily/FourFunctions.lean
@@ -219,7 +219,7 @@ lemma sum_collapse (h𝒜 : 𝒜 ⊆ (insert a u).powerset) (hu : a ∉ u) :
     _ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ u.powerset.image (insert a) ∩ 𝒜, f s := ?_
     _ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ ((insert a u).powerset \ u.powerset) ∩ 𝒜, f s := ?_
     _ = ∑ s ∈ 𝒜, f s := ?_
-  · rw [← sum_ite_mem, ← sum_ite_mem, sum_image, ← sum_add_distrib]
+  · rw [← Finset.sum_ite_mem, ← Finset.sum_ite_mem, sum_image, ← sum_add_distrib]
     · exact sum_congr rfl fun s hs ↦ collapse_eq (not_mem_mono (mem_powerset.1 hs) hu) _ _
     · exact (insert_erase_invOn.2.injOn).mono fun s hs ↦ not_mem_mono (mem_powerset.1 hs) hu
   · congr with s