# HG changeset patch
# User desharna
# Date 1666269809 -7200
# Node ID f7002e5b15bbb345cc935f2ee3a9ce8040b0b202
# Parent  d72a8cdca1ab43990739676aefda54da084e0891
tuned proof

diff -r d72a8cdca1ab -r f7002e5b15bb src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Oct 20 12:57:06 2022 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Oct 20 14:43:29 2022 +0200
@@ -2002,13 +2002,12 @@
   by (induct xs) simp_all
 
 lemma surj_mset: "surj mset"
-apply (unfold surj_def)
-apply (rule allI)
-apply (rule_tac M = y in multiset_induct)
- apply auto
-apply (rule_tac x = "x # xa" in exI)
-apply auto
-done
+  unfolding surj_def
+proof (rule allI)
+  fix M
+  show "\<exists>xs. M = mset xs"
+    by (induction M) (auto intro: exI[of _ "_ # _"])
+qed
 
 lemma distinct_count_atmost_1:
   "distinct x = (\<forall>a. count (mset x) a = (if a \<in> set x then 1 else 0))"