feat(data/multiset): add some lemmas about filter (eq x) (#10626)

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

src/data/multiset/basic.lean

@@ -2109,6 +2109,14 @@ quot.induction_on s $ λ l, count_filter h
   {a} {s : multiset α} (h : ¬ p a) : count a (filter p s) = 0 :=
 multiset.count_eq_zero_of_not_mem (λ t, h (of_mem_filter t))
 
+theorem count_filter {p} [decidable_pred p] {a} {s : multiset α} :
+  count a (filter p s) = if p a then count a s else 0 :=
+begin
+  split_ifs with h,
+  { exact count_filter_of_pos h },
+  { exact count_filter_of_neg h },
+end
+
 theorem ext {s t : multiset α} : s = t ↔ ∀ a, count a s = count a t :=
 quotient.induction_on₂ s t $ λ l₁ l₂, quotient.eq.trans perm_iff_count
 
@@ -2152,6 +2160,20 @@ begin
     simp only [count_repeat, eq_self_iff_true, if_true, card_repeat]},
 end
 
+lemma filter_eq' (s : multiset α) (b : α) : s.filter (= b) = repeat b (count b s) :=
+begin
+  ext a,
+  rw [count_repeat, count_filter],
+  exact if_ctx_congr iff.rfl (λ h, congr_arg _ h) (λ h, rfl),
+end
+
+lemma filter_eq (s : multiset α) (b : α) : s.filter (eq b) = repeat b (count b s) :=
+by { simp_rw [←filter_eq', eq_comm], congr }
+
+lemma pow_count [comm_monoid α] {s : multiset α} (a : α) :
+  a ^ (count a s) = (filter (eq a) s).prod :=
+by rw [filter_eq, prod_repeat]
+
 end
 
 /-! ### Lift a relation to `multiset`s -/