chore(data/fintype/card): review API (#4287)

API changes:

* `finset.filter_mem_eq_inter` now takes `[Π i, decidable (i ∈ t)]`; this way it works better
  with `classical`;
* add `finset.mem_compl` and `finset.coe_compl`;
* [DRY] drop `finset.prod_range_eq_prod_fin` and `finset.sum_range_eq_sum_fin`:
  use `fin.prod_univ_eq_prod_range` and `fin.sum_univ_eq_sum_range` instead;
* rename `finset.prod_equiv` to `equiv.prod_comp` to enable dot notation;
* add `fintype.prod_dite`: a specialized version of `finset.prod_dite`.

Also golf a proof in `analysis/normed_space/multilinear`

Author: urkud

src/analysis/analytic/composition.lean

@@ -168,7 +168,7 @@ calc ∥q.comp_along_composition_multilinear p c v∥ = ∥q c.length (p.apply_c
         ∏ i (j : fin (c.blocks_fun i)), ∥(v ∘ (c.embedding i)) j∥ :
   by rw [finset.prod_mul_distrib, mul_assoc]
 ... = ∥q c.length∥ * (∏ i, ∥p (c.blocks_fun i)∥) * (∏ i : fin n, ∥v i∥) :
-  by { rw [← finset.prod_equiv c.blocks_fin_equiv, ← finset.univ_sigma_univ, finset.prod_sigma],
+  by { rw [← c.blocks_fin_equiv.prod_comp, ← finset.univ_sigma_univ, finset.prod_sigma],
        congr }
 
 /-- Given two formal multilinear series `q` and `p` and a composition `c` of `n`, one may
@@ -1073,7 +1073,7 @@ begin
     exact A },
   /- Now, we use `composition.sigma_equiv_sigma_pi n` to change
   variables in the second sum, and check that we get exactly the same sums. -/
-  rw ← finset.sum_equiv (sigma_equiv_sigma_pi n),
+  rw ← (sigma_equiv_sigma_pi n).sum_comp,
   /- To check that we have the same terms, we should check that we apply the same component of
   `r`, and the same component of `q`, and the same component of `p`, to the same coordinate of
   `v`. This is true by definition, but at each step one needs to convince Lean that the types

src/analysis/normed_space/multilinear.lean

@@ -252,32 +252,14 @@ lemma restr_norm_le {k n : ℕ} (f : (multilinear_map 𝕜 (λ i : fin n, G) E
   (s : finset (fin n)) (hk : s.card = k) (z : G) {C : ℝ}
   (H : ∀ m, ∥f m∥ ≤ C * ∏ i, ∥m i∥) (v : fin k → G) :
   ∥f.restr s hk z v∥ ≤ C * ∥z∥ ^ (n - k) * ∏ i, ∥v i∥ :=
-calc ∥f.restr s hk z v∥
-≤ C * ∏ j, ∥(if h : j ∈ s then v ((s.mono_equiv_of_fin hk).symm ⟨j, h⟩) else z)∥ : H _
-... = C * ((∏ j in finset.univ \ s,
-        ∥(if h : j ∈ s then v ((s.mono_equiv_of_fin hk).symm ⟨j, h⟩) else z)∥)
-      * (∏ j in s,
-        ∥(if h : j ∈ s then v ((s.mono_equiv_of_fin hk).symm ⟨j, h⟩) else z)∥)) :
-  by rw ← finset.prod_sdiff (finset.subset_univ _)
-... = C * (∥z∥ ^ (n - k) * ∏ i, ∥v i∥) :
-  begin
-    congr' 2,
-    { have : ∥z∥ ^ (n - k) = ∏ j in finset.univ \ s, ∥z∥,
-        by simp [finset.card_sdiff  (finset.subset_univ _), hk],
-      rw this,
-      exact finset.prod_congr rfl (λ i hi, by rw dif_neg (finset.mem_sdiff.1 hi).2) },
-    { apply finset.prod_bij (λ (i : fin n) (hi : i ∈ s), (s.mono_equiv_of_fin hk).symm ⟨i, hi⟩),
-      { exact λ _ _, finset.mem_univ _ },
-      { exact λ i hi, by simp [hi] },
-      { exact λ i j hi hi hij, subtype.mk.inj ((s.mono_equiv_of_fin hk).symm.injective hij) },
-      { assume i hi,
-        rcases (s.mono_equiv_of_fin hk).symm.surjective i with ⟨j, hj⟩,
-        refine ⟨j.1, j.2, _⟩,
-        unfold_coes,
-        convert hj.symm,
-        rw subtype.ext_iff_val } }
-  end
-... = C * ∥z∥ ^ (n - k) * ∏ i, ∥v i∥ : by rw mul_assoc
+begin
+  rw mul_assoc,
+  convert H _ using 2,
+  simp only [apply_dite norm, fintype.prod_dite, prod_const (∥z∥), finset.card_univ,
+    fintype.card_of_subtype sᶜ (λ x, mem_compl), card_compl, fintype.card_fin, hk, mk_coe,
+    (s.mono_equiv_of_fin hk).symm.prod_comp (λ x, ∥v x∥)],
+  apply mul_comm
+end
 
 end multilinear_map
 

src/data/finset/basic.lean

@@ -965,7 +965,8 @@ theorem filter_union_right (p q : α → Prop) [decidable_pred p] [decidable_pre
   s.filter p ∪ s.filter q = s.filter (λx, p x ∨ q x) :=
 ext $ λ x, by simp only [mem_filter, mem_union, and_or_distrib_left.symm]
 
-lemma filter_mem_eq_inter {s t : finset α} : s.filter (λ i, i ∈ t) = s ∩ t :=
+lemma filter_mem_eq_inter {s t : finset α} [Π i, decidable (i ∈ t)] :
+  s.filter (λ i, i ∈ t) = s ∩ t :=
 ext $ λ i, by rw [mem_filter, mem_inter]
 
 theorem filter_inter {s t : finset α} : filter p s ∩ t = filter p (s ∩ t) :=

src/data/fintype/basic.lean

@@ -57,6 +57,12 @@ instance [decidable_eq α] : boolean_algebra (finset α) :=
 
 lemma compl_eq_univ_sdiff [decidable_eq α] (s : finset α) : sᶜ = univ \ s := rfl
 
+@[simp] lemma mem_compl [decidable_eq α] {s : finset α} {x : α} : x ∈ sᶜ ↔ x ∉ s :=
+by simp [compl_eq_univ_sdiff]
+
+@[simp, norm_cast] lemma coe_compl [decidable_eq α] (s : finset α) : ↑(sᶜ) = (↑s : set α)ᶜ :=
+set.ext $ λ x, mem_compl
+
 theorem eq_univ_iff_forall {s : finset α} : s = univ ↔ ∀ x, x ∈ s :=
 by simp [ext_iff]
 
@@ -179,7 +185,7 @@ multiset.card_pmap _ _ _
 theorem card_of_subtype {p : α → Prop} (s : finset α)
   (H : ∀ x : α, x ∈ s ↔ p x) [fintype {x // p x}] :
   card {x // p x} = s.card :=
-by rw ← subtype_card s H; congr
+by { rw ← subtype_card s H, congr }
 
 /-- Construct a fintype from a finset with the same elements. -/
 def of_finset {p : set α} (s : finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : fintype p :=

src/data/fintype/card.lean

@@ -157,34 +157,11 @@ by rw [fintype.card_pi, finset.prod_const]; refl
   fintype.card (vector α n) = fintype.card α ^ n :=
 by rw fintype.of_equiv_card; simp
 
-
 @[simp, to_additive]
 lemma finset.prod_attach_univ [fintype α] [comm_monoid β] (f : {a : α // a ∈ @univ α _} → β) :
   ∏ x in univ.attach, f x = ∏ x, f ⟨x, (mem_univ _)⟩ :=
 prod_bij (λ x _, x.1) (λ _ _, mem_univ _) (λ _ _ , by simp) (by simp) (λ b _, ⟨⟨b, mem_univ _⟩, by simp⟩)
 
-@[to_additive]
-lemma finset.prod_range_eq_prod_fin [comm_monoid β] (n : ℕ) (f : ℕ → β) :
-  ∏ k in range n, f k = ∏ k : fin n, f k :=
-begin
-  symmetry,
-  refine prod_bij (λ k hk, k) _ _ _ _,
-  { rintro ⟨k, hk⟩ _, simp * },
-  { rintro ⟨k, hk⟩ _, simp * },
-  { intros, rwa fin.eq_iff_veq },
-  { intros k hk, rw mem_range at hk,
-    exact ⟨⟨k, hk⟩, mem_univ _, rfl⟩ }
-end
-
-@[to_additive]
-lemma finset.prod_fin_eq_prod_range [comm_monoid β] {n : ℕ} (c : fin n → β) :
-  ∏ i, c i = ∏ i in finset.range n, if h : i < n then c ⟨i, h⟩ else 1 :=
-begin
-  rw [finset.prod_range_eq_prod_fin, finset.prod_congr rfl],
-  rintros ⟨i, hi⟩ _,
-  simp only [fin.coe_eq_val, hi, dif_pos]
-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
@@ -227,20 +204,8 @@ lemma fin.sum_pow_mul_eq_add_pow {n : ℕ} {R : Type*} [comm_semiring R] (a b :
   (a + b) ^ n :=
 by simpa using fintype.sum_pow_mul_eq_add_pow (fin n) a b
 
-/-- It is equivalent to sum a function over `fin n` or `finset.range n`. -/
 @[to_additive]
-lemma fin.prod_univ_eq_prod_range [comm_monoid α] (f : ℕ → α) (n : ℕ) :
-  ∏ i : fin n, f i.val = ∏ i in finset.range n, f i :=
-begin
-  apply finset.prod_bij (λ (a : fin n) ha, a.val),
-  { assume a ha, simp [a.is_lt] },
-  { assume a ha, refl },
-  { assume a b ha hb H, exact (fin.ext_iff _ _).2 H },
-  { assume b hb, exact ⟨⟨b, list.mem_range.mp hb⟩, finset.mem_univ _, rfl⟩, }
-end
-
-@[to_additive]
-lemma finset.prod_equiv [fintype α] [fintype β] [comm_monoid γ] (e : α ≃ β) (f : β → γ) :
+lemma equiv.prod_comp [fintype α] [fintype β] [comm_monoid γ] (e : α ≃ β) (f : β → γ) :
   ∏ i, f (e i) = ∏ i, f i :=
 begin
   apply prod_bij (λ i hi, e i) (λ i hi, mem_univ _) _ (λ a b _ _ h, e.injective h),
@@ -250,16 +215,33 @@ begin
   { simp }
 end
 
+/-- It is equivalent to sum a function over `fin n` or `finset.range n`. -/
+@[to_additive]
+lemma fin.prod_univ_eq_prod_range [comm_monoid α] (f : ℕ → α) (n : ℕ) :
+  ∏ i : fin n, f i = ∏ i in range n, f i :=
+calc (∏ i : fin n, f i) = ∏ i : {x // x ∈ range n}, f i :
+  ((equiv.fin_equiv_subtype n).trans
+    (equiv.subtype_congr_right (λ _, mem_range.symm))).prod_comp (f ∘ coe)
+... = ∏ i in range n, f i : by rw [← attach_eq_univ, prod_attach]
+
+@[to_additive]
+lemma finset.prod_fin_eq_prod_range [comm_monoid β] {n : ℕ} (c : fin n → β) :
+  ∏ i, c i = ∏ i in finset.range n, if h : i < n then c ⟨i, h⟩ else 1 :=
+begin
+  rw [← fin.prod_univ_eq_prod_range, finset.prod_congr rfl],
+  rintros ⟨i, hi⟩ _,
+  simp only [fin.coe_eq_val, hi, dif_pos]
+end
+
 @[to_additive]
 lemma finset.prod_subtype {M : Type*} [comm_monoid M]
   {p : α → Prop} {F : fintype (subtype p)} {s : finset α} (h : ∀ x, x ∈ s ↔ p x) (f : α → M) :
   ∏ a in s, f a = ∏ a : subtype p, f a :=
 have (∈ s) = p, from set.ext h,
 begin
-  rw ← prod_attach,
+  rw [← prod_attach, attach_eq_univ],
   substI p,
-  congr,
-  simp [finset.ext_iff]
+  congr
 end
 
 @[to_additive] lemma finset.prod_fiberwise [decidable_eq β] [fintype β] [comm_monoid γ]
@@ -284,10 +266,22 @@ lemma fintype.prod_fiberwise [fintype α] [decidable_eq β] [fintype β] [comm_m
   (f : α → β) (g : α → γ) :
   (∏ b : β, ∏ a : {a // f a = b}, g (a : α)) = ∏ a, g a :=
 begin
-  rw [← finset.prod_equiv (equiv.sigma_preimage_equiv f) _, ← univ_sigma_univ, prod_sigma],
+  rw [← (equiv.sigma_preimage_equiv f).prod_comp, ← univ_sigma_univ, prod_sigma],
   refl
 end
 
+lemma fintype.prod_dite [fintype α] {p : α → Prop} [decidable_pred p]
+  [comm_monoid β] (f : Π (a : α) (ha : p a), β) (g : Π (a : α) (ha : ¬p a), β) :
+  (∏ a, dite (p a) (f a) (g a)) = (∏ a : {a // p a}, f a a.2) * (∏ a : {a // ¬p a}, g a a.2) :=
+begin
+  simp only [prod_dite, attach_eq_univ],
+  congr' 1,
+  { convert (equiv.subtype_congr_right _).prod_comp (λ x : {x // p x}, f x x.2),
+    simp },
+  { convert (equiv.subtype_congr_right _).prod_comp (λ x : {x // ¬p x}, g x x.2),
+    simp }
+end
+
 section
 open finset
 

src/field_theory/chevalley_warning.lean

@@ -66,7 +66,7 @@ begin
   intros x₀,
   let e : K ≃ {x // x ∘ coe = x₀} := (equiv.subtype_equiv_codomain _).symm,
   calc (∑ x : {x : σ → K // x ∘ coe = x₀}, ∏ j, (x : σ → K) j ^ d j)
-        = ∑ a : K, ∏ j : σ, (e a : σ → K) j ^ d j : (finset.sum_equiv e _).symm
+        = ∑ a : K, ∏ j : σ, (e a : σ → K) j ^ d j : (e.sum_comp _).symm
     ... = ∑ a : K, (∏ j, x₀ j ^ d j) * a ^ d i    : fintype.sum_congr _ _ _
     ... = (∏ j, x₀ j ^ d j) * ∑ a : K, a ^ d i    : by rw mul_sum
     ... = 0                                       : by rw [sum_pow_lt_card_sub_one _ hi, mul_zero],
@@ -76,7 +76,7 @@ begin
   { default := ⟨i, rfl⟩, uniq := λ ⟨j, h⟩, subtype.val_injective h },
   calc (∏ j : σ, (e a : σ → K) j ^ d j)
         = (e a : σ → K) i ^ d i * (∏ (j : {j // j ≠ i}), (e a : σ → K) j ^ d j) :
-        by { rw [← finset.prod_equiv e', fintype.prod_sum_type, univ_unique, prod_singleton], refl }
+        by { rw [← e'.prod_comp, fintype.prod_sum_type, univ_unique, prod_singleton], refl }
     ... = a ^ d i * (∏ (j : {j // j ≠ i}), (e a : σ → K) j ^ d j) : by rw equiv.subtype_equiv_codomain_symm_apply_eq
     ... = a ^ d i * (∏ j, x₀ j ^ d j) : congr_arg _ (fintype.prod_congr _ _ _) -- see below
     ... = (∏ j, x₀ j ^ d j) * a ^ d i : mul_comm _ _,

src/linear_algebra/determinant.lean

@@ -89,7 +89,7 @@ calc det (M ⬝ N) = ∑ p : n → n, ∑ σ : perm n, ε σ * ∏ i, (M (σ i)
   sum_congr rfl (λ σ _, sum_bij (λ τ _, τ * σ⁻¹) (λ _ _, mem_univ _)
     (λ τ _,
       have ∏ j, M (τ j) (σ j) = ∏ j, M ((τ * σ⁻¹) j) j,
-        by rw ← finset.prod_equiv σ⁻¹; simp [mul_apply],
+        by rw ← σ⁻¹.prod_comp; simp [mul_apply],
       have h : ε σ * ε (τ * σ⁻¹) = ε τ :=
         calc ε σ * ε (τ * σ⁻¹) = ε ((τ * σ⁻¹) * σ) :
           by rw [mul_comm, sign_mul (τ * σ⁻¹)]; simp [sign_mul]

src/linear_algebra/matrix.lean

@@ -101,7 +101,7 @@ theorem to_lin_of_equiv {p q : Type*} [fintype p] [fintype q] (e₁ : m ≃ p) (
 linear_map.ext $ λ v, funext $ λ i,
 calc  ∑ j : n, f (e₁ i) (e₂ j) * v j
     = ∑ j : n, f (e₁ i) (e₂ j) * v (e₂.symm (e₂ j)) : by simp_rw e₂.symm_apply_apply
-... = ∑ k : q, f (e₁ i) k * v (e₂.symm k) : finset.sum_equiv e₂ (λ k, f (e₁ i) k * v (e₂.symm k))
+... = ∑ k : q, f (e₁ i) k * v (e₂.symm k) : e₂.sum_comp (λ k, f (e₁ i) k * v (e₂.symm k))
 
 lemma to_lin_add (M N : matrix m n R) : (M + N).to_lin = M.to_lin + N.to_lin :=
 matrix.eval.map_add M N
@@ -266,9 +266,9 @@ begin
   refine function.left_inverse.injective linear_equiv.symm_symm _; ext x;
   simp_rw [linear_equiv.symm_trans_apply, is_basis.equiv_fun_symm_apply, fun_congr_left_symm,
     fun_congr_left_apply, fun_left_apply],
-  convert (finset.sum_equiv (equiv.of_injective _ hv₁.injective) _).symm,
+  convert ((equiv.of_injective _ hv₁.injective).sum_comp _).symm,
   simp_rw [equiv.symm_apply_apply, equiv.of_injective_apply, subtype.coe_mk],
-  convert (finset.sum_equiv (equiv.of_injective _ hv₂.injective) _).symm,
+  convert ((equiv.of_injective _ hv₂.injective).sum_comp _).symm,
   simp_rw [equiv.symm_apply_apply, equiv.of_injective_apply, subtype.coe_mk]
 end
 
@@ -752,7 +752,7 @@ linear_map.ext $ λ f, if H : 0 = 1 then eq_of_zero_eq_one H _ _ else
 begin
   haveI : nontrivial R := ⟨⟨0, 1, H⟩⟩,
   change ∑ i : set.range b, _ = ∑ i : ι, _, simp_rw [matrix.diag_apply], symmetry,
-  convert finset.sum_equiv (equiv.of_injective _ hb.injective) _, ext i,
+  convert (equiv.of_injective _ hb.injective).sum_comp _, ext i,
   exact (linear_equiv_matrix_range hb hb f i i).symm
 end
 

src/number_theory/bernoulli.lean

@@ -38,7 +38,7 @@ well_founded.fix_eq _ _ _
 
 lemma bernoulli_def (n : ℕ) :
   bernoulli n = 1 - ∑ k in finset.range n, (n.choose k) * (bernoulli k) / (n + 1 - k) :=
-by { rw [bernoulli_def', finset.sum_range_eq_sum_fin], refl }
+by { rw [bernoulli_def', ← fin.sum_univ_eq_sum_range], refl }
 
 @[simp] lemma bernoulli_zero  : bernoulli 0 = 1   := rfl
 @[simp] lemma bernoulli_one   : bernoulli 1 = 1/2 :=

src/number_theory/sum_four_squares.lean

@@ -94,7 +94,7 @@ let ⟨x, hx⟩ := h01 in let ⟨y, hy⟩ := h23 in
       ← int.sum_two_squares_of_two_mul_sum_two_squares hy.symm,
       ← mul_right_inj' (show (2 : ℤ) ≠ 0, from dec_trivial), ← h, mul_add, ← hx, ← hy],
     have : ∑ x, f (σ x)^2 = ∑ x, f x^2,
-    { conv_rhs { rw ← finset.sum_equiv σ } },
+    { conv_rhs { rw ← σ.sum_comp } },
     have fin4univ : (univ : finset (fin 4)).1 = 0::1::2::3::0, from dec_trivial,
     simpa [finset.sum_eq_multiset_sum, fin4univ, multiset.sum_cons, f, add_assoc]
   end⟩