feat: Fintype.prod_ite_mem (#17017)

This specializes the existing `Finset.prod_ite_mem`. From LeanAPAP
leanprover-community · Sep 22, 2024 · ed1a8a0 · ed1a8a0
1 parent da16ebc
commit ed1a8a0
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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