# HG changeset patch
# User paulson
# Date 1598818864 -3600
# Node ID 0881bc2c607d51e3b2d30e207b0c8a69ee578126
# Parent  0f3d24dc197f144741b49d51719e3e5c7ad035c4# Parent  aa7cb84983e97a83a71502c186c0b1547cb4b234
merged

diff -r 0f3d24dc197f -r 0881bc2c607d src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Sun Aug 30 15:15:28 2020 +0000
+++ b/src/HOL/Analysis/Connected.thy	Sun Aug 30 21:21:04 2020 +0100
@@ -68,94 +68,94 @@
 
 subsection \<open>Connected components, considered as a connectedness relation or a set\<close>
 
-definition\<^marker>\<open>tag important\<close> "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
+definition\<^marker>\<open>tag important\<close> "connected_component S x y \<equiv> \<exists>T. connected T \<and> T \<subseteq> S \<and> x \<in> T \<and> y \<in> T"
 
-abbreviation "connected_component_set s x \<equiv> Collect (connected_component s x)"
+abbreviation "connected_component_set S x \<equiv> Collect (connected_component S x)"
 
 lemma connected_componentI:
-  "connected t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> t \<Longrightarrow> y \<in> t \<Longrightarrow> connected_component s x y"
+  "connected T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> x \<in> T \<Longrightarrow> y \<in> T \<Longrightarrow> connected_component S x y"
   by (auto simp: connected_component_def)
 
-lemma connected_component_in: "connected_component s x y \<Longrightarrow> x \<in> s \<and> y \<in> s"
+lemma connected_component_in: "connected_component S x y \<Longrightarrow> x \<in> S \<and> y \<in> S"
   by (auto simp: connected_component_def)
 
-lemma connected_component_refl: "x \<in> s \<Longrightarrow> connected_component s x x"
+lemma connected_component_refl: "x \<in> S \<Longrightarrow> connected_component S x x"
   by (auto simp: connected_component_def) (use connected_sing in blast)
 
-lemma connected_component_refl_eq [simp]: "connected_component s x x \<longleftrightarrow> x \<in> s"
+lemma connected_component_refl_eq [simp]: "connected_component S x x \<longleftrightarrow> x \<in> S"
   by (auto simp: connected_component_refl) (auto simp: connected_component_def)
 
-lemma connected_component_sym: "connected_component s x y \<Longrightarrow> connected_component s y x"
+lemma connected_component_sym: "connected_component S x y \<Longrightarrow> connected_component S y x"
   by (auto simp: connected_component_def)
 
 lemma connected_component_trans:
-  "connected_component s x y \<Longrightarrow> connected_component s y z \<Longrightarrow> connected_component s x z"
+  "connected_component S x y \<Longrightarrow> connected_component S y z \<Longrightarrow> connected_component S x z"
   unfolding connected_component_def
   by (metis Int_iff Un_iff Un_subset_iff equals0D connected_Un)
 
 lemma connected_component_of_subset:
-  "connected_component s x y \<Longrightarrow> s \<subseteq> t \<Longrightarrow> connected_component t x y"
+  "connected_component S x y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> connected_component T x y"
   by (auto simp: connected_component_def)
 
-lemma connected_component_Union: "connected_component_set s x = \<Union>{t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
+lemma connected_component_Union: "connected_component_set S x = \<Union>{T. connected T \<and> x \<in> T \<and> T \<subseteq> S}"
   by (auto simp: connected_component_def)
 
-lemma connected_connected_component [iff]: "connected (connected_component_set s x)"
+lemma connected_connected_component [iff]: "connected (connected_component_set S x)"
   by (auto simp: connected_component_Union intro: connected_Union)
 
 lemma connected_iff_eq_connected_component_set:
-  "connected s \<longleftrightarrow> (\<forall>x \<in> s. connected_component_set s x = s)"
-proof (cases "s = {}")
+  "connected S \<longleftrightarrow> (\<forall>x \<in> S. connected_component_set S x = S)"
+proof (cases "S = {}")
   case True
   then show ?thesis by simp
 next
   case False
-  then obtain x where "x \<in> s" by auto
+  then obtain x where "x \<in> S" by auto
   show ?thesis
   proof
-    assume "connected s"
-    then show "\<forall>x \<in> s. connected_component_set s x = s"
+    assume "connected S"
+    then show "\<forall>x \<in> S. connected_component_set S x = S"
       by (force simp: connected_component_def)
   next
-    assume "\<forall>x \<in> s. connected_component_set s x = s"
-    then show "connected s"
-      by (metis \<open>x \<in> s\<close> connected_connected_component)
+    assume "\<forall>x \<in> S. connected_component_set S x = S"
+    then show "connected S"
+      by (metis \<open>x \<in> S\<close> connected_connected_component)
   qed
 qed
 
-lemma connected_component_subset: "connected_component_set s x \<subseteq> s"
+lemma connected_component_subset: "connected_component_set S x \<subseteq> S"
   using connected_component_in by blast
 
-lemma connected_component_eq_self: "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> connected_component_set s x = s"
+lemma connected_component_eq_self: "connected S \<Longrightarrow> x \<in> S \<Longrightarrow> connected_component_set S x = S"
   by (simp add: connected_iff_eq_connected_component_set)
 
 lemma connected_iff_connected_component:
-  "connected s \<longleftrightarrow> (\<forall>x \<in> s. \<forall>y \<in> s. connected_component s x y)"
+  "connected S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. connected_component S x y)"
   using connected_component_in by (auto simp: connected_iff_eq_connected_component_set)
 
 lemma connected_component_maximal:
-  "x \<in> t \<Longrightarrow> connected t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> t \<subseteq> (connected_component_set s x)"
+  "x \<in> T \<Longrightarrow> connected T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> T \<subseteq> (connected_component_set S x)"
   using connected_component_eq_self connected_component_of_subset by blast
 
 lemma connected_component_mono:
-  "s \<subseteq> t \<Longrightarrow> connected_component_set s x \<subseteq> connected_component_set t x"
+  "S \<subseteq> T \<Longrightarrow> connected_component_set S x \<subseteq> connected_component_set T x"
   by (simp add: Collect_mono connected_component_of_subset)
 
-lemma connected_component_eq_empty [simp]: "connected_component_set s x = {} \<longleftrightarrow> x \<notin> s"
+lemma connected_component_eq_empty [simp]: "connected_component_set S x = {} \<longleftrightarrow> x \<notin> S"
   using connected_component_refl by (fastforce simp: connected_component_in)
 
 lemma connected_component_set_empty [simp]: "connected_component_set {} x = {}"
   using connected_component_eq_empty by blast
 
 lemma connected_component_eq:
-  "y \<in> connected_component_set s x \<Longrightarrow> (connected_component_set s y = connected_component_set s x)"
+  "y \<in> connected_component_set S x \<Longrightarrow> (connected_component_set S y = connected_component_set S x)"
   by (metis (no_types, lifting)
       Collect_cong connected_component_sym connected_component_trans mem_Collect_eq)
 
 lemma closed_connected_component:
-  assumes s: "closed s"
-  shows "closed (connected_component_set s x)"
-proof (cases "x \<in> s")
+  assumes S: "closed S"
+  shows "closed (connected_component_set S x)"
+proof (cases "x \<in> S")
   case False
   then show ?thesis
     by (metis connected_component_eq_empty closed_empty)
@@ -164,29 +164,29 @@
   show ?thesis
     unfolding closure_eq [symmetric]
   proof
-    show "closure (connected_component_set s x) \<subseteq> connected_component_set s x"
+    show "closure (connected_component_set S x) \<subseteq> connected_component_set S x"
       apply (rule connected_component_maximal)
         apply (simp add: closure_def True)
        apply (simp add: connected_imp_connected_closure)
-      apply (simp add: s closure_minimal connected_component_subset)
+      apply (simp add: S closure_minimal connected_component_subset)
       done
   next
-    show "connected_component_set s x \<subseteq> closure (connected_component_set s x)"
+    show "connected_component_set S x \<subseteq> closure (connected_component_set S x)"
       by (simp add: closure_subset)
   qed
 qed
 
 lemma connected_component_disjoint:
-  "connected_component_set s a \<inter> connected_component_set s b = {} \<longleftrightarrow>
-    a \<notin> connected_component_set s b"
+  "connected_component_set S a \<inter> connected_component_set S b = {} \<longleftrightarrow>
+    a \<notin> connected_component_set S b"
   apply (auto simp: connected_component_eq)
   using connected_component_eq connected_component_sym
   apply blast
   done
 
 lemma connected_component_nonoverlap:
-  "connected_component_set s a \<inter> connected_component_set s b = {} \<longleftrightarrow>
-    a \<notin> s \<or> b \<notin> s \<or> connected_component_set s a \<noteq> connected_component_set s b"
+  "connected_component_set S a \<inter> connected_component_set S b = {} \<longleftrightarrow>
+    a \<notin> S \<or> b \<notin> S \<or> connected_component_set S a \<noteq> connected_component_set S b"
   apply (auto simp: connected_component_in)
   using connected_component_refl_eq
     apply blast
@@ -195,30 +195,30 @@
   done
 
 lemma connected_component_overlap:
-  "connected_component_set s a \<inter> connected_component_set s b \<noteq> {} \<longleftrightarrow>
-    a \<in> s \<and> b \<in> s \<and> connected_component_set s a = connected_component_set s b"
+  "connected_component_set S a \<inter> connected_component_set S b \<noteq> {} \<longleftrightarrow>
+    a \<in> S \<and> b \<in> S \<and> connected_component_set S a = connected_component_set S b"
   by (auto simp: connected_component_nonoverlap)
 
-lemma connected_component_sym_eq: "connected_component s x y \<longleftrightarrow> connected_component s y x"
+lemma connected_component_sym_eq: "connected_component S x y \<longleftrightarrow> connected_component S y x"
   using connected_component_sym by blast
 
 lemma connected_component_eq_eq:
-  "connected_component_set s x = connected_component_set s y \<longleftrightarrow>
-    x \<notin> s \<and> y \<notin> s \<or> x \<in> s \<and> y \<in> s \<and> connected_component s x y"
-  apply (cases "y \<in> s", simp)
+  "connected_component_set S x = connected_component_set S y \<longleftrightarrow>
+    x \<notin> S \<and> y \<notin> S \<or> x \<in> S \<and> y \<in> S \<and> connected_component S x y"
+  apply (cases "y \<in> S", simp)
    apply (metis connected_component_eq connected_component_eq_empty connected_component_refl_eq mem_Collect_eq)
-  apply (cases "x \<in> s", simp)
+  apply (cases "x \<in> S", simp)
    apply (metis connected_component_eq_empty)
   using connected_component_eq_empty
   apply blast
   done
 
 lemma connected_iff_connected_component_eq:
-  "connected s \<longleftrightarrow> (\<forall>x \<in> s. \<forall>y \<in> s. connected_component_set s x = connected_component_set s y)"
+  "connected S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. connected_component_set S x = connected_component_set S y)"
   by (simp add: connected_component_eq_eq connected_iff_connected_component)
 
 lemma connected_component_idemp:
