# HG changeset patch
# User desharna
# Date 1741102701 -3600
# Node ID 1b7dc0728f5c0c96e2fe11cc06452ce31edc13ae
# Parent  c8ed5e759d2210a7b1c9817b41bf1a7bc42122a7
removed lemma size_multiset_sum_mset[simp]

diff -r c8ed5e759d22 -r 1b7dc0728f5c NEWS
--- a/NEWS	Tue Mar 04 16:37:14 2025 +0100
+++ b/NEWS	Tue Mar 04 16:38:21 2025 +0100
@@ -17,6 +17,8 @@
 * Theory "HOL-Library.Multiset":
   - Renamed lemmas. Minor INCOMPATIBILITY.
       filter_image_mset ~> filter_mset_image_mset
+  - Removed lemmas.
+      size_multiset_sum_mset[simp]
   - Added lemmas.
       filter_mset_eq_mempty_iff
       filter_mset_mono_strong
diff -r c8ed5e759d22 -r 1b7dc0728f5c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Mar 04 16:37:14 2025 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Mar 04 16:38:21 2025 +0100
@@ -2847,12 +2847,6 @@
 lemma size_mset_sum_mset_conv [simp]: "size (\<Sum>\<^sub># A :: 'a multiset) = (\<Sum>X\<in>#A. size X)"
   by (induction A) auto
 
-lemma size_multiset_sum_mset [simp]: "size (\<Sum>X\<in>#A. X :: 'a multiset) = (\<Sum>X\<in>#A. size X)"
-  unfolding size_mset_sum_mset_conv
-  unfolding image_mset.identity
-  unfolding id_apply
-  ..
-
 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)"