# HG changeset patch
# User desharna
# Date 1741090247 -3600
# Node ID 91c00d8f1bdd21b37a360c23b6c874b6eec68038
# Parent  eee83daed0d7242fc256dc120c165409b4bdee8f
added lemma sum_mset_image_mset_mono_strong

diff -r eee83daed0d7 -r 91c00d8f1bdd src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Mar 04 13:10:31 2025 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Mar 04 13:10:47 2025 +0100
@@ -2844,6 +2844,29 @@
 lemma size_multiset_sum_mset [simp]: "size (\<Sum>X\<in>#A. X :: 'a multiset) = (\<Sum>X\<in>#A. size X)"
   by (induction A) auto
 
+lemma sum_mset_image_mset_mono_strong:
+  assumes "A \<subseteq># B" and f_subeq_g: "\<And>x. x \<in># A \<Longrightarrow> f x \<subseteq># g x"
+  shows "(\<Sum>x\<in>#A. f x) \<subseteq># (\<Sum>x\<in>#B. g x)"
+proof -
+  define B' where
+    "B' = B - A"
+
+  have "B = A + B'"
+    using B'_def assms(1) by fastforce
+
+  have "\<Sum>\<^sub># (image_mset f A) \<subseteq># \<Sum>\<^sub># (image_mset g A)"
+    using f_subeq_g by (induction A) (auto intro!: subset_mset.add_mono)
+  also have "\<dots> \<subseteq># \<Sum>\<^sub># (image_mset g A) + \<Sum>\<^sub># (image_mset g B')"
+    by simp
+  also have "\<dots> = \<Sum>\<^sub># (image_mset g A + image_mset g B')"
+    by simp
+  also have "\<dots> = \<Sum>\<^sub># (image_mset g (A + B'))"
+    by simp
+  also have "\<dots> = \<Sum>\<^sub># (image_mset g B)"
+    unfolding \<open>B = A + B'\<close> ..
+  finally show ?thesis .
+qed
+
 context comm_monoid_mult
 begin