-  "connected_component_set (connected_component_set s x) x = connected_component_set s x"
+  "connected_component_set (connected_component_set S x) x = connected_component_set S x"
   apply (rule subset_antisym)
    apply (simp add: connected_component_subset)
   apply (metis connected_component_eq_empty connected_component_maximal
@@ -226,25 +226,24 @@
   done
 
 lemma connected_component_unique:
-  "\<lbrakk>x \<in> c; c \<subseteq> s; connected c;
-    \<And>c'. x \<in> c' \<and> c' \<subseteq> s \<and> connected c'
-              \<Longrightarrow> c' \<subseteq> c\<rbrakk>
-        \<Longrightarrow> connected_component_set s x = c"
-apply (rule subset_antisym)
-apply (meson connected_component_maximal connected_component_subset connected_connected_component contra_subsetD)
-by (simp add: connected_component_maximal)
+  "\<lbrakk>x \<in> c; c \<subseteq> S; connected c;
+    \<And>c'. \<lbrakk>x \<in> c'; c' \<subseteq> S; connected c'\<rbrakk> \<Longrightarrow> c' \<subseteq> c\<rbrakk>
+        \<Longrightarrow> connected_component_set S x = c"
+  apply (rule subset_antisym)
+   apply (meson connected_component_maximal connected_component_subset connected_connected_component contra_subsetD)
+  by (simp add: connected_component_maximal)
 
 lemma joinable_connected_component_eq:
-  "\<lbrakk>connected t; t \<subseteq> s;
-    connected_component_set s x \<inter> t \<noteq> {};
-    connected_component_set s y \<inter> t \<noteq> {}\<rbrakk>
-    \<Longrightarrow> connected_component_set s x = connected_component_set s y"
+  "\<lbrakk>connected T; T \<subseteq> S;
+    connected_component_set S x \<inter> T \<noteq> {};
+    connected_component_set S y \<inter> T \<noteq> {}\<rbrakk>
+    \<Longrightarrow> connected_component_set S x = connected_component_set S y"
 apply (simp add: ex_in_conv [symmetric])
 apply (rule connected_component_eq)
 by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
 
 
-lemma Union_connected_component: "\<Union>(connected_component_set s ` s) = s"
+lemma Union_connected_component: "\<Union>(connected_component_set S ` S) = S"
   apply (rule subset_antisym)
   apply (simp add: SUP_least connected_component_subset)
   using connected_component_refl_eq
@@ -252,16 +251,16 @@
 
 
 lemma complement_connected_component_unions:
-    "s - connected_component_set s x =
-     \<Union>(connected_component_set s ` s - {connected_component_set s x})"
+    "S - connected_component_set S x =
+     \<Union>(connected_component_set S ` S - {connected_component_set S x})"
   apply (subst Union_connected_component [symmetric], auto)
   apply (metis connected_component_eq_eq connected_component_in)
   by (metis connected_component_eq mem_Collect_eq)
 
 lemma connected_component_intermediate_subset:
-        "\<lbrakk>connected_component_set u a \<subseteq> t; t \<subseteq> u\<rbrakk>
-        \<Longrightarrow> connected_component_set t a = connected_component_set u a"
-  apply (case_tac "a \<in> u")
+        "\<lbrakk>connected_component_set U a \<subseteq> T; T \<subseteq> U\<rbrakk>
+        \<Longrightarrow> connected_component_set T a = connected_component_set U a"
+  apply (case_tac "a \<in> U")
   apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
   using connected_component_eq_empty by blast
 
@@ -269,17 +268,17 @@
 subsection \<open>The set of connected components of a set\<close>
 
 definition\<^marker>\<open>tag important\<close> components:: "'a::topological_space set \<Rightarrow> 'a set set"
-  where "components s \<equiv> connected_component_set s ` s"
+  where "components S \<equiv> connected_component_set S ` S"
 
-lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
+lemma components_iff: "S \<in> components U \<longleftrightarrow> (\<exists>x. x \<in> U \<and> S = connected_component_set U x)"
   by (auto simp: components_def)
 
-lemma componentsI: "x \<in> u \<Longrightarrow> connected_component_set u x \<in> components u"
+lemma componentsI: "x \<in> U \<Longrightarrow> connected_component_set U x \<in> components U"
   by (auto simp: components_def)
 
 lemma componentsE:
-  assumes "s \<in> components u"
-  obtains x where "x \<in> u" "s = connected_component_set u x"
+  assumes "S \<in> components U"
+  obtains x where "x \<in> U" "S = connected_component_set U x"
   using assms by (auto simp: components_def)
 
 lemma Union_components [simp]: "\<Union>(components u) = u"
diff -r 0f3d24dc197f -r 0881bc2c607d src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Sun Aug 30 15:15:28 2020 +0000
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Sun Aug 30 21:21:04 2020 +0100
@@ -61,7 +61,7 @@
   by (simp add: subset_eq)
 
 lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"
-  by (auto)
+  by auto
 
 lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
   by force
@@ -70,34 +70,34 @@
   by auto
 
 lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
-  by (simp add: subset_eq)
+  by auto
 
 lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e"
-  by (simp add: subset_eq)
+  by auto
 
 lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"
-  by (auto)
+  by auto
 
 lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
-  by (auto)
+  by auto
 
 lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
   by metric
 
 lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
-  by (simp add: set_eq_iff) arith
+  by auto
 
 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
-  by (simp add: set_eq_iff)
+  by auto
 
 lemma cball_max_Un: "cball a (max r s) = cball a r \<union> cball a s"
-  by (simp add: set_eq_iff) arith
+  by auto
 
 lemma cball_min_Int: "cball a (min r s) = cball a r \<inter> cball a s"
-  by (simp add: set_eq_iff)
+  by auto
 
 lemma cball_diff_eq_sphere: "cball a r - ball a r =  sphere a r"
-  by (auto simp: cball_def ball_def dist_commute)
+  by auto
 
 lemma open_ball [intro, simp]: "open (ball x e)"
 proof -
@@ -126,7 +126,8 @@
   unfolding mem_ball set_eq_iff
   by (simp add: not_less) metric
 
-lemma ball_empty: "e \<le> 0 \<Longrightarrow> ball x e = {}" by simp
+lemma ball_empty: "e \<le> 0 \<Longrightarrow> ball x e = {}" 
+  by simp
 
 lemma closed_cball [iff]: "closed (cball x e)"
 proof -
@@ -142,16 +143,15 @@
   {
     fix x and e::real
     assume "x\<in>S" "e>0" "ball x e \<subseteq> S"
-    then have "\<exists>d>0. cball x d \<subseteq> S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto)
+    then have "\<exists>d>0. cball x d \<subseteq> S"
+      unfolding subset_eq by (rule_tac x="e/2" in exI, auto)
   }
   moreover
   {
     fix x and e::real
     assume "x\<in>S" "e>0" "cball x e \<subseteq> S"
     then have "\<exists>d>0. ball x d \<subseteq> S"
-      unfolding subset_eq
-      apply (rule_tac x="e/2" in exI, auto)
-      done
+      using mem_ball_imp_mem_cball by blast
   }
   ultimately show ?thesis
     unfolding open_contains_ball by auto
@@ -206,24 +206,17 @@
 lemma cball_sing:
   fixes x :: "'a::metric_space"
   shows "e = 0 \<Longrightarrow> cball x e = {x}"
-  by (auto simp: set_eq_iff)
+  by simp
 
 lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"
-  apply (cases "e \<le> 0")
-  apply (simp add: ball_empty field_split_simps)
-  apply (rule subset_ball)
-  apply (simp add: field_split_simps)
-  done
+  by (metis ball_eq_empty div_by_1 frac_le linear subset_ball zero_less_one)
 
 lemma ball_divide_subset_numeral: "ball x (e / numeral w) \<subseteq> ball x e"
   using ball_divide_subset one_le_numeral by blast
 
 lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"
-  apply (cases "e < 0")
-  apply (simp add: field_split_simps)
-  apply (rule subset_cball)
-  apply (metis div_by_1 frac_le not_le order_refl zero_less_one)
-  done
+  apply (cases "e < 0", simp add: field_split_simps)
+  by (metis div_by_1 frac_le less_numeral_extra(1) not_le order_refl subset_cball)
 
 lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
   using cball_divide_subset one_le_numeral by blast
@@ -2141,7 +2134,7 @@
     then have D: "T \<subseteq> V" unfolding V_def by auto
 
     have "(ball x ((infdist x T)/2)) \<inter> (ball y ((infdist y S)/2)) = {}" if "x \<in> S" "y \<in> T" for x y
-    proof (auto)
+    proof auto
       fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"
       have "2 * dist x y \<le> 2 * dist x z + 2 * dist y z"
         by metric
@@ -2728,8 +2721,8 @@
 subsection \<open>With Abstract Topology (TODO: move and remove dependency?)\<close>
 
 lemma openin_contains_ball:
-    "openin (top_of_set t) s \<longleftrightarrow>
-     s \<subseteq> t \<and> (\<forall>x \<in> s. \<exists>e. 0 < e \<and> ball x e \<inter> t \<subseteq> s)"
+    "openin (top_of_set T) S \<longleftrightarrow>
+     S \<subseteq> T \<and> (\<forall>x \<in> S. \<exists>e. 0 < e \<and> ball x e \<inter> T \<subseteq> S)"
     (is "?lhs = ?rhs")
 proof
   assume ?lhs
@@ -2745,14 +2738,18 @@
 qed
 
 lemma openin_contains_cball:
-   "openin (top_of_set t) s \<longleftrightarrow>
-        s \<subseteq> t \<and>
-        (\<forall>x \<in> s. \<exists>e. 0 < e \<and> cball x e \<inter> t \<subseteq> s)"
-  apply (simp add: openin_contains_ball)
-  apply (rule iffI)
-   apply (auto dest!: bspec)
-   apply (rule_tac x="e/2" in exI, force+)
-  done
+   "openin (top_of_set T) S \<longleftrightarrow>
+        S \<subseteq> T \<and> (\<forall>x \<in> S. \<exists>e. 0 < e \<and> cball x e \<inter> T \<subseteq> S)"
+    (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (force simp add: openin_contains_ball intro: exI [where x="_/2"])
+next
+  assume ?rhs
+  then show ?lhs
+    by (force simp add: openin_contains_ball)
+qed
 
 
 subsection \<open>Closed Nest\<close>
@@ -3086,9 +3083,9 @@
   by (auto intro!: bdd_belowI [where m=0] cInf_lower)
 
 lemma le_setdist_iff:
-        "d \<le> setdist s t \<longleftrightarrow>
-        (\<forall>x \<in> s. \<forall>y \<in> t. d \<le> dist x y) \<and> (s = {} \<or> t = {} \<longrightarrow> d \<le> 0)"
-  apply (cases "s = {} \<or> t = {}")
+        "d \<le> setdist S T \<longleftrightarrow>
+        (\<forall>x \<in> S. \<forall>y \<in> T. d \<le> dist x y) \<and> (S = {} \<or> T = {} \<longrightarrow> d \<le> 0)"
+  apply (cases "S = {} \<or> T = {}")
   apply (force simp add: setdist_def)
   apply (intro iffI conjI)
   using setdist_le_dist apply fastforce
@@ -3096,34 +3093,33 @@
   done
 
 lemma setdist_ltE:
-  assumes "setdist s t < b" "s \<noteq> {}" "t \<noteq> {}"
-    obtains x y where "x \<in> s" "y \<in> t" "dist x y < b"
+  assumes "setdist S T < b" "S \<noteq> {}" "T \<noteq> {}"
+    obtains x y where "x \<in> S" "y \<in> T" "dist x y < b"
 using assms
 by (auto simp: not_le [symmetric] le_setdist_iff)
 
-lemma setdist_refl: "setdist s s = 0"
-  apply (cases "s = {}")
+lemma setdist_refl: "setdist S S = 0"
+  apply (cases "S = {}")
   apply (force simp add: setdist_def)
   apply (rule antisym [OF _ setdist_pos_le])
   apply (metis all_not_in_conv dist_self setdist_le_dist)
   done
 
-lemma setdist_sym: "setdist s t = setdist t s"
+lemma setdist_sym: "setdist S T = setdist T S"
   by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])
 
-lemma setdist_triangle: "setdist s t \<le> setdist s {a} + setdist {a} t"
-proof (cases "s = {} \<or> t = {}")
+lemma setdist_triangle: "setdist S T \<le> setdist S {a} + setdist {a} T"
+proof (cases "S = {} \<or> T = {}")
   case True then show ?thesis
     using setdist_pos_le by fastforce
 next
   case False
-  have "\<And>x. x \<in> s \<Longrightarrow> setdist s t - dist x a \<le> setdist {a} t"
-    apply (rule le_setdistI, blast)
-    using False apply (fastforce intro: le_setdistI)
-    apply (simp add: algebra_simps)
+  then have "\<And>x. x \<in> S \<Longrightarrow> setdist S T - dist x a \<le> setdist {a} T"
+    apply (intro le_setdistI)
+    apply (simp_all add: algebra_simps)
     apply (metis dist_commute dist_triangle3 order_trans [OF setdist_le_dist])
     done
-  then have "setdist s t - setdist {a} t \<le> setdist s {a}"
+  then have "setdist S T - setdist {a} T \<le> setdist S {a}"
     using False by (fastforce intro: le_setdistI)
   then show ?thesis
     by (simp add: algebra_simps)
@@ -3132,52 +3128,48 @@
 lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
   by (simp add: setdist_def)
 
-lemma setdist_Lipschitz: "\<bar>setdist {x} s - setdist {y} s\<bar> \<le> dist x y"
+lemma setdist_Lipschitz: "\<bar>setdist {x} S - setdist {y} S\<bar> \<le> dist x y"
   apply (subst setdist_singletons [symmetric])
   by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
 
-lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\<lambda>y. (setdist {y} s))"
+lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\<lambda>y. (setdist {y} S))"
   by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
 
-lemma continuous_on_setdist [continuous_intros]: "continuous_on t (\<lambda>y. (setdist {y} s))"
+lemma continuous_on_setdist [continuous_intros]: "continuous_on T (\<lambda>y. (setdist {y} S))"
   by (metis continuous_at_setdist continuous_at_imp_continuous_on)
 
-lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\<lambda>y. (setdist {y} s))"
+lemma uniformly_continuous_on_setdist: "uniformly_continuous_on T (\<lambda>y. (setdist {y} S))"
   by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
 
-lemma setdist_subset_right: "\<lbrakk>t \<noteq> {}; t \<subseteq> u\<rbrakk> \<Longrightarrow> setdist s u \<le> setdist s t"
-  apply (cases "s = {} \<or> u = {}", force)
+lemma setdist_subset_right: "\<lbrakk>T \<noteq> {}; T \<subseteq> u\<rbrakk> \<Longrightarrow> setdist S u \<le> setdist S T"
+  apply (cases "S = {} \<or> u = {}", force)
   apply (auto simp: setdist_def intro!: bdd_belowI [where m=0] cInf_superset_mono)
   done
 
-lemma setdist_subset_left: "\<lbrakk>s \<noteq> {}; s \<subseteq> t\<rbrakk> \<Longrightarrow> setdist t u \<le> setdist s u"
+lemma setdist_subset_left: "\<lbrakk>S \<noteq> {}; S \<subseteq> T\<rbrakk> \<Longrightarrow> setdist T u \<le> setdist S u"
   by (metis setdist_subset_right setdist_sym)
 
-lemma setdist_closure_1 [simp]: "setdist (closure s) t = setdist s t"
-proof (cases "s = {} \<or> t = {}")
+lemma setdist_closure_1 [simp]: "setdist (closure S) T = setdist S T"
+proof (cases "S = {} \<or> T = {}")
   case True then show ?thesis by force
 next
   case False
   { fix y
-    assume "y \<in> t"
-    have "continuous_on (closure s) (\<lambda>a. dist a y)"
+    assume "y \<in> T"
+    have "continuous_on (closure S) (\<lambda>a. dist a y)"
       by (auto simp: continuous_intros dist_norm)
-    then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"
-      apply (rule continuous_ge_on_closure)
-      apply assumption
-      apply (blast intro: setdist_le_dist \<open>y \<in> t\<close> )
-      done
+    then have *: "\<And>x. x \<in> closure S \<Longrightarrow> setdist S T \<le> dist x y"
+      by (fast intro: setdist_le_dist \<open>y \<in> T\<close> continuous_ge_on_closure)
   } note * = this
   show ?thesis
     apply (rule antisym)
      using False closure_subset apply (blast intro: setdist_subset_left)
-    using False *
-    apply (force intro!: le_setdistI)
+    using False * apply (force intro!: le_setdistI)
     done
 qed
 
-lemma setdist_closure_2 [simp]: "setdist t (closure s) = setdist t s"
-by (metis setdist_closure_1 setdist_sym)
+lemma setdist_closure_2 [simp]: "setdist T (closure S) = setdist T S"
+  by (metis setdist_closure_1 setdist_sym)
 
 lemma setdist_eq_0I: "\<lbrakk>x \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> setdist S T = 0"
   by (metis antisym dist_self setdist_le_dist setdist_pos_le)
diff -r 0f3d24dc197f -r 0881bc2c607d src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Sun Aug 30 15:15:28 2020 +0000
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Sun Aug 30 21:21:04 2020 +0100
@@ -482,7 +482,8 @@
     define U where "U = {x<..<y}"
     then have "open U" by simp
     moreover have "z \<in> U" using z U_def by simp
-    ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+    ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" 
+      using topological_basisE[OF \<open>topological_basis A\<close>] by auto
     define w where "w = (SOME x. x \<in> V)"
     then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
     then have "x < w \<and> w \<le> y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
@@ -494,7 +495,8 @@
     define U where "U = {x<..}"
     then have "open U" by simp
     moreover have "y \<in> U" using \<open>x < y\<close> U_def by simp
-    ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+    ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" 
+      using topological_basisE[OF \<open>topological_basis A\<close>] by auto
     have "U = {y..}" unfolding U_def using * \<open>x < y\<close> by auto
     then have "V \<subseteq> {y..}" using \<open>V \<subseteq> U\<close> by simp
     then have "(LEAST w. w \<in> V) = y" using \<open>y \<in> V\<close> by (meson Least_equality atLeast_iff subsetCE)
@@ -521,7 +523,8 @@
     define U where "U = {x<..<y}"
     then have "open U" by simp
     moreover have "z \<in> U" using z U_def by simp
-    ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+    ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" 
+      using topological_basisE[OF \<open>topological_basis A\<close>] by auto
     define w where "w = (SOME x. x \<in> V)"
     then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
     then have "x \<le> w \<and> w < y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
@@ -533,7 +536,8 @@
     define U where "U = {..<y}"
     then have "open U" by simp
     moreover have "x \<in> U" using \<open>x < y\<close> U_def by simp
-    ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+    ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" 
+      using topological_basisE[OF \<open>topological_basis A\<close>] by auto
     have "U = {..x}" unfolding U_def using * \<open>x < y\<close> by auto
     then have "V \<subseteq> {..x}" using \<open>V \<subseteq> U\<close> by simp
     then have "(GREATEST x. x \<in> V) = x" using \<open>x \<in> V\<close> by (meson Greatest_equality atMost_iff subsetCE)
@@ -1556,18 +1560,12 @@
   shows "infinite (range f)"
 proof
   assume "finite (range f)"
-  then have "closed (range f)"
-    by (rule finite_imp_closed)
-  then have "open (- range f)"
-    by (rule open_Compl)
-  from assms(1) have "l \<in> - range f"
-    by auto
-  from assms(2) have "eventually (\<lambda>n. f n \<in> - range f) sequentially"
-    using \<open>open (- range f)\<close> \<open>l \<in> - range f\<close>
-    by (rule topological_tendstoD)
+  then have "l \<notin> range f \<and> closed (range f)"
+    using \<open>finite (range f)\<close> assms(1) finite_imp_closed by blast
+  then have "eventually (\<lambda>n. f n \<in> - range f) sequentially"
+    by (metis Compl_iff assms(2) open_Compl topological_tendstoD)
   then show False
-    unfolding eventually_sequentially
-    by auto
+    unfolding eventually_sequentially by auto
 qed
 
 lemma Bolzano_Weierstrass_imp_closed:
diff -r 0f3d24dc197f -r 0881bc2c607d src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Sun Aug 30 15:15:28 2020 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Sun Aug 30 21:21:04 2020 +0100
@@ -1629,8 +1629,7 @@
   then have "y \<in> S"
     by (simp add: path_component_mem(2))
   then obtain e where e: "e > 0" "ball y e \<subseteq> S"
-    using assms[unfolded open_contains_ball]
-    by auto
+    using assms openE by blast
 have "\<And>u. dist y u < e \<Longrightarrow> path_component S x u"
       by (metis (full_types) as centre_in_ball convex_ball convex_imp_path_connected e mem_Collect_eq mem_ball path_component_eq path_component_of_subset path_connected_component)
   then show "\<exists>e > 0. ball y e \<subseteq> path_component_set S x"
@@ -2863,30 +2862,33 @@
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relations between components and path components\<close>
 
 lemma open_connected_component:
-  fixes s :: "'a::real_normed_vector set"
-  shows "open s \<Longrightarrow> open (connected_component_set s x)"
-    apply (simp add: open_contains_ball, clarify)
-    apply (rename_tac y)
-    apply (drule_tac x=y in bspec)
-     apply (simp add: connected_component_in, clarify)
-    apply (rule_tac x=e in exI)
-    by (metis mem_Collect_eq connected_component_eq connected_component_maximal centre_in_ball connected_ball)
+  fixes S :: "'a::real_normed_vector set"
+  assumes "open S"
+  shows "open (connected_component_set S x)"
+proof (clarsimp simp: open_contains_ball)
+  fix y
+  assume xy: "connected_component S x y"
+  then obtain e where "e>0" "ball y e \<subseteq> S"
+    using assms connected_component_in openE by blast
+  then show "\<exists>e>0. ball y e  \<subseteq> connected_component_set S x"
+    by (metis xy centre_in_ball connected_ball connected_component_eq_eq connected_component_in connected_component_maximal)
+qed
 
 corollary open_components:
-    fixes s :: "'a::real_normed_vector set"
-    shows "\<lbrakk>open u; s \<in> components u\<rbrakk> \<Longrightarrow> open s"
+    fixes S :: "'a::real_normed_vector set"
+    shows "\<lbrakk>open u; S \<in> components u\<rbrakk> \<Longrightarrow> open S"
   by (simp add: components_iff) (metis open_connected_component)
 
 lemma in_closure_connected_component:
-  fixes s :: "'a::real_normed_vector set"
-  assumes x: "x \<in> s" and s: "open s"
-  shows "x \<in> closure (connected_component_set s y) \<longleftrightarrow>  x \<in> connected_component_set s y"
+  fixes S :: "'a::real_normed_vector set"
+  assumes x: "x \<in> S" and S: "open S"
+  shows "x \<in> closure (connected_component_set S y) \<longleftrightarrow>  x \<in> connected_component_set S y"
 proof -
