added lemma image_mset_filter_mset_swap

--- a/src/HOL/Library/Multiset.thy	Mon May 23 10:12:19 2022 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon May 23 10:13:08 2022 +0200
@@ -1815,6 +1815,10 @@
   "{#c. a \<in># M#} = replicate_mset (size M) c"
   by (induct M) simp_all
 
+lemma image_mset_filter_mset_swap:
+  "image_mset f (filter_mset (\<lambda>x. P (f x)) M) = filter_mset P (image_mset f M)"
+  by (induction M rule: multiset_induct) simp_all
+
 
 subsection \<open>Further conversions\<close>