src/HOL/Topological_Spaces.thy

       by (auto simp: decseq_def)
     show "\<And>n. x \<in> (\<Inter>i\<le>n. A i)" "\<And>n. open (\<Inter>i\<le>n. A i)"
       using A by auto
     show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
       using A unfolding nhds_def
-      apply (intro INF_eq)
+      apply -
+      apply (rule INF_eq)
       apply simp_all
-      apply force
-      apply (intro exI[of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
+      apply fastforce
+      apply (intro exI [of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
       apply auto
       done
   qed
 qed
 

   "(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"
   unfolding continuous_on_def by safe (metis open_Union at_within_open UnionI)
 
 lemma continuous_on_open_UN:
   "(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
-  unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
+  by (rule continuous_on_open_Union) auto
 
 lemma continuous_on_open_Un:
   "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
   using continuous_on_open_Union [of "{s,t}"] by auto
 

   using assms unfolding compact_eq_heine_borel by metis
 
 lemma compactE_image:
   assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)"
   obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)"
-  using assms unfolding ball_simps[symmetric] SUP_def
+  using assms unfolding ball_simps [symmetric]
   by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
 
 lemma compact_inter_closed [intro]:
   assumes "compact s" and "closed t"
   shows "compact (s \<inter> t)"