src/HOL/Number_Theory/UniqueFactorization.thy

   shows "gcd x y =
     (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))"
   (is "_ = ?z")
 proof -
   have [arith]: "?z > 0"
-    by (rule setprod_pos_nat) auto
+    by auto
   have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = min (multiplicity p x) (multiplicity p y)"
     apply (subst multiplicity_prod_prime_powers_nat)
     apply auto
     done
   have "?z dvd x"

   shows "lcm (x::nat) y =
     (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ max (multiplicity p x) (multiplicity p y))"
   (is "_ = ?z")
 proof -
   have [arith]: "?z > 0"
-    by (rule setprod_pos_nat, auto)
+    by auto
   have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = max (multiplicity p x) (multiplicity p y)"
     apply (subst multiplicity_prod_prime_powers_nat)
     apply auto
     done
   have "x dvd ?z"