src/HOL/Library/Multiset_Order.thy

   from step(3) have "M \<noteq> N" and
     **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
     by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
   from step(2) obtain M0 a K where
     *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
-    by (blast elim: mult1_lessE)
+    by (auto elim: mult1_lessE)
   from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
   moreover
   { assume "count P a \<le> count M a"
     with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
       by (auto simp add: not_in_iff)