[Merged by Bors] - feat(data/multiset): add some lemmas about filter (eq x)

[Ruben-VandeVelde]

---

[eric-wieser]

A slight golf:

Suggested change

	begin
	ext a,
	rw [count_repeat, count_filter],
	simp_rw [eq_comm],
	split_ifs with ha,
	{ subst a },
	{ refl }
	end
	begin
	ext a,
	rw [count_repeat, count_filter],
	simp_rw [eq_comm, ←dif_eq_if],
	congr' 1 with rfl,
	refl,
	end

up to you whether you think it's an improvement.

[eric-wieser]

Can you add a variant for (= b) too? Perhaps:

lemma filter_eq' (s : multiset α) (b : α) : s.filter (= b) = repeat b (count b s) :=
begin
  ext a,
  rw [count_repeat, count_filter],
  simp_rw [←dif_eq_if],
  congr' 1 with rfl,
  refl,
end

lemma filter_eq (s : multiset α) (b : α) : s.filter (eq b) = repeat b (count b s) :=
by { simp_rw [←filter_eq', eq_comm], congr }

which also saves needing eq_comm in both proofs.

[Ruben-VandeVelde]

Thanks for the suggestion, it helped me find an even shorter proof with if_ctx_congr

[eric-wieser]

bors d+

Thanks!

[bors]

✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Ruben-VandeVelde]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests