# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1507670338 -3600
# Node ID ecc99a5a1ab8095604f2a2c1f5fe58b23ca7343a
# Parent  c925393ae6b93f2f2fdd83135db84676e2b45423
fixed markup

diff -r c925393ae6b9 -r ecc99a5a1ab8 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Tue Oct 10 20:33:29 2017 +0200
+++ b/src/HOL/Analysis/Connected.thy	Tue Oct 10 22:18:58 2017 +0100
@@ -1,9 +1,9 @@
-(*  Author:     L C Paulson, University of Cambridge*)
+(*  Author:     L C Paulson, University of Cambridge
+    Material split off from Topology_Euclidean_Space
+*)
 
 section \<open>Connected Components, Homeomorphisms, Baire property, etc.\<close>
 
-text\<open>Material split off from Topology_Euclidean_Space\<close>
-
 theory Connected
 imports Topology_Euclidean_Space
 begin
@@ -1266,18 +1266,9 @@
       then obtain N :: nat where N: "\<forall>n\<ge>N. dist (t n) l < e"
         using l[unfolded lim_sequentially] by auto
       have "t (max n N) \<in> s n"
-        using assms(3)
-        unfolding subset_eq
-        apply (erule_tac x=n in allE)
-        apply (erule_tac x="max n N" in allE)
-        using t
-        apply auto
-        done
+        by (meson assms(3) contra_subsetD max.cobounded1 t)
       then have "\<exists>y\<in>s n. dist y l < e"
-        apply (rule_tac x="t (max n N)" in bexI)
-        using N
-        apply auto
-        done
+        using N max.cobounded2 by blast
     }
     then have "l \<in> s n"
       using closed_approachable[of "s n" l] assms(1) by auto
@@ -1495,11 +1486,7 @@
   have *: "f ` s \<subseteq> cball 0 b"
     using assms(2)[unfolded mem_cball_0[symmetric]] by auto
   show ?thesis
-    using image_closure_subset[OF assms(1) closed_cball[of 0 b] *] assms(3)
-    unfolding subset_eq
-    apply (erule_tac x="f x" in ballE)
-    apply (auto simp: dist_norm)
-    done
+    by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0)
 qed
 
 lemma isCont_indicator: