src/HOL/Number_Theory/UniqueFactorization.thy

     then show ?thesis
       by (subst (1) b, subst setprod.union_disjoint, auto)
   next
     case False
     then show ?thesis
-      by auto
+      by (auto simp add: not_in_iff)
   qed
   finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" .
   moreover
   have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
     apply (subst gcd.commute)

   with a show ?thesis
     using power_dvd_imp_le prime_def by blast
 next
   case False
   then show ?thesis
-    by auto
+    by (auto simp add: not_in_iff)
 qed
 
 lemma multiset_prime_factorization_unique:
   assumes "\<forall>p::nat \<in> set_mset M. prime p"
     and "\<forall>p \<in> set_mset N. prime p"

   fixes p n :: nat
   shows "\<not> prime p \<Longrightarrow> multiplicity p n = 0"
   apply (cases "n = 0")
   apply auto
   apply (frule multiset_prime_factorization)
-  apply (auto simp add: set_mset_def multiplicity_nat_def)
+  apply (auto simp add: multiplicity_nat_def count_eq_zero_iff)
   done
 
 lemma multiplicity_not_factor_nat [simp]:
   fixes p n :: nat
   shows "p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"