src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy

   have 1: "openin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
     apply (rule open_subset, force)
     using \<open>open s\<close>
     apply (simp add: open_contains_ball Ball_def)
     apply (erule all_forward)
-    using "*" by blast
+    using "*" by auto blast+
   have 2: "closedin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
     using assms
     by (auto intro: continuous_closed_in_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv)
   obtain e where "e>0" and e: "ball w e \<subseteq> s" using openE [OF \<open>open s\<close> \<open>w \<in> s\<close>] .
   then have holfb: "f holomorphic_on ball w e"