feat(data/fintype/card): prod_univ_sum (#2284)

* feat(data/fintype/card): prod_univ_sum

* Update src/data/fintype.lean

* Update src/data/fintype/card.lean

* docstrings

* fix build

* remove unused argument

* fix build

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/big_operators.lean

@@ -683,6 +683,8 @@ lemma prod_eq_zero (ha : a ∈ s) (h : f a = 0) : s.prod f = 0 :=
 calc s.prod f = (insert a (erase s a)).prod f : by rw insert_erase ha
   ... = 0 : by rw [prod_insert (not_mem_erase _ _), h, zero_mul]
 
+/-- The product over a sum can be written as a sum over the product of sets, `finset.pi`.
+  `finset.prod_univ_sum` is an alternative statement when the product is over `univ`. -/
 lemma prod_sum {δ : α → Type*} [∀a, decidable_eq (δ a)]
   {s : finset α} {t : Πa, finset (δ a)} {f : Πa, δ a → β} :
   s.prod (λa, (t a).sum (λb, f a b)) =

src/data/finset.lean

@@ -1316,8 +1316,8 @@ theorem card_image_of_injective [decidable_eq β] {f : α → β} (s : finset α
   (H : function.injective f) : card (image f s) = card s :=
 card_image_of_inj_on $ λ x _ y _ h, H h
 
-@[simp] lemma card_map {α β} [decidable_eq β] (f : α ↪ β) {s : finset α} : (s.map f).card = s.card :=
-by rw [map_eq_image, card_image_of_injective]; exact f.2
+@[simp] lemma card_map {α β} (f : α ↪ β) {s : finset α} : (s.map f).card = s.card :=
+multiset.card_map _ _
 
 lemma card_eq_of_bijective [decidable_eq α] {s : finset α} {n : ℕ}
   (f : ∀i, i < n → α)

src/data/fintype/basic.lean

@@ -499,38 +499,27 @@ instance Prop.fintype : fintype Prop :=
 def set_fintype {α} [fintype α] (s : set α) [decidable_pred s] : fintype s :=
 fintype.subtype (univ.filter (∈ s)) (by simp)
 
-
-/-! ### pi -/
-
-/-- A dependent product of fintypes, indexed by a fintype, is a fintype. -/
-instance pi.fintype {α : Type*} {β : α → Type*}
-  [decidable_eq α] [fintype α] [∀a, fintype (β a)] : fintype (Πa, β a) :=
-@fintype.of_equiv _ _
-  ⟨univ.pi $ λa:α, @univ (β a) _,
-    λ f, finset.mem_pi.2 $ λ a ha, mem_univ _⟩
-  ⟨λ f a, f a (mem_univ _), λ f a _, f a, λ f, rfl, λ f, rfl⟩
-
 namespace fintype
 
-variables [fintype α] [decidable_eq α] {δ : α → Type*} [decidable_eq (Π a, δ a)]
+variables [fintype α] [decidable_eq α] {δ : α → Type*}
 
 /-- Given for all `a : α` a finset `t a` of `δ a`, then one can define the
 finset `fintype.pi_finset t` of all functions taking values in `t a` for all `a`. This is the
 analogue of `finset.pi` where the base finset is `univ` (but formally they are not the same, as
 there is an additional condition `i ∈ finset.univ` in the `finset.pi` definition). -/
 def pi_finset (t : Πa, finset (δ a)) : finset (Πa, δ a) :=
-(finset.univ.pi t).image (λ f a, f a (mem_univ a))
+(finset.univ.pi t).map ⟨λ f a, f a (mem_univ a), λ _ _, by simp [function.funext_iff]⟩
 
 @[simp] lemma mem_pi_finset {t : Πa, finset (δ a)} {f : Πa, δ a} :
   f ∈ pi_finset t ↔ (∀a, f a ∈ t a) :=
 begin
   split,
-  { simp only [pi_finset, mem_image, and_imp, forall_prop_of_true, exists_prop, mem_univ,
+  { simp only [pi_finset, mem_map, and_imp, forall_prop_of_true, exists_prop, mem_univ,
                exists_imp_distrib, mem_pi],
     assume g hg hgf a,
     rw ← hgf,
     exact hg a },
-  { simp only [pi_finset, mem_image, forall_prop_of_true, exists_prop, mem_univ, mem_pi],
+  { simp only [pi_finset, mem_map, forall_prop_of_true, exists_prop, mem_univ, mem_pi],
     assume hf,
     exact ⟨λ a ha, f a, hf, rfl⟩ }
 end
@@ -545,12 +534,20 @@ lemma pi_finset_disjoint_of_disjoint [∀ a, decidable_eq (δ a)]
 disjoint_iff_ne.2 $ λ f₁ hf₁ f₂ hf₂ eq₁₂,
 disjoint_iff_ne.1 h (f₁ a) (mem_pi_finset.1 hf₁ a) (f₂ a) (mem_pi_finset.1 hf₂ a) (congr_fun eq₁₂ a)
 
-@[simp] lemma pi_finset_univ [∀ a, fintype (δ a)]:
-  pi_finset (λ a : α, (finset.univ : finset (δ a))) = (finset.univ : finset (Π a, δ a)) :=
-by { ext f, simp }
-
 end fintype
 
+/-! ### pi -/
+
+/-- A dependent product of fintypes, indexed by a fintype, is a fintype. -/
+instance pi.fintype {α : Type*} {β : α → Type*}
+  [decidable_eq α] [fintype α] [∀a, fintype (β a)] : fintype (Πa, β a) :=
+⟨fintype.pi_finset (λ _, univ), by simp⟩
+
+@[simp] lemma fintype.pi_finset_univ {α : Type*} {β : α → Type*}
+  [decidable_eq α] [fintype α] [∀a, fintype (β a)] :
+  fintype.pi_finset (λ a : α, (finset.univ : finset (β a))) = (finset.univ : finset (Π a, β a)) :=
+rfl
+
 instance d_array.fintype {n : ℕ} {α : fin n → Type*}
   [∀n, fintype (α n)] : fintype (d_array n α) :=
 fintype.of_equiv _ (equiv.d_array_equiv_fin _).symm

src/data/fintype/card.lean

@@ -68,13 +68,14 @@ card_sigma _ _
   fintype.card (α ⊕ β) = fintype.card α + fintype.card β :=
 by rw [sum.fintype, fintype.of_equiv_card]; simp
 
+@[simp] lemma fintype.card_pi_finset [decidable_eq α] [fintype α]
+  {δ : α → Type*} (t : Π a, finset (δ a)) :
+  (fintype.pi_finset t).card = finset.univ.prod (λ a, card (t a)) :=
+by simp [fintype.pi_finset, card_map]
+
 @[simp] lemma fintype.card_pi {β : α → Type*} [fintype α] [decidable_eq α]
   [f : Π a, fintype (β a)] : fintype.card (Π a, β a) = univ.prod (λ a, fintype.card (β a)) :=
-by letI f' : fintype (Πa∈univ, β a) :=
-  ⟨(univ.pi $ λa, univ), assume f, finset.mem_pi.2 $ assume a ha, mem_univ _⟩;
-exact calc fintype.card (Π a, β a) = fintype.card (Π a ∈ univ, β a) : fintype.card_congr
-  ⟨λ f a ha, f a, λ f a, f a (mem_univ a), λ _, rfl, λ _, rfl⟩
-... = univ.prod (λ a, fintype.card (β a)) : finset.card_pi _ _
+fintype.card_pi_finset _
 
 -- FIXME ouch, this should be in the main file.
 @[simp] lemma fintype.card_fun [fintype α] [decidable_eq α] [fintype β] :
@@ -104,17 +105,33 @@ begin
     exact ⟨⟨k, hk⟩, mem_univ _, rfl⟩ }
 end
 
-@[simp] lemma fintype.card_pi_finset [decidable_eq α] [fintype α]
-  {δ : α → Type*} [decidable_eq (Π a, δ a)] (t : Π a, finset (δ a)) :
-  (fintype.pi_finset t).card = finset.univ.prod (λ a, card (t a)) :=
-begin
-  dsimp [fintype.pi_finset],
-  rw card_image_of_injective,
-  { simp },
-  { assume f g hfg,
-    ext a ha,
-    exact (congr_fun hfg a : _) }
-end
+/-- Taking a product over `univ.pi t` is the same as taking the product over `fintype.pi_finset t`.
+  `univ.pi t` and `fintype.pi_finset t` are essentially the same `finset`, but differ
+  in the type of their element, `univ.pi t` is a `finset (Π a ∈ univ, t a)` and
+  `fintype.pi_finset t` is a `finset (Π a, t a)`. -/
+@[to_additive "Taking a sum over `univ.pi t` is the same as taking the sum over
+  `fintype.pi_finset t`. `univ.pi t` and `fintype.pi_finset t` are essentially the same `finset`,
+  but differ in the type of their element, `univ.pi t` is a `finset (Π a ∈ univ, t a)` and
+  `fintype.pi_finset t` is a `finset (Π a, t a)`."]
+lemma finset.prod_univ_pi [decidable_eq α] [fintype α] [comm_monoid β]
+  {δ : α → Type*} {t : Π (a : α), finset (δ a)}
+  (f : (Π (a : α), a ∈ (univ : finset α) → δ a) → β) :
+  (univ.pi t).prod f = (fintype.pi_finset t).prod (λ x, f (λ a _, x a)) :=
+prod_bij (λ x _ a, x a (mem_univ _))
+  (by simp)
+  (by simp)
+  (by simp [function.funext_iff] {contextual := tt})
+  (λ x hx, ⟨λ a _, x a, by simp * at *⟩)
+
+/-- The product over `univ` of a sum can be written as a sum over the product of sets,
+  `fintype.pi_finset`. `finset.prod_sum` is an alternative statement when the product is not
+  over `univ` -/
+lemma finset.prod_univ_sum [decidable_eq α] [fintype α] [comm_semiring β] {δ : α → Type u_1}
+  [Π (a : α), decidable_eq (δ a)] {t : Π (a : α), finset (δ a)}
+  {f : Π (a : α), δ a → β} :
+  univ.prod (λ a, (t a).sum (λ b, f a b)) =
+  (fintype.pi_finset t).sum (λ p, univ.prod (λ x, f x (p x))) :=
+by simp only [finset.prod_attach_univ, prod_sum, finset.sum_univ_pi]
 
 /-- Summing `a^s.card * b^(n-s.card)` over all finite subsets `s` of a fintype of cardinality `n`
 gives `(a + b)^n`. The "good" proof involves expanding along all coordinates using the fact that

src/linear_algebra/determinant.lean

@@ -72,18 +72,10 @@ begin
 end
 
 @[simp] lemma det_mul (M N : matrix n n R) : det (M ⬝ N) = det M * det N :=
-calc det (M ⬝ N) = univ.sum (λ σ : perm n, (univ.pi (λ a, univ)).sum
-    (λ (p : Π (a : n), a ∈ univ → n), ε σ *
-    univ.attach.prod (λ i, M (σ i.1) (p i.1 (mem_univ _)) * N (p i.1 (mem_univ _)) i.1))) :
-  by simp only [det, mul_val, prod_sum, mul_sum]
-... = univ.sum (λ σ : perm n, univ.sum
-    (λ p : n → n, ε σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) :
-  sum_congr rfl (λ σ _, sum_bij
-    (λ f h i, f i (mem_univ _)) (λ _ _, mem_univ _)
-    (by simp) (by simp [funext_iff]) (λ b _, ⟨λ i hi, b i, by simp⟩))
-... = univ.sum (λ p : n → n, univ.sum
+calc det (M ⬝ N) = univ.sum (λ p : n → n, univ.sum
     (λ σ : perm n, ε σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) :
-  finset.sum_comm
+  by simp only [det, mul_val, prod_univ_sum, mul_sum,
+    fintype.pi_finset_univ]; rw [finset.sum_comm]
 ... = ((@univ (n → n) _).filter bijective).sum (λ p : n → n, univ.sum
     (λ σ : perm n, ε σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) :
   eq.symm $ sum_subset (filter_subset _)