# HG changeset patch
# User wenzelm
# Date 1730715679 -3600
# Node ID 1baf5c35d5192d4cbc3e0d4cd5abd51662603782
# Parent  cb31fd7c4bce093391d641e5f2a6857dd4abeb3c
tuned proofs;

diff -r cb31fd7c4bce -r 1baf5c35d519 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Nov 04 11:21:04 2024 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Nov 04 11:21:19 2024 +0100
@@ -4342,16 +4342,14 @@
   proof (cases "List.extract ((=) x) ys")
     case None
     hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
-    {
-      assume "mset (x # xs) \<subseteq># mset ys"
-      from set_mset_mono[OF this] x have False by simp
-    } note nle = this
+    have nle: False if "mset (x # xs) \<subseteq># mset ys"
+      using set_mset_mono[OF that] x by simp
     moreover
-    {
-      assume "mset (x # xs) \<subset># mset ys"
-      hence "mset (x # xs) \<subseteq># mset ys" by auto
-      from nle[OF this] have False .
-    }
+    have False if "mset (x # xs) \<subset># mset ys"
+    proof -
+      from that have "mset (x # xs) \<subseteq># mset ys" by auto
+      from nle[OF this] show ?thesis .
+    qed
     ultimately show ?thesis using None by auto
   next
     case (Some res)