feat: More big operator lemmas (#10551)

From LeanAPAP

Author: YaelDillies

Mathlib/Algebra/BigOperators/Basic.lean

@@ -667,6 +667,19 @@ lemma prod_of_injOn (e : ι → κ) (he : Set.InjOn e s) (hest : Set.MapsTo e s
 
 variable [DecidableEq κ]
 
+@[to_additive]
+lemma prod_fiberwise_eq_prod_filter (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → α) :
+    ∏ j in t, ∏ i in s.filter fun i ↦ g i = j, f i = ∏ i in s.filter fun i ↦ g i ∈ t, f i := by
+  rw [← prod_disjiUnion, disjiUnion_filter_eq]
+
+@[to_additive]
+lemma prod_fiberwise_eq_prod_filter' (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → α) :
+    ∏ j in t, ∏ _i in s.filter fun i ↦ g i = j, f j = ∏ i in s.filter fun i ↦ g i ∈ t, f (g i) := by
+  calc
+    _ = ∏ j in t, ∏ i in s.filter fun i ↦ g i = j, f (g i) :=
+        prod_congr rfl fun j _ ↦ prod_congr rfl fun i hi ↦ by rw [(mem_filter.1 hi).2]
+    _ = _ := prod_fiberwise_eq_prod_filter _ _ _ _
+
 @[to_additive]
 lemma prod_fiberwise_of_maps_to {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → α) :
     ∏ j in t, ∏ i in s.filter fun i ↦ g i = j, f i = ∏ i in s, f i := by
@@ -1945,6 +1958,23 @@ theorem prod_dvd_prod_of_subset {ι M : Type*} [CommMonoid M] (s t : Finset ι)
 
 end CommMonoid
 
+section CancelCommMonoid
+variable [DecidableEq ι] [CancelCommMonoid α] {s t : Finset ι} {f : ι → α}
+
+@[to_additive]
+lemma prod_sdiff_eq_prod_sdiff_iff :
+    ∏ i in s \ t, f i = ∏ i in t \ s, f i ↔ ∏ i in s, f i = ∏ i in t, f i :=
+  eq_comm.trans $ eq_iff_eq_of_mul_eq_mul $ by
+    rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left,
+      sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm]
+
+@[to_additive]
+lemma prod_sdiff_ne_prod_sdiff_iff :
+    ∏ i in s \ t, f i ≠ ∏ i in t \ s, f i ↔ ∏ i in s, f i ≠ ∏ i in t, f i :=
+  prod_sdiff_eq_prod_sdiff_iff.not
+
+end CancelCommMonoid
+
 theorem card_eq_sum_ones (s : Finset α) : s.card = ∑ x in s, 1 := by
   rw [sum_const, smul_eq_mul, mul_one]
 #align finset.card_eq_sum_ones Finset.card_eq_sum_ones
@@ -1955,6 +1985,10 @@ theorem sum_const_nat {m : ℕ} {f : α → ℕ} (h₁ : ∀ x ∈ s, f x = m) :
   apply sum_congr rfl h₁
 #align finset.sum_const_nat Finset.sum_const_nat
 
+lemma sum_card_fiberwise_eq_card_filter {κ : Type*} [DecidableEq κ] (s : Finset ι) (t : Finset κ)
+    (g : ι → κ) : ∑ j in t, (s.filter fun i ↦ g i = j).card = (s.filter fun i ↦ g i ∈ t).card := by
+  simpa only [card_eq_sum_ones] using sum_fiberwise_eq_sum_filter _ _ _ _
+
 lemma card_filter (p) [DecidablePred p] (s : Finset α) :
     (filter p s).card = ∑ a in s, ite (p a) 1 0 := by
   rw [sum_ite, sum_const_zero, add_zero, sum_const, smul_eq_mul, mul_one]
@@ -2156,10 +2190,13 @@ theorem prod_int_mod (s : Finset α) (n : ℤ) (f : α → ℤ) :
 end Finset
 
 namespace Fintype
-variable {ι κ α : Type*} [Fintype ι] [Fintype κ] [CommMonoid α]
+variable {ι κ α : Type*} [Fintype ι] [Fintype κ]
 
 open Finset
 
+section CommMonoid
+variable [CommMonoid α]
+
 /-- `Fintype.prod_bijective` is a variant of `Finset.prod_bij` that accepts `Function.Bijective`.
 
 See `Function.Bijective.prod_comp` for a version without `h`. -/
@@ -2256,6 +2293,52 @@ theorem prod_subtype_mul_prod_subtype {α β : Type*} [Fintype α] [CommMonoid 
 #align fintype.prod_subtype_mul_prod_subtype Fintype.prod_subtype_mul_prod_subtype
 #align fintype.sum_subtype_add_sum_subtype Fintype.sum_subtype_add_sum_subtype
 
+@[to_additive] lemma prod_subset {s : Finset ι} {f : ι → α} (h : ∀ i, f i ≠ 1 → i ∈ s) :
+    ∏ i in s, f i = ∏ i, f i :=
+  Finset.prod_subset s.subset_univ $ by simpa [not_imp_comm (a := _ ∈ s)]
+
+@[to_additive]
+lemma prod_ite_eq_ite_exists (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j)
+    (a : α) : ∏ i, ite (p i) a 1 = ite (∃ i, p i) a 1 := by
+  simp [prod_ite_one univ p (by simpa using h)]
+
+variable [DecidableEq ι]
+
+/-- 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
+  rw [Finset.prod_dite_eq, if_pos (mem_univ _)]
+
+/-- See also `Finset.prod_dite_eq'`. -/
+@[to_additive "See also `Finset.sum_dite_eq'`."] lemma prod_dite_eq' (i : ι) (f : ∀ j, j = i → α) :
+    ∏ j, (if h : j = i then f j h else 1) = f i rfl := by
+  rw [Finset.prod_dite_eq', if_pos (mem_univ _)]
+
+/-- See also `Finset.prod_ite_eq`. -/
+@[to_additive "See also `Finset.sum_ite_eq`."]
+lemma prod_ite_eq (i : ι) (f : ι → α) : ∏ j, (if i = j then f j else 1) = f i := by
+  rw [Finset.prod_ite_eq, if_pos (mem_univ _)]
+
+/-- See also `Finset.prod_ite_eq'`. -/
+@[to_additive "See also `Finset.sum_ite_eq'`."]
+lemma prod_ite_eq' (i : ι) (f : ι → α) : ∏ j, (if j = i then f j else 1) = f i := by
+  rw [Finset.prod_ite_eq', if_pos (mem_univ _)]
+
+/-- See also `Finset.prod_pi_mulSingle`. -/
+@[to_additive "See also `Finset.sum_pi_single`."]
+lemma prod_pi_mulSingle {α : ι → Type*} [∀ i, CommMonoid (α i)] (i : ι) (f : ∀ i, α i) :
+    ∏ j, Pi.mulSingle j (f j) i = f i := prod_dite_eq _ _
+
+/-- See also `Finset.prod_pi_mulSingle'`. -/
+@[to_additive "See also `Finset.sum_pi_single'`."]
+lemma prod_pi_mulSingle' (i : ι) (a : α) : ∏ j, Pi.mulSingle i a j = a := prod_dite_eq' _ _
+
+end CommMonoid
+
+variable [CommMonoidWithZero α] {p : ι → Prop} [DecidablePred p]
+
+lemma prod_boole : ∏ i, ite (p i) (1 : α) 0 = ite (∀ i, p i) 1 0 := by simp [Finset.prod_boole]
+
 end Fintype
 
 namespace Finset

Mathlib/Algebra/BigOperators/Ring.lean

@@ -170,11 +170,11 @@ lemma prod_univ_sum [Fintype ι] (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i →
 
 lemma sum_prod_piFinset {κ : Type*} [Fintype ι] (s : Finset κ) (g : ι → κ → α) :
     ∑ f in piFinset fun _ : ι ↦ s, ∏ i, g i (f i) = ∏ i, ∑ j in s, g i j := by
-  classical rw [← prod_univ_sum]
+  rw [← prod_univ_sum]
 
 lemma sum_pow' (s : Finset ι) (f : ι → α) (n : ℕ) :
     (∑ a in s, f a) ^ n = ∑ p in piFinset fun _i : Fin n ↦ s, ∏ i, f (p i) := by
-  classical convert @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp
+  convert @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp
 
 /-- The product of `f a + g a` over all of `s` is the sum over the powerset of `s` of the product of
 `f` over a subset `t` times the product of `g` over the complement of `t`  -/
@@ -297,7 +297,31 @@ lemma sum_div (s : Finset ι) (f : ι → α) (a : α) :
 end DivisionSemiring
 end Finset
 
+open Finset
+
+namespace Fintype
+variable {ι κ α : Type*} [DecidableEq ι] [Fintype ι] [Fintype κ] [CommSemiring α]
+
+lemma sum_pow (f : ι → α) (n : ℕ) : (∑ a, f a) ^ n = ∑ p : Fin n → ι, ∏ i, f (p i) := by
+  simp [sum_pow']
+
+lemma sum_mul_sum (f : ι → α) (g : κ → α) : (∑ i, f i) * ∑ j, g j = ∑ i, ∑ j, f i * g j :=
+  Finset.sum_mul_sum _ _ _ _
+
+lemma prod_add (f g : ι → α) : ∏ a, (f a + g a) = ∑ t, (∏ a in t, f a) * ∏ a in tᶜ, g a := by
+  simpa [compl_eq_univ_sdiff] using Finset.prod_add f g univ
+
+end Fintype
+
 namespace Nat
+variable {ι : Type*} {s : Finset ι} {f : ι → ℕ} {n : ℕ}
+
+protected lemma sum_div (hf : ∀ i ∈ s, n ∣ f i) : (∑ i in s, f i) / n = ∑ i in s, f i / n := by
+  obtain rfl | hn := n.eq_zero_or_pos
+  · simp
+  rw [Nat.div_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]
+  refine' sum_congr rfl fun s hs ↦ _
+  rw [Nat.div_mul_cancel (hf _ hs)]
 
 @[simp, norm_cast]
 lemma cast_list_sum [AddMonoidWithOne β] (s : List ℕ) : (↑s.sum : β) = (s.map (↑)).sum :=

Mathlib/Algebra/Module/BigOperators.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yury Kudryashov, Yaël Dillies
 -/
 import Mathlib.Algebra.Module.Defs
+import Mathlib.Data.Fintype.BigOperators
 import Mathlib.GroupTheory.GroupAction.BigOperators
 
 #align_import algebra.module.big_operators from "leanprover-community/mathlib"@"509de852e1de55e1efa8eacfa11df0823f26f226"
@@ -14,7 +15,7 @@ import Mathlib.GroupTheory.GroupAction.BigOperators
 
 open BigOperators
 
-variable {α β R M ι : Type*}
+variable {ι κ α β R M : Type*}
 
 section AddCommMonoid
 
@@ -51,3 +52,17 @@ end AddCommMonoid
 theorem Finset.cast_card [CommSemiring R] (s : Finset α) : (s.card : R) = ∑ a in s, 1 := by
   rw [Finset.sum_const, Nat.smul_one_eq_coe]
 #align finset.cast_card Finset.cast_card
+
+open Finset
+
+namespace Fintype
+variable [DecidableEq ι] [Fintype ι] [AddCommMonoid α]
+
+lemma sum_piFinset_apply (f : κ → α) (s : Finset κ) (i : ι) :
+    ∑ g in piFinset fun _ : ι ↦ s, f (g i) = s.card ^ (card ι - 1) • ∑ b in s, f b := by
+  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]
+
+end Fintype

Mathlib/Data/Finset/Basic.lean

@@ -2631,7 +2631,7 @@ theorem filter_False {h} (s : Finset α) : @filter _ (fun _ => False) h s = ∅
 
 variable {p q}
 
-theorem filter_eq_self : s.filter p = s ↔ ∀ x ∈ s, p x := by simp [Finset.ext_iff]
+@[simp] lemma filter_eq_self : s.filter p = s ↔ ∀ x ∈ s, p x := by simp [Finset.ext_iff]
 #align finset.filter_eq_self Finset.filter_eq_self
 
 theorem filter_eq_empty_iff : s.filter p = ∅ ↔ ∀ ⦃x⦄, x ∈ s → ¬p x := by simp [Finset.ext_iff]

Mathlib/Data/Finset/Union.lean

@@ -88,14 +88,20 @@ lemma disjiUnion_disjiUnion (s : Finset α) (f : α → Finset β) (g : β → F
   eq_of_veq <| Multiset.bind_assoc.trans (Multiset.attach_bind_coe _ _).symm
 #align finset.disj_Union_disj_Union Finset.disjiUnion_disjiUnion
 
-lemma disjiUnion_filter_eq_of_maps_to [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
-    (h : ∀ x ∈ s, f x ∈ t) :
-    t.disjiUnion (fun a ↦ s.filter (fun c ↦ f c = a))
-      (fun x' hx y' hy hne ↦ by
-        simp_rw [disjoint_left, mem_filter]
-        rintro i ⟨_, rfl⟩ ⟨_, rfl⟩
-        exact hne rfl) = s :=
-  ext fun b ↦ by simpa using h b
+variable [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
+
+private lemma pairwiseDisjoint_fibers : Set.PairwiseDisjoint ↑t fun a ↦ s.filter (f · = a) :=
+  fun x' hx y' hy hne ↦ by
+    simp_rw [disjoint_left, mem_filter]; rintro i ⟨_, rfl⟩ ⟨_, rfl⟩; exact hne rfl
+
+-- `simpNF` claims that the statement can't simplify itself, but it can (as of 2024-02-14)
+@[simp, nolint simpNF] lemma disjiUnion_filter_eq (s : Finset α) (t : Finset β) (f : α → β) :
+    t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers =
+      s.filter fun c ↦ f c ∈ t :=
+  ext fun b => by simpa using and_comm
+
+lemma disjiUnion_filter_eq_of_maps_to (h : ∀ x ∈ s, f x ∈ t) :
+    t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers = s := by simpa
 #align finset.disj_Union_filter_eq_of_maps_to Finset.disjiUnion_filter_eq_of_maps_to
 
 end DisjiUnion

Mathlib/Data/Fintype/BigOperators.lean

@@ -118,29 +118,63 @@ end
 
 open Finset
 
-@[simp]
-nonrec theorem Fintype.card_sigma {α : Type*} (β : α → Type*) [Fintype α] [∀ a, Fintype (β a)] :
-    Fintype.card (Sigma β) = ∑ a, Fintype.card (β a) :=
-  card_sigma _ _
-#align fintype.card_sigma Fintype.card_sigma
+section Pi
+variable {ι κ : Type*} {α : ι → Type*} [DecidableEq ι] [DecidableEq κ] [Fintype ι]
+  [∀ i, DecidableEq (α i)]
 
-@[simp]
-theorem Finset.card_pi [DecidableEq α] {δ : α → Type*} (s : Finset α) (t : ∀ a, Finset (δ a)) :
-    (s.pi t).card = ∏ a in s, card (t a) :=
-  Multiset.card_pi _ _
+@[simp] lemma Finset.card_pi (s : Finset ι) (t : ∀ i, Finset (α i)) :
+    (s.pi t).card = ∏ i in s, card (t i) := Multiset.card_pi _ _
 #align finset.card_pi Finset.card_pi
 
-@[simp]
-theorem Fintype.card_piFinset [DecidableEq α] [Fintype α] {δ : α → Type*} (t : ∀ a, Finset (δ a)) :
-    (Fintype.piFinset t).card = ∏ a, Finset.card (t a) := by simp [Fintype.piFinset, card_map]
+namespace Fintype
+
+@[simp] lemma card_piFinset (s : ∀ i, Finset (α i)) :
+    (piFinset s).card = ∏ i, (s i).card := by simp [piFinset, card_map]
 #align fintype.card_pi_finset Fintype.card_piFinset
 
-@[simp]
-theorem Fintype.card_pi {β : α → Type*} [DecidableEq α] [Fintype α] [∀ a, Fintype (β a)] :
-    Fintype.card (∀ a, β a) = ∏ a, Fintype.card (β a) :=
-  Fintype.card_piFinset _
+@[simp] lemma card_pi [DecidableEq ι] [∀ i, Fintype (α i)] : card (∀ i, α i) = ∏ i, card (α i) :=
+  card_piFinset _
 #align fintype.card_pi Fintype.card_pi
 
+@[simp] nonrec lemma card_sigma [Fintype ι] [∀ i, Fintype (α i)] :
+    card (Sigma α) = ∑ i, card (α i) := card_sigma _ _
+#align fintype.card_sigma Fintype.card_sigma
+
+/-- The number of dependent maps `f : Π j, s j` for which the `i` component is `a` is the product
+over all `j ≠ i` of `(s j).card`.
+
+Note that this is just a composition of easier lemmas, but there's some glue missing to make that
+smooth enough not to need this lemma. -/
+lemma card_filter_piFinset_eq_of_mem (s : ∀ i, Finset (α i)) (i : ι) {a : α i} (ha : a ∈ s i) :
+    ((piFinset s).filter fun f ↦ f i = a).card = ∏ j in univ.erase i, (s j).card := by
+  calc
+    _ = ∏ j, (Function.update s i {a} j).card := by
+      rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]
+    _ = ∏ j, Function.update (fun j ↦ (s j).card) i 1 j :=
+      Fintype.prod_congr _ _ fun j ↦ by obtain rfl | hji := eq_or_ne j i <;> simp [*]
+    _ = _ := by simp [prod_update_of_mem, erase_eq]
+
+lemma card_filter_piFinset_const_eq_of_mem (s : Finset κ) (i : ι) {x : κ} (hx : x ∈ s) :
+    ((piFinset fun _ ↦ s).filter fun f ↦ f i = x).card = s.card ^ (card ι - 1) :=
+  (card_filter_piFinset_eq_of_mem _ _ hx).trans $ by
+    rw [prod_const s.card, card_erase_of_mem (mem_univ _), card_univ]
+
+lemma card_filter_piFinset_eq (s : ∀ i, Finset (α i)) (i : ι) (a : α i) :
+    ((piFinset s).filter fun f ↦ f i = a).card =
+      if a ∈ s i then ∏ b in univ.erase i, (s b).card else 0 := by
+  split_ifs with h
+  · rw [card_filter_piFinset_eq_of_mem _ _ h]
+  · rw [filter_piFinset_of_not_mem _ _ _ h, Finset.card_empty]
+
+lemma card_filter_piFinset_const (s : Finset κ) (i : ι) (j : κ) :
+    ((piFinset fun _ ↦ s).filter fun f ↦ f i = j).card =
+      if j ∈ s then s.card ^ (card ι - 1) else 0 :=
+  (card_filter_piFinset_eq _ _ _).trans $ by
+    rw [prod_const s.card, card_erase_of_mem (mem_univ _), card_univ]
+
+end Fintype
+end Pi
+
 -- FIXME ouch, this should be in the main file.
 @[simp]
 theorem Fintype.card_fun [DecidableEq α] [Fintype α] [Fintype β] :

Mathlib/Data/Fintype/Pi.lean

@@ -97,10 +97,39 @@ lemma eval_image_piFinset (t : ∀ a, Finset (δ a)) (a : α) [DecidableEq (δ a
   choose f hf using ht
   exact ⟨fun b ↦ if h : a = b then h ▸ x else f _ h, by aesop, by simp⟩
 
-lemma filter_piFinset_of_not_mem [∀ a, DecidableEq (δ a)] (t : ∀ a, Finset (δ a)) (a : α)
-    (x : δ a) (hx : x ∉ t a) : (piFinset t).filter (· a = x) = ∅ := by
+lemma eval_image_piFinset_const {β} [DecidableEq β] (t : Finset β) (a : α) :
+    ((piFinset fun _i : α ↦ t).image fun f ↦ f a) = t := by
+  obtain rfl | ht := t.eq_empty_or_nonempty
+  · haveI : Nonempty α := ⟨a⟩
+    simp
+  · exact eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht
+
+variable [∀ a, DecidableEq (δ a)]
+
+lemma filter_piFinset_of_not_mem (t : ∀ a, Finset (δ a)) (a : α) (x : δ a) (hx : x ∉ t a) :
+    (piFinset t).filter (· a = x) = ∅ := by
   simp only [filter_eq_empty_iff, mem_piFinset]; rintro f hf rfl; exact hx (hf _)
 
+-- TODO: This proof looks like a good example of something that `aesop` can't do but should
+lemma piFinset_update_eq_filter_piFinset_mem (s : ∀ i, Finset (δ i)) (i : α) {t : Finset (δ i)}
+    (hts : t ⊆ s i) : piFinset (Function.update s i t) = (piFinset s).filter (fun f ↦ f i ∈ t) := by
+  ext f
+  simp only [mem_piFinset, mem_filter]
+  refine ⟨fun h ↦ ?_, fun h j ↦ ?_⟩
+  · have := by simpa using h i
+    refine ⟨fun j ↦ ?_, this⟩
+    obtain rfl | hji := eq_or_ne j i
+    · exact hts this
+    · simpa [hji] using h j
+  · obtain rfl | hji := eq_or_ne j i
+    · simpa using h.2
+    · simpa [hji] using h.1 j
+
+lemma piFinset_update_singleton_eq_filter_piFinset_eq (s : ∀ i, Finset (δ i)) (i : α) {a : δ i}
+    (ha : a ∈ s i) :
+    piFinset (Function.update s i {a}) = (piFinset s).filter (fun f ↦ f i = a) := by
+  simp [piFinset_update_eq_filter_piFinset_mem, ha]
+
 end Fintype
 
 /-! ### pi -/

Mathlib/GroupTheory/PGroup.lean

@@ -187,7 +187,7 @@ theorem card_modEq_card_fixedPoints [Fintype (fixedPoints G α)] :
     calc
       card α = card (Σy : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
         card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
-      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma _
+      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
       _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
       _ = _ := by simp; rfl
     rw [← ZMod.eq_iff_modEq_nat p, Nat.cast_sum, Nat.cast_sum]