feat(big_operators/fin): sum over elements of vector equal to a equ…

…als count `a` (#15360)

The sum over `i : fin n` of 1 for vector elements equal to some `a` is just count applied to `a`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/fintype/fin.lean

@@ -18,7 +18,9 @@ open fintype
 
 namespace fin
 
-@[simp] lemma Ioi_zero_eq_map {n : ℕ} :
+variables {α β : Type*} {n : ℕ}
+
+@[simp] lemma Ioi_zero_eq_map :
   Ioi (0 : fin n.succ) = univ.map (fin.succ_embedding _).to_embedding :=
 begin
   ext i,
@@ -31,7 +33,7 @@ begin
     exact succ_pos _ },
 end
 
-@[simp] lemma Ioi_succ {n : ℕ} (i : fin n) :
+@[simp] lemma Ioi_succ (i : fin n) :
   Ioi i.succ = (Ioi i).map (fin.succ_embedding _).to_embedding :=
 begin
   ext i,
@@ -45,4 +47,25 @@ begin
   { rintro ⟨i, hi, rfl⟩, simpa },
 end
 
+lemma card_filter_univ_succ' (p : fin (n + 1) → Prop) [decidable_pred p] :
+  (univ.filter p).card = (ite (p 0) 1 0) + (univ.filter (p ∘ fin.succ)).card :=
+begin
+  rw [fin.univ_succ, filter_cons, card_disj_union, map_filter, card_map],
+  split_ifs; simp,
+end
+
+lemma card_filter_univ_succ (p : fin (n + 1) → Prop) [decidable_pred p] :
+  (univ.filter p).card =
+    if p 0 then (univ.filter (p ∘ fin.succ)).card + 1 else (univ.filter (p ∘ fin.succ)).card :=
+(card_filter_univ_succ' p).trans (by split_ifs; simp [add_comm 1])
+
+lemma card_filter_univ_eq_vector_nth_eq_count [decidable_eq α] (a : α) (v : vector α n) :
+  (univ.filter $ λ i, a = v.nth i).card = v.to_list.count a :=
+begin
+  induction v using vector.induction_on with n x xs hxs,
+  { simp },
+  { simp_rw [card_filter_univ_succ', vector.nth_cons_zero, vector.to_list_cons,
+      function.comp, vector.nth_cons_succ, hxs, list.count_cons', add_comm (ite (a = x) 1 0)] }
+end
+
 end fin