-  { assume "x \<in> closure (connected_component_set s y)"
-    moreover have "x \<in> connected_component_set s x"
+  { assume "x \<in> closure (connected_component_set S y)"
+    moreover have "x \<in> connected_component_set S x"
       using x by simp
-    ultimately have "x \<in> connected_component_set s y"
-      using s by (meson Compl_disjoint closure_iff_nhds_not_empty connected_component_disjoint disjoint_eq_subset_Compl open_connected_component)
+    ultimately have "x \<in> connected_component_set S y"
+      using S by (meson Compl_disjoint closure_iff_nhds_not_empty connected_component_disjoint disjoint_eq_subset_Compl open_connected_component)
   }
   then show ?thesis
     by (auto simp: closure_def)
@@ -2957,76 +2959,72 @@
 proof -
   have "open S" using assms by blast
   show ?thesis
-    apply (rule connected_disjoint_Union_open_unique)
-    apply (simp add: components_eq disjnt_def pairwise_def)
-    using \<open>open S\<close>
-    apply (simp_all add: assms open_components in_components_connected in_components_nonempty)
-    done
+  proof (rule connected_disjoint_Union_open_unique)
+    show "disjoint (components S)"
+      by (simp add: components_eq disjnt_def pairwise_def)
+  qed (use \<open>open S\<close> in \<open>simp_all add: assms open_components in_components_connected in_components_nonempty\<close>)
 qed
 
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Existence of unbounded components\<close>
 
 lemma cobounded_unbounded_component:
-    fixes s :: "'a :: euclidean_space set"
-    assumes "bounded (-s)"
-      shows "\<exists>x. x \<in> s \<and> \<not> bounded (connected_component_set s x)"
+    fixes S :: "'a :: euclidean_space set"
+    assumes "bounded (-S)"
+      shows "\<exists>x. x \<in> S \<and> \<not> bounded (connected_component_set S x)"
 proof -
   obtain i::'a where i: "i \<in> Basis"
     using nonempty_Basis by blast
-  obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
+  obtain B where B: "B>0" "-S \<subseteq> ball 0 B"
     using bounded_subset_ballD [OF assms, of 0] by auto
-  then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
+  then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> S"
     by (force simp: ball_def dist_norm)
   have unbounded_inner: "\<not> bounded {x. inner i x \<ge> B}"
-    apply (auto simp: bounded_def dist_norm)
+  proof (clarsimp simp: bounded_def dist_norm)
+    fix e x
+    show "\<exists>y. B \<le> i \<bullet> y \<and> \<not> norm (x - y) \<le> e"
     apply (rule_tac x="x + (max B e + 1 + \<bar>i \<bullet> x\<bar>) *\<^sub>R i" in exI)
-    apply simp
-    using i
-    apply (auto simp: algebra_simps)
-    done
-  have **: "{x. B \<le> i \<bullet> x} \<subseteq> connected_component_set s (B *\<^sub>R i)"
+      using i by (auto simp: inner_right_distrib)
+  qed
+  have \<section>: "\<And>x. B \<le> i \<bullet> x \<Longrightarrow> x \<in> S"
+    using * Basis_le_norm [OF i] by (metis abs_ge_self inner_commute order_trans)
+  have "{x. B \<le> i \<bullet> x} \<subseteq> connected_component_set S (B *\<^sub>R i)"
     apply (rule connected_component_maximal)
-    apply (auto simp: i intro: convex_connected convex_halfspace_ge [of B])
-    apply (rule *)
-    apply (rule order_trans [OF _ Basis_le_norm [OF i]])
-    by (simp add: inner_commute)
-  have "B *\<^sub>R i \<in> s"
+      apply (auto simp: i intro: convex_connected convex_halfspace_ge [of B] \<section>)
+    done
+  then have "\<not> bounded (connected_component_set S (B *\<^sub>R i))"
+    using bounded_subset unbounded_inner by blast
+  moreover have "B *\<^sub>R i \<in> S"
     by (rule *) (simp add: norm_Basis [OF i])
-  then show ?thesis
-    apply (rule_tac x="B *\<^sub>R i" in exI, clarify)
-    apply (frule bounded_subset [of _ "{x. B \<le> i \<bullet> x}", OF _ **])
-    using unbounded_inner apply blast
-    done
+  ultimately show ?thesis
+    by blast
 qed
 
 lemma cobounded_unique_unbounded_component:
-    fixes s :: "'a :: euclidean_space set"
-    assumes bs: "bounded (-s)" and "2 \<le> DIM('a)"
-        and bo: "\<not> bounded(connected_component_set s x)"
-                "\<not> bounded(connected_component_set s y)"
-      shows "connected_component_set s x = connected_component_set s y"
+    fixes S :: "'a :: euclidean_space set"
+    assumes bs: "bounded (-S)" and "2 \<le> DIM('a)"
+        and bo: "\<not> bounded(connected_component_set S x)"
+                "\<not> bounded(connected_component_set S y)"
+      shows "connected_component_set S x = connected_component_set S y"
 proof -
   obtain i::'a where i: "i \<in> Basis"
     using nonempty_Basis by blast
-  obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
+  obtain B where B: "B>0" "-S \<subseteq> ball 0 B"
     using bounded_subset_ballD [OF bs, of 0] by auto
-  then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
+  then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> S"
     by (force simp: ball_def dist_norm)
-  have ccb: "connected (- ball 0 B :: 'a set)"
-    using assms by (auto intro: connected_complement_bounded_convex)
-  obtain x' where x': "connected_component s x x'" "norm x' > B"
+  obtain x' where x': "connected_component S x x'" "norm x' > B"
     using bo [unfolded bounded_def dist_norm, simplified, rule_format]
     by (metis diff_zero norm_minus_commute not_less)
-  obtain y' where y': "connected_component s y y'" "norm y' > B"
+  obtain y' where y': "connected_component S y y'" "norm y' > B"
     using bo [unfolded bounded_def dist_norm, simplified, rule_format]
     by (metis diff_zero norm_minus_commute not_less)
-  have x'y': "connected_component s x' y'"
-    apply (simp add: connected_component_def)
-    apply (rule_tac x="- ball 0 B" in exI)
-    using x' y'
-    apply (auto simp: ccb dist_norm *)
-    done
+  have x'y': "connected_component S x' y'"
+    unfolding connected_component_def
+  proof (intro exI conjI)
+    show "connected (- ball 0 B :: 'a set)"
+      using assms by (auto intro: connected_complement_bounded_convex)
+  qed (use x' y' dist_norm * in auto)
   show ?thesis
     apply (rule connected_component_eq)
     using x' y' x'y'
@@ -3034,13 +3032,13 @@
 qed
 
 lemma cobounded_unbounded_components:
-    fixes s :: "'a :: euclidean_space set"
-    shows "bounded (-s) \<Longrightarrow> \<exists>c. c \<in> components s \<and> \<not>bounded c"
+    fixes S :: "'a :: euclidean_space set"
+    shows "bounded (-S) \<Longrightarrow> \<exists>c. c \<in> components S \<and> \<not>bounded c"
   by (metis cobounded_unbounded_component components_def imageI)
 
 lemma cobounded_unique_unbounded_components:
-    fixes s :: "'a :: euclidean_space set"
-    shows  "\<lbrakk>bounded (- s); c \<in> components s; \<not> bounded c; c' \<in> components s; \<not> bounded c'; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> c' = c"
+    fixes S :: "'a :: euclidean_space set"
+    shows  "\<lbrakk>bounded (- S); c \<in> components S; \<not> bounded c; c' \<in> components S; \<not> bounded c'; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> c' = c"
   unfolding components_iff
   by (metis cobounded_unique_unbounded_component)
 
@@ -3169,25 +3167,23 @@
     assumes "bounded S" "2 \<le> DIM('a)"
       shows "connected(outside S)"
   apply (clarsimp simp add: connected_iff_connected_component outside)
-  apply (rule_tac s="connected_component_set (- S) x" in connected_component_of_subset)
+  apply (rule_tac S="connected_component_set (- S) x" in connected_component_of_subset)
   apply (metis (no_types) assms cobounded_unbounded_component cobounded_unique_unbounded_component connected_component_eq_eq connected_component_idemp double_complement mem_Collect_eq)
   apply clarify
   apply (metis connected_component_eq_eq connected_component_in)
   done
 
 lemma outside_connected_component_lt:
-    "outside S = {x. \<forall>B. \<exists>y. B < norm(y) \<and> connected_component (- S) x y}"
-apply (auto simp: outside bounded_def dist_norm)
-apply (metis diff_0 norm_minus_cancel not_less)
-by (metis less_diff_eq norm_minus_commute norm_triangle_ineq2 order.trans pinf(6))
+  "outside S = {x. \<forall>B. \<exists>y. B < norm(y) \<and> connected_component (- S) x y}"
+  apply (auto simp: outside bounded_def dist_norm)
+   apply (metis diff_0 norm_minus_cancel not_less)
+  by (metis less_diff_eq norm_minus_commute norm_triangle_ineq2 order.trans pinf(6))
 
 lemma outside_connected_component_le:
-   "outside S =
-            {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and>
-                         connected_component (- S) x y}"
-apply (simp add: outside_connected_component_lt)
-apply (simp add: Set.set_eq_iff)
-by (meson gt_ex leD le_less_linear less_imp_le order.trans)
+  "outside S =
+            {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> connected_component (- S) x y}"
+  apply (simp add: outside_connected_component_lt Set.set_eq_iff)
+  by (meson gt_ex leD le_less_linear less_imp_le order.trans)
 
 lemma not_outside_connected_component_lt:
     fixes S :: "'a::euclidean_space set"
@@ -3199,28 +3195,23 @@
   { fix y::'a and z::'a
     assume yz: "B < norm z" "B < norm y"
     have "connected_component (- cball 0 B) y z"
-      apply (rule connected_componentI [OF _ subset_refl])
-      apply (rule connected_complement_bounded_convex)
-      using assms yz
-      by (auto simp: dist_norm)
+      apply (intro connected_componentI [OF _ subset_refl] connected_complement_bounded_convex)
+      using assms yz by (auto simp: dist_norm)
     then have "connected_component (- S) y z"
-      apply (rule connected_component_of_subset)
-      apply (metis Bno Compl_anti_mono mem_cball_0 subset_iff)
-      done
+      by (metis connected_component_of_subset Bno Compl_anti_mono mem_cball_0 subset_iff)
   } note cyz = this
   show ?thesis
-    apply (auto simp: outside)
+    apply (auto simp: outside bounded_pos)
     apply (metis Compl_iff bounded_iff cobounded_imp_unbounded mem_Collect_eq not_le)
-    apply (simp add: bounded_pos)
     by (metis B connected_component_trans cyz not_le)
 qed
 
 lemma not_outside_connected_component_le:
-    fixes S :: "'a::euclidean_space set"
-    assumes S: "bounded S"  "2 \<le> DIM('a)"
-      shows "- (outside S) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> \<not> connected_component (- S) x y}"
-apply (auto intro: less_imp_le simp: not_outside_connected_component_lt [OF assms])
-by (meson gt_ex less_le_trans)
+  fixes S :: "'a::euclidean_space set"
+  assumes S: "bounded S"  "2 \<le> DIM('a)"
+  shows "- (outside S) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> \<not> connected_component (- S) x y}"
+  apply (auto intro: less_imp_le simp: not_outside_connected_component_lt [OF assms])
+  by (meson gt_ex less_le_trans)
 
 lemma inside_connected_component_lt:
     fixes S :: "'a::euclidean_space set"
@@ -3237,9 +3228,9 @@
 lemma inside_subset:
   assumes "connected U" and "\<not> bounded U" and "T \<union> U = - S"
   shows "inside S \<subseteq> T"
-apply (auto simp: inside_def)
-by (metis bounded_subset [of "connected_component_set (- S) _"] connected_component_maximal
-       Compl_iff Un_iff assms subsetI)
+  apply (auto simp: inside_def)
+  by (metis bounded_subset [of "connected_component_set (- S) _"] connected_component_maximal
+      Compl_iff Un_iff assms subsetI)
 
 lemma frontier_not_empty:
   fixes S :: "'a :: real_normed_vector set"
@@ -3384,10 +3375,9 @@
     assume x: "x \<in> interior s" and y: "y \<notin> s"
        and cc: "connected_component (- frontier s) x y"
     have "connected_component_set (- frontier s) x \<inter> frontier s \<noteq> {}"
-      apply (rule connected_Int_frontier, simp)
-      apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq rev_subsetD x)
-      using  y cc
-      by blast
+      apply (rule connected_Int_frontier; simp add: set_eq_iff)
+      apply (meson cc connected_component_in connected_component_refl_eq interior_subset subsetD x)
+      using y cc by blast
     then have "bounded (connected_component_set (- frontier s) x)"
       using connected_component_in by auto
   }
