chore(data/fin,data/finset): a few lemmas (#7168)

* `fin.heq_fun_iff`: use `Sort*` instead of `Type*`;
* `fin.cast_refl`: take `h : n = n := rfl` as an argument;
* `fin.cast_to_equiv`, `fin.cast_eq_cast`: relate `fin.cast` to `_root_.cast`;
* `finset.map_cast_heq`: new lemma;
* `finset.subset_univ`: add `@[simp]`;
* `card_finset_fin_le`, `fintype.card_finset_len`, `fin.prod_const` : new lemmas;
* `order_iso.refl`: new definition.

src/data/fin.lean

@@ -139,7 +139,7 @@ lemma coe_eq_val (a : fin n) : (a : ℕ) = a.val := rfl
 
 /-- Assume `k = l`. If two functions defined on `fin k` and `fin l` are equal on each element,
 then they coincide (in the heq sense). -/
-protected lemma heq_fun_iff {α : Type*} {k l : ℕ} (h : k = l) {f : fin k → α} {g : fin l → α} :
+protected lemma heq_fun_iff {α : Sort*} {k l : ℕ} (h : k = l) {f : fin k → α} {g : fin l → α} :
   f == g ↔ (∀ (i : fin k), f i = g ⟨(i : ℕ), h ▸ i.2⟩) :=
 by { induction h, simp [heq_iff_eq, function.funext_iff] }
 
@@ -571,9 +571,19 @@ lemma coe_cast (h : n = m) (i : fin n) : (cast h i : ℕ) = i := rfl
 @[simp] lemma cast_trans {k : ℕ} (h : n = m) (h' : m = k) {i : fin n} :
   cast h' (cast h i) = cast (eq.trans h h') i := rfl
 
-@[simp] lemma cast_refl {i : fin n} : cast rfl i = i :=
+@[simp] lemma cast_refl (h : n = n := rfl) : cast h = order_iso.refl (fin n) :=
 by { ext, refl }
 
+/-- While in many cases `fin.cast` is better than `equiv.cast`/`cast`, sometimes we want to apply
+a generic theorem about `cast`. -/
+lemma cast_to_equiv (h : n = m) : (cast h).to_equiv = equiv.cast (h ▸ rfl) :=
+by { subst h, simp }
+
+/-- While in many cases `fin.cast` is better than `equiv.cast`/`cast`, sometimes we want to apply
+a generic theorem about `cast`. -/
+lemma cast_eq_cast (h : n = m) : (cast h : fin n → fin m) = _root_.cast (h ▸ rfl) :=
+by { subst h, ext, simp }
+
 /-- `cast_add m i` embeds `i : fin n` in `fin (n+m)`. -/
 def cast_add (m) : fin n ↪o fin (n + m) := cast_le $ le_add_right n m
 

src/data/finset/basic.lean

@@ -1667,11 +1667,11 @@ mem_map_of_injective f.2
 theorem mem_map_of_mem (f : α ↪ β) {a} {s : finset α} : a ∈ s → f a ∈ s.map f :=
 (mem_map' _).2
 
-@[simp, norm_cast] theorem coe_map (f : α ↪ β) (s : finset α) : (↑(s.map f) : set β) = f '' ↑s :=
+@[simp, norm_cast] theorem coe_map (f : α ↪ β) (s : finset α) : (s.map f : set β) = f '' s :=
 set.ext $ λ x, mem_map.trans set.mem_image_iff_bex.symm
 
-theorem coe_map_subset_range (f : α ↪ β) (s : finset α) : (↑(s.map f) : set β) ⊆ set.range f :=
-calc ↑(s.map f) = f '' ↑s     : coe_map f s
+theorem coe_map_subset_range (f : α ↪ β) (s : finset α) : (s.map f : set β) ⊆ set.range f :=
+calc ↑(s.map f) = f '' s      : coe_map f s
             ... ⊆ set.range f : set.image_subset_range f ↑s
 
 theorem map_to_finset [decidable_eq α] [decidable_eq β] {s : multiset α} :
@@ -1681,6 +1681,10 @@ ext $ λ _, by simp only [mem_map, multiset.mem_map, exists_prop, multiset.mem_t
 @[simp] theorem map_refl : s.map (embedding.refl _) = s :=
 ext $ λ _, by simpa only [mem_map, exists_prop] using exists_eq_right
 
+@[simp] theorem map_cast_heq {α β} (h : α = β) (s : finset α) :
+  s.map (equiv.cast h).to_embedding == s :=
+by { subst h, simp }
+
 theorem map_map {g : β ↪ γ} : (s.map f).map g = s.map (f.trans g) :=
 eq_of_veq $ by simp only [map_val, multiset.map_map]; refl
 

src/data/fintype/basic.lean

@@ -51,7 +51,7 @@ univ_nonempty_iff.2 ‹_›
 lemma univ_eq_empty : (univ : finset α) = ∅ ↔ ¬nonempty α :=
 by rw [← univ_nonempty_iff, nonempty_iff_ne_empty, ne.def, not_not]
 
-theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
+@[simp] theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
 
 instance : order_top (finset α) :=
 { top := univ,
@@ -498,6 +498,9 @@ list.length_fin_range n
 @[simp] lemma finset.card_fin (n : ℕ) : finset.card (finset.univ : finset (fin n)) = n :=
 by rw [finset.card_univ, fintype.card_fin]
 
+lemma card_finset_fin_le {n : ℕ} (s : finset (fin n)) : s.card ≤ n :=
+by simpa only [fintype.card_fin] using s.card_le_univ
+
 lemma fin.equiv_iff_eq {m n : ℕ} : nonempty (fin m ≃ fin n) ↔ m = n :=
   ⟨λ ⟨h⟩, by simpa using fintype.card_congr h, λ h, ⟨equiv.cast $ h ▸ rfl ⟩ ⟩
 
@@ -986,6 +989,14 @@ instance finset.fintype [fintype α] : fintype (finset α) :=
   fintype.card (finset α) = 2 ^ (fintype.card α) :=
 finset.card_powerset finset.univ
 
+@[simp] lemma finset.univ_filter_card_eq (α : Type*) [fintype α] (k : ℕ) :
+  (finset.univ : finset (finset α)).filter (λ s, s.card = k) = finset.univ.powerset_len k :=
+by { ext, simp [finset.mem_powerset_len] }
+
+@[simp] lemma fintype.card_finset_len [fintype α] (k : ℕ) :
+  fintype.card {s : finset α // s.card = k} = nat.choose (fintype.card α) k :=
+by simp [fintype.subtype_card, finset.card_univ]
+
 @[simp] lemma set.to_finset_univ [fintype α] :
   (set.univ : set α).to_finset = finset.univ :=
 by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }

src/data/fintype/card.lean

@@ -241,10 +241,13 @@ lemma fintype.sum_pow_mul_eq_add_pow
 finset.sum_pow_mul_eq_add_pow _ _ _
 
 lemma fin.sum_pow_mul_eq_add_pow {n : ℕ} {R : Type*} [comm_semiring R] (a b : R) :
-  ∑ s : finset (fin n), a ^ s.card * b ^ (n - s.card) =
-  (a + b) ^ n :=
+  ∑ s : finset (fin n), a ^ s.card * b ^ (n - s.card) = (a + b) ^ n :=
 by simpa using fintype.sum_pow_mul_eq_add_pow (fin n) a b
 
+lemma fin.prod_const [comm_monoid α] (n : ℕ) (x : α) : ∏ i : fin n, x = x ^ n := by simp
+
+lemma fin.sum_const [add_comm_monoid α] (n : ℕ) (x : α) : ∑ i : fin n, x = n • x := by simp
+
 @[to_additive]
 lemma function.bijective.prod_comp [fintype α] [fintype β] [comm_monoid γ] {f : α → β}
   (hf : function.bijective f) (g : β → γ) :

src/linear_algebra/multilinear.lean

@@ -338,7 +338,7 @@ begin
       simp only [finset.sum_congr rfl this, finset.mem_univ, finset.sum_const, Ai_card i,
                  one_nsmul] },
     simp only [sum_congr rfl this, Ai_card, card_pi_finset, prod_const_one, one_nsmul,
-               sum_const] },
+               finset.sum_const] },
   -- Remains the interesting case where one of the `A i`, say `A i₀`, has cardinality at least 2.
   -- We will split into two parts `B i₀` and `C i₀` of smaller cardinality, let `B i = C i = A i`
   -- for `i ≠ i₀`, apply the inductive assumption to `B` and `C`, and add up the corresponding

src/order/rel_iso.lean

@@ -516,6 +516,15 @@ protected lemma surjective (e : α ≃o β) : surjective e := e.to_equiv.surject
 @[simp] lemma apply_eq_iff_eq (e : α ≃o β) {x y : α} : e x = e y ↔ x = y :=
 e.to_equiv.apply_eq_iff_eq
 
+/-- Identity order isomorphism. -/
+def refl (α : Type*) [has_le α] : α ≃o α := rel_iso.refl (≤)
+
+@[simp] lemma coe_refl : ⇑(refl α) = id := rfl
+
+lemma refl_apply (x : α) : refl α x = x := rfl
+
+@[simp] lemma refl_to_equiv : (refl α).to_equiv = equiv.refl α := rfl
+
 /-- Inverse of an order isomorphism. -/
 def symm (e : α ≃o β) : β ≃o α := e.symm
 
@@ -525,6 +534,8 @@ e.to_equiv.apply_symm_apply x
 @[simp] lemma symm_apply_apply (e : α ≃o β) (x : α) : e.symm (e x) = x :=
 e.to_equiv.symm_apply_apply x
 
+@[simp] lemma symm_refl (α : Type*) [has_le α] : (refl α).symm = refl α := rfl
+
 lemma apply_eq_iff_eq_symm_apply (e : α ≃o β) (x : α) (y : β) : e x = y ↔ x = e.symm y :=
 e.to_equiv.apply_eq_iff_eq_symm_apply
 
@@ -545,6 +556,10 @@ lemma symm_injective : injective (symm : (α ≃o β) → (β ≃o α)) :=
 
 lemma trans_apply (e : α ≃o β) (e' : β ≃o γ) (x : α) : e.trans e' x = e' (e x) := rfl
 
+@[simp] lemma refl_trans (e : α ≃o β) : (refl α).trans e = e := by { ext x, refl }
+
+@[simp] lemma trans_refl (e : α ≃o β) : e.trans (refl β) = e := by { ext x, refl }
+
 end has_le
 
 open set