diff -r 89347c0cc6a3 -r 5d0d35680311 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Jun 19 17:15:40 2025 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Jun 25 14:16:30 2025 +0200
@@ -2175,6 +2175,27 @@
   \<open>mset (removeAll x xs) = filter_mset ((\<noteq>) x) (mset xs)\<close>
   by (induction xs) auto
 
+lemma singleton_set_mset_subset: fixes X Y :: "'a list set"
+  assumes "\<forall>xs \<in> X. set xs \<subseteq> {a}" "mset ` X \<subseteq> mset ` Y"
+  shows "X \<subseteq> Y"
+proof
+  fix xs assume "xs \<in> X"
+  obtain ys where ys: "ys \<in> Y" "mset xs = mset ys"
+    using \<open>xs \<in> X\<close> assms(2) by auto
+  then show "xs \<in> Y" using \<open>xs \<in> X\<close> assms(1) ys
+    by (metis singleton_iff mset_eq_setD replicate_eqI set_empty subset_singletonD size_mset)
+qed
+
+lemma singleton_set_mset_eq: fixes X Y :: "'a list set"
+  assumes "\<forall>xs \<in> X. set xs \<subseteq> {a}" "mset ` X = mset ` Y"
+  shows "X = Y"
+proof -
+  have "\<forall>ys \<in> Y. set ys \<subseteq> {a}"
+    by (metis (mono_tags, lifting) assms image_iff mset_eq_setD)
+  thus ?thesis
+    by (metis antisym assms(1,2) singleton_set_mset_subset subset_refl)
+qed
+
 global_interpretation mset_set: folding add_mset "{#}"
   defines mset_set = "folding_on.F add_mset {#}"
   by standard (simp add: fun_eq_iff)