@@ -3402,29 +3392,29 @@
   by (simp add: inside_def)
 
 lemma outside_empty [simp]: "outside {} = (UNIV :: 'a :: {real_normed_vector, perfect_space} set)"
-using inside_empty inside_Un_outside by blast
+  using inside_empty inside_Un_outside by blast
 
 lemma inside_same_component:
-   "\<lbrakk>connected_component (- s) x y; x \<in> inside s\<rbrakk> \<Longrightarrow> y \<in> inside s"
+   "\<lbrakk>connected_component (- S) x y; x \<in> inside S\<rbrakk> \<Longrightarrow> y \<in> inside S"
   using connected_component_eq connected_component_in
   by (fastforce simp add: inside_def)
 
 lemma outside_same_component:
-   "\<lbrakk>connected_component (- s) x y; x \<in> outside s\<rbrakk> \<Longrightarrow> y \<in> outside s"
+   "\<lbrakk>connected_component (- S) x y; x \<in> outside S\<rbrakk> \<Longrightarrow> y \<in> outside S"
   using connected_component_eq connected_component_in
   by (fastforce simp add: outside_def)
 
 lemma convex_in_outside:
-  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
-  assumes s: "convex s" and z: "z \<notin> s"
-    shows "z \<in> outside s"
-proof (cases "s={}")
+  fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+  assumes S: "convex S" and z: "z \<notin> S"
+    shows "z \<in> outside S"
+proof (cases "S={}")
   case True then show ?thesis by simp
 next
-  case False then obtain a where "a \<in> s" by blast
+  case False then obtain a where "a \<in> S" by blast
   with z have zna: "z \<noteq> a" by auto
-  { assume "bounded (connected_component_set (- s) z)"
-    with bounded_pos_less obtain B where "B>0" and B: "\<And>x. connected_component (- s) z x \<Longrightarrow> norm x < B"
+  { assume "bounded (connected_component_set (- S) z)"
+    with bounded_pos_less obtain B where "B>0" and B: "\<And>x. connected_component (- S) z x \<Longrightarrow> norm x < B"
       by (metis mem_Collect_eq)
     define C where "C = (B + 1 + norm z) / norm (z-a)"
     have "C > 0"
@@ -3435,16 +3425,16 @@
       using zna \<open>B>0\<close> by (simp add: C_def le_max_iff_disj)
     ultimately have C: "norm (z + C *\<^sub>R (z-a)) > B" by linarith
     { fix u::real
-      assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> s"
+      assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> S"
       then have Cpos: "1 + u * C > 0"
         by (meson \<open>0 < C\<close> add_pos_nonneg less_eq_real_def zero_le_mult_iff zero_less_one)
       then have *: "(1 / (1 + u * C)) *\<^sub>R z + (u * C / (1 + u * C)) *\<^sub>R z = z"
         by (simp add: scaleR_add_left [symmetric] field_split_simps)
       then have False
-        using convexD_alt [OF s \<open>a \<in> s\<close> ins, of "1/(u*C + 1)"] \<open>C>0\<close> \<open>z \<notin> s\<close> Cpos u
+        using convexD_alt [OF S \<open>a \<in> S\<close> ins, of "1/(u*C + 1)"] \<open>C>0\<close> \<open>z \<notin> S\<close> Cpos u
         by (simp add: * field_split_simps)
     } note contra = this
-    have "connected_component (- s) z (z + C *\<^sub>R (z-a))"
+    have "connected_component (- S) z (z + C *\<^sub>R (z-a))"
       apply (rule connected_componentI [OF connected_segment [of z "z + C *\<^sub>R (z-a)"]])
       apply (simp add: closed_segment_def)
       using contra
@@ -3459,9 +3449,9 @@
 qed
 
 lemma outside_convex:
-  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
-  assumes "convex s"
-    shows "outside s = - s"
+  fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+  assumes "convex S"
+    shows "outside S = - S"
   by (metis ComplD assms convex_in_outside equalityI inside_Un_outside subsetI sup.cobounded2)
 
 lemma outside_singleton [simp]:
@@ -3470,8 +3460,8 @@
   by (auto simp: outside_convex)
 
 lemma inside_convex:
-  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
-  shows "convex s \<Longrightarrow> inside s = {}"
+  fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+  shows "convex S \<Longrightarrow> inside S = {}"
   by (simp add: inside_outside outside_convex)
 
 lemma inside_singleton [simp]:
@@ -3480,8 +3470,8 @@
   by (auto simp: inside_convex)
 
 lemma outside_subset_convex:
-  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
-  shows "\<lbrakk>convex t; s \<subseteq> t\<rbrakk> \<Longrightarrow> - t \<subseteq> outside s"
+  fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+  shows "\<lbrakk>convex T; S \<subseteq> T\<rbrakk> \<Longrightarrow> - T \<subseteq> outside S"
   using outside_convex outside_mono by blast
 
 lemma outside_Un_outside_Un:
@@ -3505,49 +3495,49 @@
 qed
 
 lemma outside_frontier_misses_closure:
-    fixes s :: "'a::real_normed_vector set"
-    assumes "bounded s"
-    shows  "outside(frontier s) \<subseteq> - closure s"
+    fixes S :: "'a::real_normed_vector set"
+    assumes "bounded S"
+    shows  "outside(frontier S) \<subseteq> - closure S"
   unfolding outside_inside Lattices.boolean_algebra_class.compl_le_compl_iff
 proof -
-  { assume "interior s \<subseteq> inside (frontier s)"
-    hence "interior s \<union> inside (frontier s) = inside (frontier s)"
+  { assume "interior S \<subseteq> inside (frontier S)"
+    hence "interior S \<union> inside (frontier S) = inside (frontier S)"
       by (simp add: subset_Un_eq)
-    then have "closure s \<subseteq> frontier s \<union> inside (frontier s)"
+    then have "closure S \<subseteq> frontier S \<union> inside (frontier S)"
       using frontier_def by auto
   }
-  then show "closure s \<subseteq> frontier s \<union> inside (frontier s)"
+  then show "closure S \<subseteq> frontier S \<union> inside (frontier S)"
     using interior_inside_frontier [OF assms] by blast
 qed
 
 lemma outside_frontier_eq_complement_closure:
-  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
-    assumes "bounded s" "convex s"
-      shows "outside(frontier s) = - closure s"
+  fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+    assumes "bounded S" "convex S"
+      shows "outside(frontier S) = - closure S"
 by (metis Diff_subset assms convex_closure frontier_def outside_frontier_misses_closure
           outside_subset_convex subset_antisym)
 
 lemma inside_frontier_eq_interior:
-     fixes s :: "'a :: {real_normed_vector, perfect_space} set"
-     shows "\<lbrakk>bounded s; convex s\<rbrakk> \<Longrightarrow> inside(frontier s) = interior s"
+     fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+     shows "\<lbrakk>bounded S; convex S\<rbrakk> \<Longrightarrow> inside(frontier S) = interior S"
   apply (simp add: inside_outside outside_frontier_eq_complement_closure)
   using closure_subset interior_subset
   apply (auto simp: frontier_def)
   done
 
 lemma open_inside:
-    fixes s :: "'a::real_normed_vector set"
-    assumes "closed s"
-      shows "open (inside s)"
+    fixes S :: "'a::real_normed_vector set"
+    assumes "closed S"
+      shows "open (inside S)"
 proof -
-  { fix x assume x: "x \<in> inside s"
-    have "open (connected_component_set (- s) x)"
+  { fix x assume x: "x \<in> inside S"
+    have "open (connected_component_set (- S) x)"
       using assms open_connected_component by blast
-    then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- s) x y"
+    then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- S) x y"
       using dist_not_less_zero
       apply (simp add: open_dist)
       by (metis (no_types, lifting) Compl_iff connected_component_refl_eq inside_def mem_Collect_eq x)
-    then have "\<exists>e>0. ball x e \<subseteq> inside s"
+    then have "\<exists>e>0. ball x e \<subseteq> inside S"
       by (metis e dist_commute inside_same_component mem_ball subsetI x)
   }
   then show ?thesis
@@ -3555,18 +3545,18 @@
 qed
 
 lemma open_outside:
-    fixes s :: "'a::real_normed_vector set"
-    assumes "closed s"
-      shows "open (outside s)"
+    fixes S :: "'a::real_normed_vector set"
+    assumes "closed S"
+      shows "open (outside S)"
 proof -
-  { fix x assume x: "x \<in> outside s"
-    have "open (connected_component_set (- s) x)"
+  { fix x assume x: "x \<in> outside S"
+    have "open (connected_component_set (- S) x)"
       using assms open_connected_component by blast
-    then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- s) x y"
+    then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- S) x y"
       using dist_not_less_zero
       apply (simp add: open_dist)
       by (metis Int_iff outside_def connected_component_refl_eq  x)
-    then have "\<exists>e>0. ball x e \<subseteq> outside s"
+    then have "\<exists>e>0. ball x e \<subseteq> outside S"
       by (metis e dist_commute outside_same_component mem_ball subsetI x)
   }
   then show ?thesis
@@ -3574,61 +3564,61 @@
 qed
 
 lemma closure_inside_subset:
-    fixes s :: "'a::real_normed_vector set"
-    assumes "closed s"
-      shows "closure(inside s) \<subseteq> s \<union> inside s"
+    fixes S :: "'a::real_normed_vector set"
+    assumes "closed S"
+      shows "closure(inside S) \<subseteq> S \<union> inside S"
 by (metis assms closure_minimal open_closed open_outside sup.cobounded2 union_with_inside)
 
 lemma frontier_inside_subset:
-    fixes s :: "'a::real_normed_vector set"
-    assumes "closed s"
-      shows "frontier(inside s) \<subseteq> s"
+    fixes S :: "'a::real_normed_vector set"
+    assumes "closed S"
+      shows "frontier(inside S) \<subseteq> S"
 proof -
-  have "closure (inside s) \<inter> - inside s = closure (inside s) - interior (inside s)"
+  have "closure (inside S) \<inter> - inside S = closure (inside S) - interior (inside S)"
     by (metis (no_types) Diff_Compl assms closure_closed interior_closure open_closed open_inside)
-  moreover have "- inside s \<inter> - outside s = s"
+  moreover have "- inside S \<inter> - outside S = S"
     by (metis (no_types) compl_sup double_compl inside_Un_outside)
-  moreover have "closure (inside s) \<subseteq> - outside s"
+  moreover have "closure (inside S) \<subseteq> - outside S"
     by (metis (no_types) assms closure_inside_subset union_with_inside)
-  ultimately have "closure (inside s) - interior (inside s) \<subseteq> s"
+  ultimately have "closure (inside S) - interior (inside S) \<subseteq> S"
     by blast
   then show ?thesis
     by (simp add: frontier_def open_inside interior_open)
 qed
 
 lemma closure_outside_subset:
-    fixes s :: "'a::real_normed_vector set"
-    assumes "closed s"
-      shows "closure(outside s) \<subseteq> s \<union> outside s"
+    fixes S :: "'a::real_normed_vector set"
+    assumes "closed S"
+      shows "closure(outside S) \<subseteq> S \<union> outside S"
   apply (rule closure_minimal, simp)
   by (metis assms closed_open inside_outside open_inside)
 
 lemma frontier_outside_subset:
-    fixes s :: "'a::real_normed_vector set"
-    assumes "closed s"
-      shows "frontier(outside s) \<subseteq> s"
+    fixes S :: "'a::real_normed_vector set"
+    assumes "closed S"
+      shows "frontier(outside S) \<subseteq> S"
   apply (simp add: frontier_def open_outside interior_open)
   by (metis Diff_subset_conv assms closure_outside_subset interior_eq open_outside sup.commute)
 
 lemma inside_complement_unbounded_connected_empty:
-     "\<lbrakk>connected (- s); \<not> bounded (- s)\<rbrakk> \<Longrightarrow> inside s = {}"
+     "\<lbrakk>connected (- S); \<not> bounded (- S)\<rbrakk> \<Longrightarrow> inside S = {}"
   apply (simp add: inside_def)
   by (meson Compl_iff bounded_subset connected_component_maximal order_refl)
 
 lemma inside_bounded_complement_connected_empty:
-    fixes s :: "'a::{real_normed_vector, perfect_space} set"
-    shows "\<lbrakk>connected (- s); bounded s\<rbrakk> \<Longrightarrow> inside s = {}"
+    fixes S :: "'a::{real_normed_vector, perfect_space} set"
+    shows "\<lbrakk>connected (- S); bounded S\<rbrakk> \<Longrightarrow> inside S = {}"
   by (metis inside_complement_unbounded_connected_empty cobounded_imp_unbounded)
 
 lemma inside_inside:
-    assumes "s \<subseteq> inside t"
-    shows "inside s - t \<subseteq> inside t"
+    assumes "S \<subseteq> inside T"
+    shows "inside S - T \<subseteq> inside T"
 unfolding inside_def
 proof clarify
   fix x
-  assume x: "x \<notin> t" "x \<notin> s" and bo: "bounded (connected_component_set (- s) x)"
-  show "bounded (connected_component_set (- t) x)"
-  proof (cases "s \<inter> connected_component_set (- t) x = {}")
+  assume x: "x \<notin> T" "x \<notin> S" and bo: "bounded (connected_component_set (- S) x)"
+  show "bounded (connected_component_set (- T) x)"
+  proof (cases "S \<inter> connected_component_set (- T) x = {}")
     case True show ?thesis
       apply (rule bounded_subset [OF bo])
       apply (rule connected_component_maximal)
@@ -3643,68 +3633,68 @@
   qed
 qed
 
-lemma inside_inside_subset: "inside(inside s) \<subseteq> s"
+lemma inside_inside_subset: "inside(inside S) \<subseteq> S"
   using inside_inside union_with_outside by fastforce
 
 lemma inside_outside_intersect_connected:
-      "\<lbrakk>connected t; inside s \<inter> t \<noteq> {}; outside s \<inter> t \<noteq> {}\<rbrakk> \<Longrightarrow> s \<inter> t \<noteq> {}"
+      "\<lbrakk>connected T; inside S \<inter> T \<noteq> {}; outside S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> S \<inter> T \<noteq> {}"
   apply (simp add: inside_def outside_def ex_in_conv [symmetric] disjoint_eq_subset_Compl, clarify)
   by (metis (no_types, hide_lams) Compl_anti_mono connected_component_eq connected_component_maximal contra_subsetD double_compl)
 
 lemma outside_bounded_nonempty:
-  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
-    assumes "bounded s" shows "outside s \<noteq> {}"
+  fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+    assumes "bounded S" shows "outside S \<noteq> {}"
   by (metis (no_types, lifting) Collect_empty_eq Collect_mem_eq Compl_eq_Diff_UNIV Diff_cancel
                    Diff_disjoint UNIV_I assms ball_eq_empty bounded_diff cobounded_outside convex_ball
                    double_complement order_refl outside_convex outside_def)
 
 lemma outside_compact_in_open:
-    fixes s :: "'a :: {real_normed_vector,perfect_space} set"
-    assumes s: "compact s" and t: "open t" and "s \<subseteq> t" "t \<noteq> {}"
-      shows "outside s \<inter> t \<noteq> {}"
+    fixes S :: "'a :: {real_normed_vector,perfect_space} set"
+    assumes S: "compact S" and T: "open T" and "S \<subseteq> T" "T \<noteq> {}"
+      shows "outside S \<inter> T \<noteq> {}"
 proof -
-  have "outside s \<noteq> {}"
-    by (simp add: compact_imp_bounded outside_bounded_nonempty s)
-  with assms obtain a b where a: "a \<in> outside s" and b: "b \<in> t" by auto
+  have "outside S \<noteq> {}"
+    by (simp add: compact_imp_bounded outside_bounded_nonempty S)
+  with assms obtain a b where a: "a \<in> outside S" and b: "b \<in> T" by auto
   show ?thesis
-  proof (cases "a \<in> t")
+  proof (cases "a \<in> T")
     case True with a show ?thesis by blast
   next
     case False
-      have front: "frontier t \<subseteq> - s"
-        using \<open>s \<subseteq> t\<close> frontier_disjoint_eq t by auto
+      have front: "frontier T \<subseteq> - S"
+        using \<open>S \<subseteq> T\<close> frontier_disjoint_eq T by auto
       { fix \<gamma>
-        assume "path \<gamma>" and pimg_sbs: "path_image \<gamma> - {pathfinish \<gamma>} \<subseteq> interior (- t)"
-           and pf: "pathfinish \<gamma> \<in> frontier t" and ps: "pathstart \<gamma> = a"
+        assume "path \<gamma>" and pimg_sbs: "path_image \<gamma> - {pathfinish \<gamma>} \<subseteq> interior (- T)"
+           and pf: "pathfinish \<gamma> \<in> frontier T" and ps: "pathstart \<gamma> = a"
         define c where "c = pathfinish \<gamma>"
-        have "c \<in> -s" unfolding c_def using front pf by blast
-        moreover have "open (-s)" using s compact_imp_closed by blast
-        ultimately obtain \<epsilon>::real where "\<epsilon> > 0" and \<epsilon>: "cball c \<epsilon> \<subseteq> -s"
-          using open_contains_cball[of "-s"] s by blast
-        then obtain d where "d \<in> t" and d: "dist d c < \<epsilon>"
-          using closure_approachable [of c t] pf unfolding c_def
+        have "c \<in> -S" unfolding c_def using front pf by blast
+        moreover have "open (-S)" using S compact_imp_closed by blast
+        ultimately obtain \<epsilon>::real where "\<epsilon> > 0" and \<epsilon>: "cball c \<epsilon> \<subseteq> -S"
+          using open_contains_cball[of "-S"] S by blast
+        then obtain d where "d \<in> T" and d: "dist d c < \<epsilon>"
+          using closure_approachable [of c T] pf unfolding c_def
           by (metis Diff_iff frontier_def)
-        then have "d \<in> -s" using \<epsilon>
+        then have "d \<in> -S" using \<epsilon>
           using dist_commute by (metis contra_subsetD mem_cball not_le not_less_iff_gr_or_eq)
-        have pimg_sbs_cos: "path_image \<gamma> \<subseteq> -s"
+        have pimg_sbs_cos: "path_image \<gamma> \<subseteq> -S"
           using pimg_sbs apply (auto simp: path_image_def)
           apply (drule subsetD)
-          using \<open>c \<in> - s\<close> \<open>s \<subseteq> t\<close> interior_subset apply (auto simp: c_def)
+          using \<open>c \<in> - S\<close> \<open>S \<subseteq> T\<close> interior_subset apply (auto simp: c_def)
           done
         have "closed_segment c d \<le> cball c \<epsilon>"
           apply (simp add: segment_convex_hull)
           apply (rule hull_minimal)
           using  \<open>\<epsilon> > 0\<close> d apply (auto simp: dist_commute)
           done
-        with \<epsilon> have "closed_segment c d \<subseteq> -s" by blast
+        with \<epsilon> have "closed_segment c d \<subseteq> -S" by blast
         moreover have con_gcd: "connected (path_image \<gamma> \<union> closed_segment c d)"
           by (rule connected_Un) (auto simp: c_def \<open>path \<gamma>\<close> connected_path_image)
-        ultimately have "connected_component (- s) a d"
+        ultimately have "connected_component (- S) a d"
           unfolding connected_component_def using pimg_sbs_cos ps by blast
-        then have "outside s \<inter> t \<noteq> {}"
-          using outside_same_component [OF _ a]  by (metis IntI \<open>d \<in> t\<close> empty_iff)
+        then have "outside S \<inter> T \<noteq> {}"
+          using outside_same_component [OF _ a]  by (metis IntI \<open>d \<in> T\<close> empty_iff)
       } note * = this
-      have pal: "pathstart (linepath a b) \<in> closure (- t)"
+      have pal: "pathstart (linepath a b) \<in> closure (- T)"
         by (auto simp: False closure_def)
       show ?thesis
         by (rule exists_path_subpath_to_frontier [OF path_linepath pal _ *]) (auto simp: b)
@@ -3712,10 +3702,10 @@
 qed
 
 lemma inside_inside_compact_connected:
-    fixes s :: "'a :: euclidean_space set"
-    assumes s: "closed s" and t: "compact t" and "connected t" "s \<subseteq> inside t"
-      shows "inside s \<subseteq> inside t"
-proof (cases "inside t = {}")
+    fixes S :: "'a :: euclidean_space set"
+    assumes S: "closed S" and T: "compact T" and "connected T" "S \<subseteq> inside T"
+      shows "inside S \<subseteq> inside T"
+proof (cases "inside T = {}")
   case True with assms show ?thesis by auto
 next
   case False
@@ -3727,120 +3717,120 @@
              using connected_convex_1_gen assms False inside_convex by blast
   next
     case 2
-    have coms: "compact s"
-      using assms apply (simp add: s compact_eq_bounded_closed)
+    have coms: "compact S"
+      using assms apply (simp add: S compact_eq_bounded_closed)
        by (meson bounded_inside bounded_subset compact_imp_bounded)
-    then have bst: "bounded (s \<union> t)"
-      by (simp add: compact_imp_bounded t)
-    then obtain r where "0 < r" and r: "s \<union> t \<subseteq> ball 0 r"
+    then have bst: "bounded (S \<union> T)"
+      by (simp add: compact_imp_bounded T)
+    then obtain r where "0 < r" and r: "S \<union> T \<subseteq> ball 0 r"
       using bounded_subset_ballD by blast
-    have outst: "outside s \<inter> outside t \<noteq> {}"
+    have outst: "outside S \<inter> outside T \<noteq> {}"
     proof -
-      have "- ball 0 r \<subseteq> outside s"
+      have "- ball 0 r \<subseteq> outside S"
         apply (rule outside_subset_convex)
         using r by auto
-      moreover have "- ball 0 r \<subseteq> outside t"
+      moreover have "- ball 0 r \<subseteq> outside T"
         apply (rule outside_subset_convex)
         using r by auto
       ultimately show ?thesis
         by (metis Compl_subset_Compl_iff Int_subset_iff bounded_ball inf.orderE outside_bounded_nonempty outside_no_overlap)
     qed
-    have "s \<inter> t = {}" using assms
+    have "S \<inter> T = {}" using assms
       by (metis disjoint_iff_not_equal inside_no_overlap subsetCE)
-    moreover have "outside s \<inter> inside t \<noteq> {}"
-      by (meson False assms(4) compact_eq_bounded_closed coms open_inside outside_compact_in_open t)
-    ultimately have "inside s \<inter> t = {}"
-      using inside_outside_intersect_connected [OF \<open>connected t\<close>, of s]
+    moreover have "outside S \<inter> inside T \<noteq> {}"
+      by (meson False assms(4) compact_eq_bounded_closed coms open_inside outside_compact_in_open T)
+    ultimately have "inside S \<inter> T = {}"
+      using inside_outside_intersect_connected [OF \<open>connected T\<close>, of S]
       by (metis "2" compact_eq_bounded_closed coms connected_outside inf.commute inside_outside_intersect_connected outst)
     then show ?thesis
-      using inside_inside [OF \<open>s \<subseteq> inside t\<close>] by blast
+      using inside_inside [OF \<open>S \<subseteq> inside T\<close>] by blast
   qed
 qed
 
 lemma connected_with_inside:
-    fixes s :: "'a :: real_normed_vector set"
-    assumes s: "closed s" and cons: "connected s"
-      shows "connected(s \<union> inside s)"
-proof (cases "s \<union> inside s = UNIV")
+    fixes S :: "'a :: real_normed_vector set"
+    assumes S: "closed S" and cons: "connected S"
+      shows "connected(S \<union> inside S)"
+proof (cases "S \<union> inside S = UNIV")
   case True with assms show ?thesis by auto
 next
   case False
-  then obtain b where b: "b \<notin> s" "b \<notin> inside s" by blast
-  have *: "\<exists>y t. y \<in> s \<and> connected t \<and> a \<in> t \<and> y \<in> t \<and> t \<subseteq> (s \<union> inside s)" if "a \<in> (s \<union> inside s)" for a
+  then obtain b where b: "b \<notin> S" "b \<notin> inside S" by blast
+  have *: "\<exists>y T. y \<in> S \<and> connected T \<and> a \<in> T \<and> y \<in> T \<and> T \<subseteq> (S \<union> inside S)" if "a \<in> (S \<union> inside S)" for a
   using that proof
-    assume "a \<in> s" then show ?thesis
+    assume "a \<in> S" then show ?thesis
       apply (rule_tac x=a in exI)
       apply (rule_tac x="{a}" in exI, simp)
       done
   next
-    assume a: "a \<in> inside s"
+    assume a: "a \<in> inside S"
     show ?thesis
-      apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "inside s"])
+      apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "inside S"])
       using a apply (simp add: closure_def)
       apply (simp add: b)
       apply (rule_tac x="pathfinish h" in exI)
       apply (rule_tac x="path_image h" in exI)
       apply (simp add: pathfinish_in_path_image connected_path_image, auto)
-      using frontier_inside_subset s apply fastforce
-      by (metis (no_types, lifting) frontier_inside_subset insertE insert_Diff interior_eq open_inside pathfinish_in_path_image s subsetCE)
+      using frontier_inside_subset S apply fastforce
+      by (metis (no_types, lifting) frontier_inside_subset insertE insert_Diff interior_eq open_inside pathfinish_in_path_image S subsetCE)
   qed
   show ?thesis
     apply (simp add: connected_iff_connected_component)
     apply (simp add: connected_component_def)
     apply (clarify dest!: *)
-    apply (rename_tac u u' t t')
-    apply (rule_tac x="(s \<union> t \<union> t')" in exI)
-    apply (auto simp: intro!: connected_Un cons)
+    apply (rename_tac u u' T t')
+    apply (rule_tac x="(S \<union> T \<union> t')" in exI)
+    apply (auto intro!: connected_Un cons)
     done
 qed
 
 text\<open>The proof is virtually the same as that above.\<close>
 lemma connected_with_outside:
-    fixes s :: "'a :: real_normed_vector set"
-    assumes s: "closed s" and cons: "connected s"
-      shows "connected(s \<union> outside s)"
-proof (cases "s \<union> outside s = UNIV")
+    fixes S :: "'a :: real_normed_vector set"
+    assumes S: "closed S" and cons: "connected S"
+      shows "connected(S \<union> outside S)"
+proof (cases "S \<union> outside S = UNIV")
   case True with assms show ?thesis by auto
 next
   case False
-  then obtain b where b: "b \<notin> s" "b \<notin> outside s" by blast
-  have *: "\<exists>y t. y \<in> s \<and> connected t \<and> a \<in> t \<and> y \<in> t \<and> t \<subseteq> (s \<union> outside s)" if "a \<in> (s \<union> outside s)" for a
+  then obtain b where b: "b \<notin> S" "b \<notin> outside S" by blast
+  have *: "\<exists>y T. y \<in> S \<and> connected T \<and> a \<in> T \<and> y \<in> T \<and> T \<subseteq> (S \<union> outside S)" if "a \<in> (S \<union> outside S)" for a
   using that proof
-    assume "a \<in> s" then show ?thesis
+    assume "a \<in> S" then show ?thesis
       apply (rule_tac x=a in exI)
       apply (rule_tac x="{a}" in exI, simp)
       done
   next
-    assume a: "a \<in> outside s"
+    assume a: "a \<in> outside S"
     show ?thesis
-      apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "outside s"])
+      apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "outside S"])
       using a apply (simp add: closure_def)
       apply (simp add: b)
       apply (rule_tac x="pathfinish h" in exI)
       apply (rule_tac x="path_image h" in exI)
       apply (simp add: pathfinish_in_path_image connected_path_image, auto)
-      using frontier_outside_subset s apply fastforce
-      by (metis (no_types, lifting) frontier_outside_subset insertE insert_Diff interior_eq open_outside pathfinish_in_path_image s subsetCE)
+      using frontier_outside_subset S apply fastforce
+      by (metis (no_types, lifting) frontier_outside_subset insertE insert_Diff interior_eq open_outside pathfinish_in_path_image S subsetCE)
   qed
   show ?thesis
     apply (simp add: connected_iff_connected_component)
     apply (simp add: connected_component_def)
     apply (clarify dest!: *)
-    apply (rename_tac u u' t t')
-    apply (rule_tac x="(s \<union> t \<union> t')" in exI)
+    apply (rename_tac u u' T t')
+    apply (rule_tac x="(S \<union> T \<union> t')" in exI)
     apply (auto simp: intro!: connected_Un cons)
     done
 qed
 
 lemma inside_inside_eq_empty [simp]:
-    fixes s :: "'a :: {real_normed_vector, perfect_space} set"
-    assumes s: "closed s" and cons: "connected s"
-      shows "inside (inside s) = {}"
+    fixes S :: "'a :: {real_normed_vector, perfect_space} set"
+    assumes S: "closed S" and cons: "connected S"
+      shows "inside (inside S) = {}"
   by (metis (no_types) unbounded_outside connected_with_outside [OF assms] bounded_Un
            inside_complement_unbounded_connected_empty unbounded_outside union_with_outside)
 
 lemma inside_in_components:
-     "inside s \<in> components (- s) \<longleftrightarrow> connected(inside s) \<and> inside s \<noteq> {}"
+     "inside S \<in> components (- S) \<longleftrightarrow> connected(inside S) \<and> inside S \<noteq> {}"
   apply (simp add: in_components_maximal)
   apply (auto intro: inside_same_component connected_componentI)
   apply (metis IntI empty_iff inside_no_overlap)
@@ -3848,15 +3838,15 @@
 
 text\<open>The proof is virtually the same as that above.\<close>
 lemma outside_in_components:
-     "outside s \<in> components (- s) \<longleftrightarrow> connected(outside s) \<and> outside s \<noteq> {}"
+     "outside S \<in> components (- S) \<longleftrightarrow> connected(outside S) \<and> outside S \<noteq> {}"
   apply (simp add: in_components_maximal)
   apply (auto intro: outside_same_component connected_componentI)
   apply (metis IntI empty_iff outside_no_overlap)
   done
 
 lemma bounded_unique_outside:
-    fixes s :: "'a :: euclidean_space set"
-    shows "\<lbrakk>bounded s; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- s) \<and> \<not> bounded c \<longleftrightarrow> c = outside s)"
+    fixes S :: "'a :: euclidean_space set"
+    shows "\<lbrakk>bounded S; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- S) \<and> \<not> bounded c \<longleftrightarrow> c = outside S)"
   apply (rule iffI)
   apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
   by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
@@ -3900,19 +3890,22 @@
       by (metis (no_types) Klim zKs y contf comp_assoc continuous_on_closure_sequentially)
     with fz have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
     have rle: "r \<le> norm (f y - f a)"
-      apply (rule le_no)
-      using w wy oint
-      by (force simp: imageI image_mono interiorI interior_subset frontier_def y)
+    proof (rule le_no)
+      show "y \<in> frontier S"
+        using w wy oint by (force simp: imageI image_mono interiorI interior_subset frontier_def y)
+    qed
     have **: "(b \<inter> (- S) \<noteq> {} \<and> b - (- S) \<noteq> {} \<Longrightarrow> b \<inter> f \<noteq> {})
-              \<Longrightarrow> (b \<inter> S \<noteq> {}) \<Longrightarrow> b \<inter> f = {} \<Longrightarrow>
-              b \<subseteq> S" for b f and S :: "'b set"
+              \<Longrightarrow> (b \<inter> S \<noteq> {}) \<Longrightarrow> b \<inter> f = {} \<Longrightarrow> b \<subseteq> S" 
+             for b f and S :: "'b set"
       by blast
+    have \<section>: "\<And>y. \<lbrakk>norm (f a - y) < r; y \<in> frontier (f ` S)\<rbrakk> \<Longrightarrow> False"
+      by (metis dw_le norm_minus_commute not_less order_trans rle wy)
     show ?thesis
       apply (rule **)   (*such a horrible mess*)
       apply (rule connected_Int_frontier [where t = "f`S", OF connected_ball])
       using \<open>a \<in> S\<close> \<open>0 < r\<close>
-      apply (auto simp: disjoint_iff_not_equal dist_norm)
-      by (metis dw_le norm_minus_commute not_less order_trans rle wy)
+         apply (auto simp: disjoint_iff_not_equal dist_norm dest: \<section>)
+      done
 qed
 
 
diff -r 0f3d24dc197f -r 0881bc2c607d src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Sun Aug 30 15:15:28 2020 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Sun Aug 30 21:21:04 2020 +0100
@@ -2823,14 +2823,11 @@
     by (auto simp: dist_real_def field_simps split: split_min)
   with \<open>x \<in> interior I\<close> e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
 
-  have "open (interior I)" by auto
-  from openE[OF this \<open>x \<in> interior I\<close>]
-  obtain e where "0 < e" "ball x e \<subseteq> interior I" .
-  moreover define K where "K = x - e / 2"
+  define K where "K = x - e / 2"
   with \<open>0 < e\<close> have "K \<in> ball x e" "K < x"
     by (auto simp: dist_real_def)
-  ultimately have "K \<in> I" "K < x" "x \<in> I"
-    using interior_subset[of I] \<open>x \<in> interior I\<close> by auto
+  then have "K \<in> I"
+    using \<open>interior I \<subseteq> I\<close> e(2) by blast
 
   have "Inf (?F x) \<le> (f x - f y) / (x - y)"
   proof (intro bdd_belowI cInf_lower2)
@@ -2870,11 +2867,8 @@
       by auto
     finally show "(f x - f y) / (x - y) \<le> z" .
   next
-    have "open (interior I)" by auto
-    from openE[OF this \<open>x \<in> interior I\<close>]
-    obtain e where e: "0 < e" "ball x e \<subseteq> interior I" .
-    then have "x + e / 2 \<in> ball x e"
-      by (auto simp: dist_real_def)
+    have "x + e / 2 \<in> ball x e"
+      using e by (auto simp: dist_real_def)
     with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I"
       by auto
     then show "?F x \<noteq> {}"
@@ -2897,58 +2891,59 @@
 qed
 
 lemma affine_independent_convex_affine_hull:
-  fixes s :: "'a::euclidean_space set"
-  assumes "\<not> affine_dependent s" "t \<subseteq> s"
-    shows "convex hull t = affine hull t \<inter> convex hull s"
+  fixes S :: "'a::euclidean_space set"
+  assumes "\<not> affine_dependent S" "T \<subseteq> S"
+    shows "convex hull T = affine hull T \<inter> convex hull S"
 proof -
-  have fin: "finite s" "finite t" using assms aff_independent_finite finite_subset by auto
+  have fin: "finite S" "finite T" using assms aff_independent_finite finite_subset by auto
     { fix u v x
-      assume uv: "sum u t = 1" "\<forall>x\<in>s. 0 \<le> v x" "sum v s = 1"
-                 "(\<Sum>x\<in>s. v x *\<^sub>R x) = (\<Sum>v\<in>t. u v *\<^sub>R v)" "x \<in> t"
-      then have s: "s = (s - t) \<union> t" \<comment> \<open>split into separate cases\<close>
+      assume uv: "sum u T = 1" "\<forall>x\<in>S. 0 \<le> v x" "sum v S = 1"
+                 "(\<Sum>x\<in>S. v x *\<^sub>R x) = (\<Sum>v\<in>T. u v *\<^sub>R v)" "x \<in> T"
+      then have S: "S = (S - T) \<union> T" \<comment> \<open>split into separate cases\<close>
         using assms by auto
-      have [simp]: "(\<Sum>x\<in>t. v x *\<^sub>R x) + (\<Sum>x\<in>s - t. v x *\<^sub>R x) = (\<Sum>x\<in>t. u x *\<^sub>R x)"
-                   "sum v t + sum v (s - t) = 1"
-        using uv fin s
+      have [simp]: "(\<Sum>x\<in>T. v x *\<^sub>R x) + (\<Sum>x\<in>S - T. v x *\<^sub>R x) = (\<Sum>x\<in>T. u x *\<^sub>R x)"
+                   "sum v T + sum v (S - T) = 1"
+        using uv fin S
         by (auto simp: sum.union_disjoint [symmetric] Un_commute)
-      have "(\<Sum>x\<in>s. if x \<in> t then v x - u x else v x) = 0"
-           "(\<Sum>x\<in>s. (if x \<in> t then v x - u x else v x) *\<^sub>R x) = 0"
+      have "(\<Sum>x\<in>S. if x \<in> T then v x - u x else v x) = 0"
+           "(\<Sum>x\<in>S. (if x \<in> T then v x - u x else v x) *\<^sub>R x) = 0"
         using uv fin
-        by (subst s, subst sum.union_disjoint, auto simp: algebra_simps sum_subtractf)+
+        by (subst S, subst sum.union_disjoint, auto simp: algebra_simps sum_subtractf)+
     } note [simp] = this
-  have "convex hull t \<subseteq> affine hull t"
+  have "convex hull T \<subseteq> affine hull T"
     using convex_hull_subset_affine_hull by blast
-  moreover have "convex hull t \<subseteq> convex hull s"
+  moreover have "convex hull T \<subseteq> convex hull S"
     using assms hull_mono by blast
-  moreover have "affine hull t \<inter> convex hull s \<subseteq> convex hull t"
-    using assms
-    apply (simp add: convex_hull_finite affine_hull_finite fin affine_dependent_explicit)
-    apply (drule_tac x=s in spec)
-    apply (auto simp: fin)
-    apply (rule_tac x=u in exI)
-    apply (rename_tac v)
-    apply (drule_tac x="\<lambda>x. if x \<in> t then v x - u x else v x" in spec)
-    apply (force)+
-    done
+  moreover have "affine hull T \<inter> convex hull S \<subseteq> convex hull T"
+  proof -
+    have 0: "\<And>u. sum u S = 0 \<Longrightarrow> (\<forall>v\<in>S. u v = 0) \<or> (\<Sum>v\<in>S. u v *\<^sub>R v) \<noteq> 0"
+      using affine_dependent_explicit_finite assms(1) fin(1) by auto
+    show ?thesis
+      apply (clarsimp simp add: convex_hull_finite affine_hull_finite fin )
+      apply (rule_tac x=u in exI)
+      subgoal for u v
+        using 0 [of "\<lambda>x. if x \<in> T then v x - u x else v x"] \<open>T \<subseteq> S\<close> by force
+      done
+  qed
   ultimately show ?thesis
     by blast
 qed
 
 lemma affine_independent_span_eq:
-  fixes s :: "'a::euclidean_space set"
-  assumes "\<not> affine_dependent s" "card s = Suc (DIM ('a))"
-    shows "affine hull s = UNIV"
-proof (cases "s = {}")
+  fixes S :: "'a::euclidean_space set"
+  assumes "\<not> affine_dependent S" "card S = Suc (DIM ('a))"
+    shows "affine hull S = UNIV"
+proof (cases "S = {}")
   case True then show ?thesis
     using assms by simp
 next
   case False
-    then obtain a t where t: "a \<notin> t" "s = insert a t"
+    then obtain a T where T: "a \<notin> T" "S = insert a T"
       by blast
-    then have fin: "finite t" using assms
+    then have fin: "finite T" using assms
       by (metis finite_insert aff_independent_finite)
     show ?thesis
-    using assms t fin
+    using assms T fin
       apply (simp add: affine_dependent_iff_dependent affine_hull_insert_span_gen)
       apply (rule subset_antisym)
       apply force
@@ -2960,9 +2955,9 @@
 qed
 
 lemma affine_independent_span_gt:
-  fixes s :: "'a::euclidean_space set"
-  assumes ind: "\<not> affine_dependent s" and dim: "DIM ('a) < card s"
-    shows "affine hull s = UNIV"
+  fixes S :: "'a::euclidean_space set"
+  assumes ind: "\<not> affine_dependent S" and dim: "DIM ('a) < card S"
+    shows "affine hull S = UNIV"
   apply (rule affine_independent_span_eq [OF ind])
   apply (rule antisym)
   using assms
@@ -2971,35 +2966,35 @@
   done
 
 lemma empty_interior_affine_hull:
-  fixes s :: "'a::euclidean_space set"
-  assumes "finite s" and dim: "card s \<le> DIM ('a)"
-    shows "interior(affine hull s) = {}"
+  fixes S :: "'a::euclidean_space set"
+  assumes "finite S" and dim: "card S \<le> DIM ('a)"
+    shows "interior(affine hull S) = {}"
   using assms
-  apply (induct s rule: finite_induct)
+  apply (induct S rule: finite_induct)
   apply (simp_all add:  affine_dependent_iff_dependent affine_hull_insert_span_gen interior_translation)
   apply (rule empty_interior_lowdim)
   by (auto simp: Suc_le_lessD card_image_le dual_order.trans intro!: dim_le_card'[THEN le_less_trans])
 
 lemma empty_interior_convex_hull:
-  fixes s :: "'a::euclidean_space set"
-  assumes "finite s" and dim: "card s \<le> DIM ('a)"
-    shows "interior(convex hull s) = {}"
+  fixes S :: "'a::euclidean_space set"
+  assumes "finite S" and dim: "card S \<le> DIM ('a)"
+    shows "interior(convex hull S) = {}"
   by (metis Diff_empty Diff_eq_empty_iff convex_hull_subset_affine_hull
             interior_mono empty_interior_affine_hull [OF assms])
 
 lemma explicit_subset_rel_interior_convex_hull:
-  fixes s :: "'a::euclidean_space set"
-  shows "finite s
-         \<Longrightarrow> {y. \<exists>u. (\<forall>x \<in> s. 0 < u x \<and> u x < 1) \<and> sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}
-             \<subseteq> rel_interior (convex hull s)"
-  by (force simp add:  rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=s, simplified])
+  fixes S :: "'a::euclidean_space set"
+  shows "finite S
+         \<Longrightarrow> {y. \<exists>u. (\<forall>x \<in> S. 0 < u x \<and> u x < 1) \<and> sum u S = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y}
+             \<subseteq> rel_interior (convex hull S)"
+  by (force simp add:  rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=S, simplified])
 
 lemma explicit_subset_rel_interior_convex_hull_minimal:
-  fixes s :: "'a::euclidean_space set"
-  shows "finite s
-         \<Longrightarrow> {y. \<exists>u. (\<forall>x \<in> s. 0 < u x) \<and> sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}
-             \<subseteq> rel_interior (convex hull s)"
-  by (force simp add:  rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=s, simplified])
+  fixes S :: "'a::euclidean_space set"
+  shows "finite S
+         \<Longrightarrow> {y. \<exists>u. (\<forall>x \<in> S. 0 < u x) \<and> sum u S = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y}
+             \<subseteq> rel_interior (convex hull S)"
+  by (force simp add:  rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=S, simplified])
 
 lemma rel_interior_convex_hull_explicit:
   fixes s :: "'a::euclidean_space set"
diff -r 0f3d24dc197f -r 0881bc2c607d src/HOL/Complex_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Sun Aug 30 15:15:28 2020 +0000
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Sun Aug 30 21:21:04 2020 +0100
@@ -1024,12 +1024,9 @@
         by (meson open_ball centre_in_ball)
       define U where "U = (\<lambda>w. (w - \<xi>) * g w) ` T"
       have "open U" by (metis oimT U_def)
-      have "0 \<in> U"
-        apply (auto simp: U_def)
-        apply (rule image_eqI [where x = \<xi>])
-        apply (auto simp: \<open>\<xi> \<in> T\<close>)
-        done
-      then obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "cball 0 \<epsilon> \<subseteq> U"
+      moreover have "0 \<in> U"
+        using \<open>\<xi> \<in> T\<close> by (auto simp: U_def intro: image_eqI [where x = \<xi>])
+      ultimately obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "cball 0 \<epsilon> \<subseteq> U"
         using \<open>open U\<close> open_contains_cball by blast
       then have "\<epsilon> * exp(2 * of_real pi * \<i> * (0/n)) \<in> cball 0 \<epsilon>"
                 "\<epsilon> * exp(2 * of_real pi * \<i> * (1/n)) \<in> cball 0 \<epsilon>"