# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1524427514 -3600
# Node ID c8a506be83bd230ea4fef6d505540b792426144d
# Parent  b91a043c0dcbfa726f36234e50e22f52c5498f8d
Tidied a lot of messy proofs

diff -r b91a043c0dcb -r c8a506be83bd src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sat Apr 21 11:13:35 2018 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Apr 22 21:05:14 2018 +0100
@@ -2,9 +2,6 @@
     Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light) and LCP
 *)
 
-(* ========================================================================= *)
-(* Results connected with topological dimension.                             *)
-(*                                                                           *)
 (* At the moment this is just Brouwer's fixpoint theorem. The proof is from  *)
 (* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518   *)
 (* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf".          *)
@@ -14,7 +11,6 @@
 (* the big advantage of Kuhn's proof over the usual Sperner's lemma one.     *)
 (*                                                                           *)
 (*              (c) Copyright, John Harrison 1998-2008                       *)
-(* ========================================================================= *)
 
 section \<open>Results connected with topological dimension\<close>
 
@@ -40,11 +36,7 @@
 lemma swap_image:
   "Fun.swap i j f ` A = (if i \<in> A then (if j \<in> A then f ` A else f ` ((A - {i}) \<union> {j}))
                                   else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
-  apply (auto simp: Fun.swap_def image_iff)
-  apply metis
-  apply (metis member_remove remove_def)
-  apply (metis member_remove remove_def)
-  done
+  by (auto simp: swap_def image_def) metis
 
 lemmas swap_apply1 = swap_apply(1)
 lemmas swap_apply2 = swap_apply(2)
@@ -191,9 +183,9 @@
     moreover obtain a where "rl a = Suc n" "a \<in> s"
       by (metis atMost_iff image_iff le_Suc_eq rl)
     ultimately have n: "{..n} = rl ` (s - {a})"
-      by (auto simp add: inj_on_image_set_diff Diff_subset rl)
+      by (auto simp: inj_on_image_set_diff Diff_subset rl)
     have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a}"
-      using inj_rl \<open>a \<in> s\<close> by (auto simp add: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
+      using inj_rl \<open>a \<in> s\<close> by (auto simp: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
     then show "card ?S = 1"
       unfolding card_S by simp }
 
@@ -202,7 +194,7 @@
     proof cases
       assume *: "{..n} \<subseteq> rl ` s"
       with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
-        by (auto simp add: atMost_Suc subset_insert_iff split: if_split_asm)
+        by (auto simp: atMost_Suc subset_insert_iff split: if_split_asm)
       then have "\<not> inj_on rl s"
         by (intro pigeonhole) simp
       then obtain a b where ab: "a \<in> s" "b \<in> s" "rl a = rl b" "a \<noteq> b"
@@ -210,7 +202,7 @@
       then have eq: "rl ` (s - {a}) = rl ` s"
         by auto
       with ab have inj: "inj_on rl (s - {a})"
-        by (intro eq_card_imp_inj_on) (auto simp add: rl_s card_Diff_singleton_if)
+        by (intro eq_card_imp_inj_on) (auto simp: rl_s card_Diff_singleton_if)
 
       { fix x assume "x \<in> s" "x \<notin> {a, b}"
         then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
@@ -275,7 +267,7 @@
     with upd have "upd ` {..< x} \<noteq> upd ` {..< y}"
       by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def)
     then have "enum x \<noteq> enum y"
-      by (auto simp add: enum_def fun_eq_iff) }
+      by (auto simp: enum_def fun_eq_iff) }
   then show ?thesis
     by (auto simp: inj_on_def)
 qed
@@ -325,7 +317,7 @@
   by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])
 
 lemma enum_strict_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i < enum j \<longleftrightarrow> i < j"
-  using enum_mono[of i j] enum_inj[of i j] by (auto simp add: le_less)
+  using enum_mono[of i j] enum_inj[of i j] by (auto simp: le_less)
 
 lemma chain: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a \<le> b \<or> b \<le> a"
   by (auto simp: s_eq enum_mono)
@@ -346,7 +338,7 @@
   by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric])
 
 lemma out_eq_p: "a \<in> s \<Longrightarrow> n \<le> j \<Longrightarrow> a j = p"
-  unfolding s_eq by (auto simp add: enum_eq_p)
+  unfolding s_eq by (auto simp: enum_eq_p)
 
 lemma s_le_p: "a \<in> s \<Longrightarrow> a j \<le> p"
   using out_eq_p[of a j] s_space by (cases "j < n") auto
@@ -578,7 +570,7 @@
         by (auto simp: image_iff Ball_def) arith
       then have upd_Suc: "\<And>i. i \<le> n \<Longrightarrow> (upd\<circ>Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
         using \<open>upd 0 = n\<close> upd_inj
-        by (auto simp add: image_comp[symmetric] inj_on_image_set_diff[OF inj_upd])
+        by (auto simp: image_comp[symmetric] inj_on_image_set_diff[OF inj_upd])
       have n_in_upd: "\<And>i. n \<in> upd ` {..< Suc i}"
         using \<open>upd 0 = n\<close> by auto
 
@@ -685,7 +677,7 @@
 qed
 
 lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y))"
-  by (auto simp add: card_Suc_eq eval_nat_numeral)
+  by (auto simp: card_Suc_eq eval_nat_numeral)
 
 lemma ksimplex_replace_2:
   assumes s: "ksimplex p n s" and "a \<in> s" and "n \<noteq> 0"
@@ -723,11 +715,11 @@
       obtain i' where "i' \<le> n" "enum i' \<noteq> enum 0" "enum i' (upd 0) \<noteq> p"
         unfolding s_eq by (auto intro: upd_space simp: enum_inj)
       then have "enum 1 \<le> enum i'" "enum i' (upd 0) < p"
-        using enum_le_p[of i' "upd 0"] by (auto simp add: enum_inj enum_mono upd_space)
+        using enum_le_p[of i' "upd 0"] by (auto simp: enum_inj enum_mono upd_space)
       then have "enum 1 (upd 0) < p"
-        by (auto simp add: le_fun_def intro: le_less_trans)
+        by (auto simp: le_fun_def intro: le_less_trans)
       then show "enum (Suc 0) \<in> {..<n} \<rightarrow> {..<p}"
-        using base \<open>n \<noteq> 0\<close> by (auto simp add: enum_0 enum_Suc PiE_iff extensional_def upd_space)
+        using base \<open>n \<noteq> 0\<close> by (auto simp: enum_0 enum_Suc PiE_iff extensional_def upd_space)
 
       { fix i assume "n \<le> i" then show "enum (Suc 0) i = p"
         using \<open>n \<noteq> 0\<close> by (auto simp: enum_eq_p) }
@@ -745,7 +737,7 @@
 
     { fix j assume j: "j < n"
       from j \<open>n \<noteq> 0\<close> have "f' j = enum (Suc j)"
-        by (auto simp add: f'_def enum_def upd_inj in_upd_image image_comp[symmetric] fun_eq_iff) }
+        by (auto simp: f'_def enum_def upd_inj in_upd_image image_comp[symmetric] fun_eq_iff) }
     note f'_eq_enum = this
     then have "enum ` Suc ` {..< n} = f' ` {..< n}"
       by (force simp: enum_inj)
@@ -859,10 +851,10 @@
       by (simp_all add: rot_def)
 
     { fix j assume j: "Suc j \<le> n" then have "b.enum (Suc j) = enum j"
-        by (induct j) (auto simp add: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
+        by (induct j) (auto simp: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
     note b_enum_eq_enum = this
     then have "enum ` {..< n} = b.enum ` Suc ` {..< n}"
-      by (auto simp add: image_comp intro!: image_cong)
+      by (auto simp: image_comp intro!: image_cong)
     also have "Suc ` {..< n} = {.. n} - {0}"
       by (auto simp: image_iff Ball_def) arith
     also have "{..< n} = {.. n} - {n}"
@@ -871,7 +863,7 @@
       unfolding s_eq \<open>a = enum i\<close> \<open>i = n\<close>
       using inj_on_image_set_diff[OF inj_enum Diff_subset, of "{n}"]
             inj_on_image_set_diff[OF b.inj_enum Diff_subset, of "{0}"]
-      by (simp add: comp_def )
+      by (simp add: comp_def)
 
     have "b.enum 0 \<le> b.enum n"
       by (simp add: b.enum_mono)
@@ -956,7 +948,7 @@
       moreover note i
       ultimately have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
         unfolding enum_def[abs_def] b.enum_def[abs_def]
-        by (auto simp add: fun_eq_iff swap_image i'_def
+        by (auto simp: fun_eq_iff swap_image i'_def
                            in_upd_image inj_on_image_set_diff[OF inj_upd]) }
     note enum_eq_benum = this
     then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
@@ -1001,7 +993,7 @@
         then obtain j where "t.enum (Suc l) = enum j" "j \<le> n" "enum j \<noteq> enum i"
           unfolding s_eq \<open>a = enum i\<close> by auto
         with i have "t.enum (Suc l) \<le> t.enum l \<or> t.enum k \<le> t.enum (Suc l)"
-          by (auto simp add: i'_def enum_mono enum_inj l k)
+          by (auto simp: i'_def enum_mono enum_inj l k)
         with \<open>Suc l < k\<close> \<open>k \<le> n\<close> show False
           by (simp add: t.enum_mono)
       qed
@@ -1041,7 +1033,7 @@
         assume u: "u l = upd (Suc i')"
         define B where "B = b.enum ` {..n}"
         have "b.enum i' = enum i'"
-          using enum_eq_benum[of i'] i by (auto simp add: i'_def gr0_conv_Suc)
+          using enum_eq_benum[of i'] i by (auto simp: i'_def gr0_conv_Suc)
         have "c = t.enum (Suc l)" unfolding c_eq ..
         also have "t.enum (Suc l) = b.enum (Suc i')"
           using u \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
@@ -1432,7 +1424,7 @@
 proof (rule ccontr)
   define n where "n = DIM('a)"
   have n: "1 \<le> n" "0 < n" "n \<noteq> 0"
-    unfolding n_def by (auto simp add: Suc_le_eq DIM_positive)
+    unfolding n_def by (auto simp: Suc_le_eq DIM_positive)
   assume "\<not> ?thesis"
   then have *: "\<not> (\<exists>x\<in>unit_cube. f x - x = 0)"
     by auto
@@ -1447,73 +1439,45 @@
     using assms(2)[unfolded image_subset_iff Ball_def]
     unfolding mem_unit_cube
     by auto
-  obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
+  obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where label [rule_format]:
     "\<forall>x. \<forall>i\<in>Basis. label x i \<le> 1"
-    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
-    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
-    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
-    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
-    using kuhn_labelling_lemma[OF *] by blast
+    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
+    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
+    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
+    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
+    using kuhn_labelling_lemma[OF *] by auto
   note label = this [rule_format]
   have lem1: "\<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
     \<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
   proof safe
     fix x y :: 'a
-    assume x: "x \<in> unit_cube"
-    assume y: "y \<in> unit_cube"
+    assume x: "x \<in> unit_cube" and y: "y \<in> unit_cube"
     fix i
     assume i: "label x i \<noteq> label y i" "i \<in> Basis"
     have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
       \<bar>fx - x\<bar> \<le> \<bar>fy - fx\<bar> + \<bar>y - x\<bar>" by auto
     have "\<bar>(f x - x) \<bullet> i\<bar> \<le> \<bar>(f y - f x)\<bullet>i\<bar> + \<bar>(y - x)\<bullet>i\<bar>"
-      unfolding inner_simps
-      apply (rule *)
-      apply (cases "label x i = 0")
-      apply (rule disjI1)
-      apply rule
-      prefer 3
-      apply (rule disjI2)
-      apply rule
-    proof -
-      assume lx: "label x i = 0"
-      then have ly: "label y i = 1"
-        using i label(1)[of i y]
-        by auto
-      show "x \<bullet> i \<le> f x \<bullet> i"
-        apply (rule label(4)[rule_format])
-        using x y lx i(2)
-        apply auto
-        done
-      show "f y \<bullet> i \<le> y \<bullet> i"
-        apply (rule label(5)[rule_format])
-        using x y ly i(2)
-        apply auto
-        done
+    proof (cases "label x i = 0")
+      case True
+      then have fxy: "\<not> f y \<bullet> i \<le> y \<bullet> i \<Longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
+        by (metis True i label(1) label(5) le_antisym less_one not_le_imp_less y)
+      show ?thesis
+      unfolding inner_simps         
+      by (rule *) (auto simp: True i label x y fxy)
     next
-      assume "label x i \<noteq> 0"
-      then have l: "label x i = 1" "label y i = 0"
-        using i label(1)[of i x] label(1)[of i y]
-        by auto
-      show "f x \<bullet> i \<le> x \<bullet> i"
-        apply (rule label(5)[rule_format])
-        using x y l i(2)
-        apply auto
-        done
-      show "y \<bullet> i \<le> f y \<bullet> i"
-        apply (rule label(4)[rule_format])
-        using x y l i(2)
-        apply auto
-        done
+      case False
+      then show ?thesis
+        using label [OF \<open>i \<in> Basis\<close>] i(1) x y
+        apply (auto simp: inner_diff_left le_Suc_eq)
+        by (metis "*")
     qed
     also have "\<dots> \<le> norm (f y - f x) + norm (y - x)"
-      apply (rule add_mono)
-      apply (rule Basis_le_norm[OF i(2)])+
-      done
+      by (simp add: add_mono i(2) norm_bound_Basis_le)
     finally show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
       unfolding inner_simps .
   qed
   have "\<exists>e>0. \<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>z\<in>unit_cube. \<forall>i\<in>Basis.
-    norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow>
+    norm (x - z) < e \<longrightarrow> norm (y - z) < e \<longrightarrow> label x i \<noteq> label y i \<longrightarrow>
       \<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
   proof -
     have d': "d / real n / 8 > 0"
@@ -1530,9 +1494,7 @@
       unfolding dist_norm
       by blast
     show ?thesis
-      apply (rule_tac x="min (e/2) (d/real n/8)" in exI)
-      apply safe
-    proof -
+    proof (intro exI conjI ballI impI)
       show "0 < min (e / 2) (d / real n / 8)"
         using d' e by auto
       fix x y z i
@@ -1551,10 +1513,9 @@
         unfolding inner_simps
       proof (rule *)
         show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y -f x) + norm (y - x)"
-          apply (rule lem1[rule_format])
-          using as i
-          apply auto
-          done
+          using as(1) as(2) as(6) i lem1 by blast
+        show "norm (f x - f z) < d / real n / 8"
+          using d' e as by auto
         show "\<bar>f x \<bullet> i - f z \<bullet> i\<bar> \<le> norm (f x - f z)" "\<bar>x \<bullet> i - z \<bullet> i\<bar> \<le> norm (x - z)"
           unfolding inner_diff_left[symmetric]
           by (rule Basis_le_norm[OF i])+
@@ -1563,30 +1524,14 @@
           unfolding norm_minus_commute
           by auto
         also have "\<dots> < e / 2 + e / 2"
-          apply (rule add_strict_mono)
-          using as(4,5)
-          apply auto
-          done
+          using as(4) as(5) by auto
         finally show "norm (f y - f x) < d / real n / 8"
-          apply -
-          apply (rule e(2))
-          using as
-          apply auto
-          done
+          using as(1) as(2) e(2) by auto
         have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8"
-          apply (rule add_strict_mono)
-          using as
-          apply auto
-          done
-        then show "norm (y - x) < 2 * (d / real n / 8)"
-          using tria
+          using as(4) as(5) by auto
+        with tria show "norm (y - x) < 2 * (d / real n / 8)"
           by auto
-        show "norm (f x - f z) < d / real n / 8"
-          apply (rule e(2))
-          using as e(1)
-          apply auto
-          done
-      qed (insert as, auto)
+      qed (use as in auto)
     qed
   qed
   then
@@ -1635,14 +1580,14 @@
   { fix x :: "nat \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
     then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (unit_cube::'a set)"
       using b'_Basis
-      by (auto simp add: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
+      by (auto simp: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
   note cube = this
   have q2: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
       (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
-    unfolding o_def using cube \<open>p > 0\<close> by (intro allI impI label(2)) (auto simp add: b'')
+    unfolding o_def using cube \<open>p > 0\<close> by (intro allI impI label(2)) (auto simp: b'')
   have q3: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow>
       (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
-    using cube \<open>p > 0\<close> unfolding o_def by (intro allI impI label(3)) (auto simp add: b'')
+    using cube \<open>p > 0\<close> unfolding o_def by (intro allI impI label(3)) (auto simp: b'')
   obtain q where q:
       "\<forall>i<n. q i < p"
       "\<forall>i<n.
@@ -1660,24 +1605,20 @@
     then have "z \<in> unit_cube"
       unfolding z_def mem_unit_cube
       using b'_Basis
-      by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
+      by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
     then have d_fz_z: "d \<le> norm (f z - z)"
       by (rule d)
     assume "\<not> ?thesis"
     then have as: "\<forall>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar> < d / real n"
       using \<open>n > 0\<close>
-      by (auto simp add: not_le inner_diff)
+      by (auto simp: not_le inner_diff)
     have "norm (f z - z) \<le> (\<Sum>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar>)"
       unfolding inner_diff_left[symmetric]
       by (rule norm_le_l1)
     also have "\<dots> < (\<Sum>(i::'a) \<in> Basis. d / real n)"
-      apply (rule sum_strict_mono)
-      using as
-      apply auto
-      done
+      by (meson as finite_Basis nonempty_Basis sum_strict_mono)
     also have "\<dots> = d"
-      using DIM_positive[where 'a='a]
-      by (auto simp: n_def)
+      using DIM_positive[where 'a='a] by (auto simp: n_def)
     finally show False
       using d_fz_z by auto
   qed
@@ -1698,50 +1639,37 @@
     apply (rule order_trans)
     apply (rule rs(1)[OF b'_im,THEN conjunct2])
     using q(1)[rule_format,OF b'_im]
-    apply (auto simp add: Suc_le_eq)
+    apply (auto simp: Suc_le_eq)
     done
   then have "r' \<in> unit_cube"
     unfolding r'_def mem_unit_cube
     using b'_Basis
-    by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
+    by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   define s' :: 'a where "s' = (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)"
   have "\<And>i. i \<in> Basis \<Longrightarrow> s (b' i) \<le> p"
-    apply (rule order_trans)
-    apply (rule rs(2)[OF b'_im, THEN conjunct2])
-    using q(1)[rule_format,OF b'_im]
-    apply (auto simp add: Suc_le_eq)
-    done
+    using b'_im q(1) rs(2) by fastforce
   then have "s' \<in> unit_cube"
     unfolding s'_def mem_unit_cube
-    using b'_Basis
-    by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
+    using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   have "z \<in> unit_cube"
     unfolding z_def mem_unit_cube
     using b'_Basis q(1)[rule_format,OF b'_im] \<open>p > 0\<close>
-    by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
-  have *: "\<And>x. 1 + real x = real (Suc x)"
-    by auto
+    by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
   {
     have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
-      apply (rule sum_mono)
-      using rs(1)[OF b'_im]
-      apply (auto simp add:* field_simps simp del: of_nat_Suc)
-      done
+      by (rule sum_mono) (use rs(1)[OF b'_im] in force)
     also have "\<dots> < e * real p"
       using p \<open>e > 0\<close> \<open>p > 0\<close>
-      by (auto simp add: field_simps n_def)
+      by (auto simp: field_simps n_def)
     finally have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) < e * real p" .
   }
   moreover
   {
     have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
-      apply (rule sum_mono)
-      using rs(2)[OF b'_im]
-      apply (auto simp add:* field_simps simp del: of_nat_Suc)
-      done
+      by (rule sum_mono) (use rs(2)[OF b'_im] in force)
     also have "\<dots> < e * real p"
       using p \<open>e > 0\<close> \<open>p > 0\<close>
-      by (auto simp add: field_simps n_def)
+      by (auto simp: field_simps n_def)
     finally have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) < e * real p" .
   }
   ultimately
@@ -1749,7 +1677,7 @@
     unfolding r'_def s'_def z_def
     using \<open>p > 0\<close>
     apply (rule_tac[!] le_less_trans[OF norm_le_l1])
-    apply (auto simp add: field_simps sum_divide_distrib[symmetric] inner_diff_left)
+    apply (auto simp: field_simps sum_divide_distrib[symmetric] inner_diff_left)
     done
   then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
     using rs(3) i
@@ -1762,121 +1690,100 @@
 
 subsection \<open>Retractions\<close>
 
-definition "retraction s t r \<longleftrightarrow> t \<subseteq> s \<and> continuous_on s r \<and> r ` s \<subseteq> t \<and> (\<forall>x\<in>t. r x = x)"
+definition "retraction S T r \<longleftrightarrow> T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
 
 definition retract_of (infixl "retract'_of" 50)
-  where "(t retract_of s) \<longleftrightarrow> (\<exists>r. retraction s t r)"
-
-lemma retraction_idempotent: "retraction s t r \<Longrightarrow> x \<in> s \<Longrightarrow>  r (r x) = r x"
+  where "(T retract_of S) \<longleftrightarrow> (\<exists>r. retraction S T r)"
+
+lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow>  r (r x) = r x"
   unfolding retraction_def by auto
 
 subsection \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
 
 lemma invertible_fixpoint_property:
-  fixes s :: "'a::euclidean_space set"
-    and t :: "'b::euclidean_space set"
-  assumes "continuous_on t i"
-    and "i ` t \<subseteq> s"
-    and "continuous_on s r"
-    and "r ` s \<subseteq> t"
-    and "\<forall>y\<in>t. r (i y) = y"
-    and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
-    and "continuous_on t g"
-    and "g ` t \<subseteq> t"
-  obtains y where "y \<in> t" and "g y = y"
+  fixes S :: "'a::euclidean_space set"
+    and T :: "'b::euclidean_space set"
+  assumes contt: "continuous_on T i"
+    and "i ` T \<subseteq> S"
+    and contr: "continuous_on S r"
+    and "r ` S \<subseteq> T"
+    and ri: "\<And>y. y \<in> T \<Longrightarrow> r (i y) = y"
+    and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
+    and contg: "continuous_on T g"
+    and "g ` T \<subseteq> T"
+  obtains y where "y \<in> T" and "g y = y"
 proof -
-  have "\<exists>x\<in>s. (i \<circ> g \<circ> r) x = x"
-    apply (rule assms(6)[rule_format])
-    apply rule
-    apply (rule continuous_on_compose assms)+
-    apply ((rule continuous_on_subset)?, rule assms)+
-    using assms(2,4,8)
-    apply auto
-    apply blast
-    done
-  then obtain x where x: "x \<in> s" "(i \<circ> g \<circ> r) x = x" ..
-  then have *: "g (r x) \<in> t"
+  have "\<exists>x\<in>S. (i \<circ> g \<circ> r) x = x"
+  proof (rule FP)
+    show "continuous_on S (i \<circ> g \<circ> r)"
+      by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset)
+    show "(i \<circ> g \<circ> r) ` S \<subseteq> S"
+      using assms(2,4,8) by force
+  qed
+  then obtain x where x: "x \<in> S" "(i \<circ> g \<circ> r) x = x" ..
+  then have *: "g (r x) \<in> T"
     using assms(4,8) by auto
   have "r ((i \<circ> g \<circ> r) x) = r x"
     using x by auto
   then show ?thesis
-    apply (rule_tac that[of "r x"])
-    using x
-    unfolding o_def
-    unfolding assms(5)[rule_format,OF *]
-    using assms(4)
-    apply auto
-    done
+    using "*" ri that by auto
 qed
 
 lemma homeomorphic_fixpoint_property:
-  fixes s :: "'a::euclidean_space set"
-    and t :: "'b::euclidean_space set"
-  assumes "s homeomorphic t"
-  shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
-    (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
+  fixes S :: "'a::euclidean_space set"
+    and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T"
+  shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow>
+         (\<forall>g. continuous_on T g \<and> g ` T \<subseteq> T \<longrightarrow> (\<exists>y\<in>T. g y = y))"
+         (is "?lhs = ?rhs")
 proof -
-  obtain r i where
-      "\<forall>x\<in>s. i (r x) = x"
-      "r ` s = t"
-      "continuous_on s r"
-      "\<forall>y\<in>t. r (i y) = y"
-      "i ` t = s"
-      "continuous_on t i"
-    using assms
-    unfolding homeomorphic_def homeomorphism_def
-    by blast
-  then show ?thesis
-    apply -
-    apply rule
-    apply (rule_tac[!] allI impI)+
-    apply (rule_tac g=g in invertible_fixpoint_property[of t i s r])
-    prefer 10
-    apply (rule_tac g=f in invertible_fixpoint_property[of s r t i])
-    apply auto
-    done
+  obtain r i where r:
+      "\<forall>x\<in>S. i (r x) = x" "r ` S = T" "continuous_on S r"
+      "\<forall>y\<in>T. r (i y) = y" "i ` T = S" "continuous_on T i"
+    using assms unfolding homeomorphic_def homeomorphism_def  by blast
+  show ?thesis
+  proof
+    assume ?lhs
+    with r show ?rhs
+      by (metis invertible_fixpoint_property[of T i S r] order_refl)
+  next
+    assume ?rhs
+    with r show ?lhs
+      by (metis invertible_fixpoint_property[of S r T i] order_refl)
+  qed
 qed
 
 lemma retract_fixpoint_property:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-    and s :: "'a set"
-  assumes "t retract_of s"
-    and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
-    and "continuous_on t g"
-    and "g ` t \<subseteq> t"
-  obtains y where "y \<in> t" and "g y = y"
+    and S :: "'a set"
+  assumes "T retract_of S"
+    and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
+    and contg: "continuous_on T g"
+    and "g ` T \<subseteq> T"
+  obtains y where "y \<in> T" and "g y = y"
 proof -
-  obtain h where "retraction s t h"
+  obtain h where "retraction S T h"
     using assms(1) unfolding retract_of_def ..
   then show ?thesis
     unfolding retraction_def
-    apply -
-    apply (rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g])
-    prefer 7
-    apply (rule_tac y = y in that)
-    using assms
-    apply auto
-    done
+    using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
+    by (metis assms(4) contg image_ident that)
 qed
 
 
 subsection \<open>The Brouwer theorem for any set with nonempty interior\<close>
 
 lemma convex_unit_cube: "convex unit_cube"
-  apply (rule is_interval_convex)
-  apply (clarsimp simp add: is_interval_def mem_unit_cube)
-  apply (drule (1) bspec)+
-  apply auto
-  done
+  by (rule is_interval_convex) (fastforce simp add: is_interval_def mem_unit_cube)
 
 lemma brouwer_weak:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
-  assumes "compact s"
-    and "convex s"
-    and "interior s \<noteq> {}"
-    and "continuous_on s f"
-    and "f ` s \<subseteq> s"
-  obtains x where "x \<in> s" and "f x = x"
+  assumes "compact S"
+    and "convex S"
+    and "interior S \<noteq> {}"
+    and "continuous_on S f"
+    and "f ` S \<subseteq> S"
+  obtains x where "x \<in> S" and "f x = x"
 proof -
   let ?U = "unit_cube :: 'a set"
   have "\<Sum>Basis /\<^sub>R 2 \<in> interior ?U"
@@ -1890,7 +1797,7 @@
       unfolding unit_cube_def by force
   qed
   then have *: "interior ?U \<noteq> {}" by fast
-  have *: "?U homeomorphic s"
+  have *: "?U homeomorphic S"
     using homeomorphic_convex_compact[OF convex_unit_cube compact_unit_cube * assms(2,1,3)] .
   have "\<forall>f. continuous_on ?U f \<and> f ` ?U \<subseteq> ?U \<longrightarrow>
     (\<exists>x\<in>?U. f x = x)"
@@ -1898,7 +1805,7 @@
   then show ?thesis
     unfolding homeomorphic_fixpoint_property[OF *]
     using assms
-    by (auto simp: intro: that)
+    by (auto intro: that)
 qed
 
 
@@ -1920,49 +1827,37 @@
 
 lemma brouwer:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
-  assumes "compact s"
-    and "convex s"
-    and "s \<noteq> {}"
-    and "continuous_on s f"
-    and "f ` s \<subseteq> s"
-  obtains x where "x \<in> s" and "f x = x"
+  assumes S: "compact S" "convex S" "S \<noteq> {}"
+    and contf: "continuous_on S f"
+    and fim: "f ` S \<subseteq> S"
+  obtains x where "x \<in> S" and "f x = x"
 proof -
-  have "\<exists>e>0. s \<subseteq> cball 0 e"
-    using compact_imp_bounded[OF assms(1)]
-    unfolding bounded_pos
-    apply (erule_tac exE)
-    apply (rule_tac x=b in exI)
-    apply (auto simp add: dist_norm)
-    done
-  then obtain e where e: "e > 0" "s \<subseteq> cball 0 e"
+  have "\<exists>e>0. S \<subseteq> cball 0 e"
+    using compact_imp_bounded[OF \<open>compact S\<close>]  unfolding bounded_pos
+    by auto
+  then obtain e where e: "e > 0" "S \<subseteq> cball 0 e"
     by blast
-  have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point s) x = x"
-    apply (rule_tac brouwer_ball[OF e(1), of 0 "f \<circ> closest_point s"])
-    apply (rule continuous_on_compose )
-    apply (rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)])
-    apply (rule continuous_on_subset[OF assms(4)])
-    apply (insert closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
-    using assms(5)[unfolded subset_eq]
-    using e(2)[unfolded subset_eq mem_cball]
-    apply (auto simp add: dist_norm)
-    done
-  then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point s) x = x" ..
-  have *: "closest_point s x = x"
-    apply (rule closest_point_self)
-    apply (rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"], unfolded image_iff])
-    apply (rule_tac x="closest_point s x" in bexI)
-    using x
-    unfolding o_def
-    using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3), of x]
-    apply auto
-    done
+  have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point S) x = x"
+  proof (rule_tac brouwer_ball[OF e(1)])
+    show "continuous_on (cball 0 e) (f \<circ> closest_point S)"
+      apply (rule continuous_on_compose)
+      using S compact_eq_bounded_closed continuous_on_closest_point apply blast
+      by (meson S contf closest_point_in_set compact_imp_closed continuous_on_subset image_subsetI)
+    show "(f \<circ> closest_point S) ` cball 0 e \<subseteq> cball 0 e"
+      by clarsimp (metis S fim closest_point_exists(1) compact_eq_bounded_closed e(2) image_subset_iff mem_cball_0 subsetCE)
+  qed (use assms in auto)
+  then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point S) x = x" ..
+  have "x \<in> S"
+    by (metis closest_point_in_set comp_apply compact_imp_closed fim image_eqI S(1) S(3) subset_iff x(2))
+  then have *: "closest_point S x = x"
+    by (rule closest_point_self)
   show thesis
-    apply (rule_tac x="closest_point s x" in that)
-    unfolding x(2)[unfolded o_def]
-    apply (rule closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
-    using *
-    apply auto
-    done
+  proof
+    show "closest_point S x \<in> S"
+      by (simp add: "*" \<open>x \<in> S\<close>)
+    show "f (closest_point S x) = closest_point S x"
+      using "*" x(2) by auto
+  qed
 qed
 
 text \<open>So we get the no-retraction theorem.\<close>
@@ -1975,17 +1870,15 @@
   assume *: "frontier (cball a e) retract_of (cball a e)"
   have **: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
     using scaleR_left_distrib[of 1 1 a] by auto
-  obtain x where x:
-      "x \<in> {x. norm (a - x) = e}"
-      "2 *\<^sub>R a - x = x"
-    apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
-    apply (blast intro: brouwer_ball[OF assms])
-    apply (intro continuous_intros)
-    unfolding frontier_cball subset_eq Ball_def image_iff dist_norm sphere_def
-    apply (auto simp add: ** norm_minus_commute)
-    done
+  obtain x where x: "x \<in> {x. norm (a - x) = e}" "2 *\<^sub>R a - x = x"
+  proof (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
+    show "continuous_on (frontier (cball a e)) ((-) (2 *\<^sub>R a))"
+      by (intro continuous_intros)
+    show "(-) (2 *\<^sub>R a) ` frontier (cball a e) \<subseteq> frontier (cball a e)"
+      by clarsimp (metis "**" dist_norm norm_minus_cancel)
+  qed (auto simp: dist_norm intro: brouwer_ball[OF assms])
   then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
-    by (auto simp add: algebra_simps)
+    by (auto simp: algebra_simps)
   then have "a = x"
     unfolding scaleR_left_distrib[symmetric]
     by auto
@@ -2006,11 +1899,7 @@
   case False
   then show ?thesis
     unfolding contractible_def nullhomotopic_from_sphere_extension
-    apply (simp add: not_less)
-    apply (rule_tac x=id in exI)
-    apply (auto simp: continuous_on_def)
-    apply (meson dist_not_less_zero le_less less_le_trans)
-    done
+    using continuous_on_const less_eq_real_def by auto
 qed
 
 lemma connected_sphere_eq:
@@ -2035,9 +1924,8 @@
         by (metis dist_self greater insertI1 less_add_same_cancel1 mem_sphere mult_2 not_le zero_le_dist)
       then have "finite (sphere a r)"
         by auto
-      with L \<open>r > 0\<close> show "False"
-        apply (auto simp: connected_finite_iff_sing)
-        using xy by auto
+      with L \<open>r > 0\<close> xy show "False"
+        using connected_finite_iff_sing by auto
     qed
     with greater show ?rhs
       by (metis DIM_ge_Suc0 One_nat_def Suc_1 le_antisym not_less_eq_eq)
@@ -2098,12 +1986,10 @@
     unfolding retraction_def
   proof (intro conjI ballI)
     show "frontier (cball a B) \<subseteq> cball a B"
-      by (force simp:)
+      by force
     show "continuous_on (cball a B) h"
       unfolding h_def
-      apply (intro continuous_intros)
-      using contg continuous_on_subset notga apply auto
-      done
+      by (intro continuous_intros) (use contg continuous_on_subset notga in auto)
     show "h ` cball a B \<subseteq> frontier (cball a B)"
       using \<open>0 < B\<close> by (auto simp: h_def notga dist_norm)
     show "\<And>x. x \<in> frontier (cball a B) \<Longrightarrow> h x = x"
@@ -2117,76 +2003,76 @@
 subsection\<open>More Properties of Retractions\<close>
 
 lemma retraction:
-   "retraction s t r \<longleftrightarrow>
-    t \<subseteq> s \<and> continuous_on s r \<and> r ` s = t \<and> (\<forall>x \<in> t. r x = x)"
+   "retraction S T r \<longleftrightarrow>
+    T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
 by (force simp: retraction_def)
 
 lemma retract_of_imp_extensible:
-  assumes "s retract_of t" and "continuous_on s f" and "f ` s \<subseteq> u"
-  obtains g where "continuous_on t g" "g ` t \<subseteq> u" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+  assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U"
+  obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
 using assms
 apply (clarsimp simp add: retract_of_def retraction)
-apply (rule_tac g = "f o r" in that)
+apply (rule_tac g = "f \<circ> r" in that)
 apply (auto simp: continuous_on_compose2)
 done
 
 lemma idempotent_imp_retraction:
-  assumes "continuous_on s f" and "f ` s \<subseteq> s" and "\<And>x. x \<in> s \<Longrightarrow> f(f x) = f x"
-    shows "retraction s (f ` s) f"
+  assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
+    shows "retraction S (f ` S) f"
 by (simp add: assms retraction)
 
 lemma retraction_subset:
-  assumes "retraction s t r" and "t \<subseteq> s'" and "s' \<subseteq> s"
-    shows "retraction s' t r"
-apply (simp add: retraction_def)
-by (metis assms continuous_on_subset image_mono retraction)
+  assumes "retraction S T r" and "T \<subseteq> s'" and "s' \<subseteq> S"
+  shows "retraction s' T r"
+  unfolding retraction_def
+  by (metis assms continuous_on_subset image_mono retraction)
 
 lemma retract_of_subset:
-  assumes "t retract_of s" and "t \<subseteq> s'" and "s' \<subseteq> s"
-    shows "t retract_of s'"
+  assumes "T retract_of S" and "T \<subseteq> s'" and "s' \<subseteq> S"
+    shows "T retract_of s'"
 by (meson assms retract_of_def retraction_subset)
 
-lemma retraction_refl [simp]: "retraction s s (\<lambda>x. x)"
+lemma retraction_refl [simp]: "retraction S S (\<lambda>x. x)"
 by (simp add: continuous_on_id retraction)
 
-lemma retract_of_refl [iff]: "s retract_of s"
+lemma retract_of_refl [iff]: "S retract_of S"
   using continuous_on_id retract_of_def retraction_def by fastforce
 
 lemma retract_of_imp_subset:
-   "s retract_of t \<Longrightarrow> s \<subseteq> t"
+   "S retract_of T \<Longrightarrow> S \<subseteq> T"
 by (simp add: retract_of_def retraction_def)
 
 lemma retract_of_empty [simp]:
-     "({} retract_of s) \<longleftrightarrow> s = {}"  "(s retract_of {}) \<longleftrightarrow> s = {}"
+     "({} retract_of S) \<longleftrightarrow> S = {}"  "(S retract_of {}) \<longleftrightarrow> S = {}"
 by (auto simp: retract_of_def retraction_def)
 
-lemma retract_of_singleton [iff]: "({x} retract_of s) \<longleftrightarrow> x \<in> s"
+lemma retract_of_singleton [iff]: "({x} retract_of S) \<longleftrightarrow> x \<in> S"
   using continuous_on_const
   by (auto simp: retract_of_def retraction_def)
 
 lemma retraction_comp:
-   "\<lbrakk>retraction s t f; retraction t u g\<rbrakk>
-        \<Longrightarrow> retraction s u (g o f)"
+   "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
+        \<Longrightarrow> retraction S U (g \<circ> f)"
 apply (auto simp: retraction_def intro: continuous_on_compose2)
 by blast
 
 lemma retract_of_trans [trans]:
-  assumes "s retract_of t" and "t retract_of u"
-    shows "s retract_of u"
+  assumes "S retract_of T" and "T retract_of U"
+    shows "S retract_of U"
 using assms by (auto simp: retract_of_def intro: retraction_comp)
 
 lemma closedin_retract:
-  fixes s :: "'a :: real_normed_vector set"
-  assumes "s retract_of t"
-    shows "closedin (subtopology euclidean t) s"
+  fixes S :: "'a :: real_normed_vector set"
+  assumes "S retract_of T"
+    shows "closedin (subtopology euclidean T) S"
 proof -
-  obtain r where "s \<subseteq> t" "continuous_on t r" "r ` t \<subseteq> s" "\<And>x. x \<in> s \<Longrightarrow> r x = x"
+  obtain r where "S \<subseteq> T" "continuous_on T r" "r ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x"
     using assms by (auto simp: retract_of_def retraction_def)
-  then have s: "s = {x \<in> t. (norm(r x - x)) = 0}" by auto
+  then have S: "S = {x \<in> T. (norm(r x - x)) = 0}" by auto
   show ?thesis
-    apply (subst s)
+    apply (subst S)
     apply (rule continuous_closedin_preimage_constant)
-    by (simp add: \<open>continuous_on t r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
+    by (simp add: \<open>continuous_on T r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
 qed
 
 lemma closedin_self [simp]:
@@ -2195,52 +2081,52 @@
   by (simp add: closedin_retract)
 
 lemma retract_of_contractible:
-  assumes "contractible t" "s retract_of t"
-    shows "contractible s"
+  assumes "contractible T" "S retract_of T"
+    shows "contractible S"
 using assms
 apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with)
 apply (rule_tac x="r a" in exI)
-apply (rule_tac x="r o h" in exI)
+apply (rule_tac x="r \<circ> h" in exI)
 apply (intro conjI continuous_intros continuous_on_compose)
 apply (erule continuous_on_subset | force)+
 done
 
 lemma retract_of_compact:
-     "\<lbrakk>compact t; s retract_of t\<rbrakk> \<Longrightarrow> compact s"
+     "\<lbrakk>compact T; S retract_of T\<rbrakk> \<Longrightarrow> compact S"
   by (metis compact_continuous_image retract_of_def retraction)
 
 lemma retract_of_closed:
-    fixes s :: "'a :: real_normed_vector set"
-    shows "\<lbrakk>closed t; s retract_of t\<rbrakk> \<Longrightarrow> closed s"
+    fixes S :: "'a :: real_normed_vector set"
+    shows "\<lbrakk>closed T; S retract_of T\<rbrakk> \<Longrightarrow> closed S"
   by (metis closedin_retract closedin_closed_eq)
 
 lemma retract_of_connected:
-    "\<lbrakk>connected t; s retract_of t\<rbrakk> \<Longrightarrow> connected s"
+    "\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S"
   by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
 
 lemma retract_of_path_connected:
-    "\<lbrakk>path_connected t; s retract_of t\<rbrakk> \<Longrightarrow> path_connected s"
+    "\<lbrakk>path_connected T; S retract_of T\<rbrakk> \<Longrightarrow> path_connected S"
   by (metis path_connected_continuous_image retract_of_def retraction)
 
 lemma retract_of_simply_connected:
-    "\<lbrakk>simply_connected t; s retract_of t\<rbrakk> \<Longrightarrow> simply_connected s"
+    "\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
 apply (simp add: retract_of_def retraction_def, clarify)
 apply (rule simply_connected_retraction_gen)
 apply (force simp: continuous_on_id elim!: continuous_on_subset)+
 done
 
 lemma retract_of_homotopically_trivial:
-  assumes ts: "t retract_of s"
-      and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s;
-                       continuous_on u g; g ` u \<subseteq> s\<rbrakk>
-                       \<Longrightarrow> homotopic_with (\<lambda>x. True) u s f g"
-      and "continuous_on u f" "f ` u \<subseteq> t"
-      and "continuous_on u g" "g ` u \<subseteq> t"
-    shows "homotopic_with (\<lambda>x. True) u t f g"
+  assumes ts: "T retract_of S"
+      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
+                       continuous_on U g; g ` U \<subseteq> S\<rbrakk>
+                       \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
+      and "continuous_on U f" "f ` U \<subseteq> T"
+      and "continuous_on U g" "g ` U \<subseteq> T"
+    shows "homotopic_with (\<lambda>x. True) U T f g"
 proof -
-  obtain r where "r ` s \<subseteq> s" "continuous_on s r" "\<forall>x\<in>s. r (r x) = r x" "t = r ` s"
+  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
     using ts by (auto simp: retract_of_def retraction)
-  then obtain k where "Retracts s r t k"
+  then obtain k where "Retracts S r T k"
     unfolding Retracts_def
     by (metis continuous_on_subset dual_order.trans image_iff image_mono)
   then show ?thesis
@@ -2251,15 +2137,15 @@
 qed
 
 lemma retract_of_homotopically_trivial_null:
-  assumes ts: "t retract_of s"
-      and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s\<rbrakk>
-                     \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) u s f (\<lambda>x. c)"
-      and "continuous_on u f" "f ` u \<subseteq> t"
-  obtains c where "homotopic_with (\<lambda>x. True) u t f (\<lambda>x. c)"
+  assumes ts: "T retract_of S"
+      and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
+                     \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
+      and "continuous_on U f" "f ` U \<subseteq> T"
+  obtains c where "homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
 proof -
-  obtain r where "r ` s \<subseteq> s" "continuous_on s r" "\<forall>x\<in>s. r (r x) = r x" "t = r ` s"
+  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
     using ts by (auto simp: retract_of_def retraction)
-  then obtain k where "Retracts s r t k"
+  then obtain k where "Retracts S r T k"
     unfolding Retracts_def
     by (metis continuous_on_subset dual_order.trans image_iff image_mono)
   then show ?thesis
@@ -2269,35 +2155,34 @@
 qed
 
 lemma retraction_imp_quotient_map:
-   "retraction s t r
-    \<Longrightarrow> u \<subseteq> t
-            \<Longrightarrow> (openin (subtopology euclidean s) (s \<inter> r -` u) \<longleftrightarrow>
-                 openin (subtopology euclidean t) u)"
+   "retraction S T r
+    \<Longrightarrow> U \<subseteq> T
+            \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> r -` U) \<longleftrightarrow>
+                 openin (subtopology euclidean T) U)"
 apply (clarsimp simp add: retraction)
 apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
 apply (auto simp: elim: continuous_on_subset)
 done
 
 lemma retract_of_locally_compact:
-    fixes s :: "'a :: {heine_borel,real_normed_vector} set"
-    shows  "\<lbrakk> locally compact s; t retract_of s\<rbrakk> \<Longrightarrow> locally compact t"
+    fixes S :: "'a :: {heine_borel,real_normed_vector} set"
+    shows  "\<lbrakk> locally compact S; T retract_of S\<rbrakk> \<Longrightarrow> locally compact T"
   by (metis locally_compact_closedin closedin_retract)
 
 lemma retract_of_Times:
-   "\<lbrakk>s retract_of s'; t retract_of t'\<rbrakk> \<Longrightarrow> (s \<times> t) retract_of (s' \<times> t')"
+   "\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
 apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
 apply (rename_tac f g)
-apply (rule_tac x="\<lambda>z. ((f o fst) z, (g o snd) z)" in exI)
+apply (rule_tac x="\<lambda>z. ((f \<circ> fst) z, (g \<circ> snd) z)" in exI)
 apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
 done
 
 lemma homotopic_into_retract:
-   "\<lbrakk>f ` s \<subseteq> t; g ` s \<subseteq> t; t retract_of u;
-        homotopic_with (\<lambda>x. True) s u f g\<rbrakk>
-        \<Longrightarrow> homotopic_with (\<lambda>x. True) s t f g"
+   "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with (\<lambda>x. True) S U f g\<rbrakk>
+        \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
 apply (subst (asm) homotopic_with_def)
 apply (simp add: homotopic_with retract_of_def retraction_def, clarify)
-apply (rule_tac x="r o h" in exI)
+apply (rule_tac x="r \<circ> h" in exI)
 apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
 done
 
@@ -2317,15 +2202,19 @@
 
 lemma deformation_retract_imp_homotopy_eqv:
   fixes S :: "'a::euclidean_space set"
-  assumes "homotopic_with (\<lambda>x. True) S S id r" "retraction S T r"
-    shows "S homotopy_eqv T"
-  apply (simp add: homotopy_eqv_def)
-  apply (rule_tac x=r in exI)
-  using assms apply (simp add: retraction_def)
-  apply (rule_tac x=id in exI)
-  apply (auto simp: continuous_on_id)
-   apply (metis homotopic_with_symD)
-  by (metis continuous_on_id' homotopic_with_equal homotopic_with_symD id_apply image_id subset_refl)
+  assumes "homotopic_with (\<lambda>x. True) S S id r" and r: "retraction S T r"
+  shows "S homotopy_eqv T"
+proof -
+  have "homotopic_with (\<lambda>x. True) S S (id \<circ> r) id"
+    by (simp add: assms(1) homotopic_with_symD)
+  moreover have "homotopic_with (\<lambda>x. True) T T (r \<circ> id) id"
+    using r unfolding retraction_def
+    by (metis (no_types, lifting) comp_id continuous_on_id' homotopic_with_equal homotopic_with_symD id_def image_id order_refl)
+  ultimately
+  show ?thesis
+    unfolding homotopy_eqv_def
+    by (metis continuous_on_id' id_def image_id r retraction_def)
+qed
 
 lemma deformation_retract:
   fixes S :: "'a::euclidean_space set"
@@ -2356,10 +2245,8 @@
   have "{a} retract_of S"
     by (simp add: \<open>a \<in> S\<close>)
   moreover have "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
-    using assms
-    apply (clarsimp simp add: contractible_def)
-    apply (rule homotopic_with_trans, assumption)
-    by (metis assms(1) contractible_imp_path_connected homotopic_constant_maps homotopic_with_sym homotopic_with_trans insert_absorb insert_not_empty path_component_mem(1) path_connected_component)
+      using assms
+      by (auto simp: contractible_def continuous_on_const continuous_on_id homotopic_into_contractible image_subset_iff)
   moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
     by (simp add: image_subsetI)
   ultimately show ?thesis
@@ -2382,15 +2269,12 @@
     using assms by auto (metis imageI subset_iff)
   have contp': "continuous_on S p"
     by (rule continuous_on_subset [OF contp \<open>S \<subseteq> T\<close>])
-  have "continuous_on T (q \<circ> p)"
-    apply (rule continuous_on_compose [OF contp])
-    apply (simp add: *)
-    apply (rule continuous_on_inv [OF contp' \<open>compact S\<close>])
-    using assms by auto
+  have "continuous_on (p ` T) q"
+    by (simp add: "*" assms(1) assms(2) assms(5) continuous_on_inv contp' rev_subsetD)
+  then have "continuous_on T (q \<circ> p)"
+    by (rule continuous_on_compose [OF contp])
   then show ?thesis
-    apply (rule continuous_on_eq [of _ "q o p"])
-    apply (simp add: o_def)
-    done
+    by (rule continuous_on_eq [of _ "q \<circ> p"]) (simp add: o_def)
 qed
 
 lemma continuous_on_compact_surface_projection:
@@ -2441,21 +2325,19 @@
   have aaffS: "a \<in> affine hull S"
     by (meson arelS subsetD hull_inc rel_interior_subset)
   have "((\<lambda>z. z - a) ` (affine hull S - {a})) = ((\<lambda>z. z - a) ` (affine hull S)) - {0}"
-    by (auto simp: )
+    by auto
   moreover have "continuous_on (((\<lambda>z. z - a) ` (affine hull S)) - {0}) (\<lambda>x. dd x *\<^sub>R x)"
   proof (rule continuous_on_compact_surface_projection)
     show "compact (rel_frontier ((\<lambda>z. z - a) ` S))"
       by (simp add: \<open>bounded S\<close> bounded_translation_minus compact_rel_frontier_bounded)
     have releq: "rel_frontier ((\<lambda>z. z - a) ` S) = (\<lambda>z. z - a) ` rel_frontier S"
       using rel_frontier_translation [of "-a"] add.commute by simp
-    also have "... \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}"
+    also have "\<dots> \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}"
       using rel_frontier_affine_hull arelS rel_frontier_def by fastforce
     finally show "rel_frontier ((\<lambda>z. z - a) ` S) \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}" .
     show "cone ((\<lambda>z. z - a) ` (affine hull S))"
-      apply (rule subspace_imp_cone)
-      using aaffS
-      apply (simp add: subspace_affine image_comp o_def affine_translation_aux [of a])
-      done
+      by (rule subspace_imp_cone)
+         (use aaffS in \<open>simp add: subspace_affine image_comp o_def affine_translation_aux [of a]\<close>)
     show "(0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)) \<longleftrightarrow> (dd x = k)"
          if x: "x \<in> (\<lambda>z. z - a) ` (affine hull S) - {0}" for k x
     proof
@@ -2471,7 +2353,7 @@
         then have segsub: "open_segment a (a + k *\<^sub>R x) \<subseteq> rel_interior S"
           by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
         have "x \<noteq> 0" and xaffS: "a + x \<in> affine hull S"
-          using x by (auto simp: )
+          using x by auto
         then have "0 < dd x" and inS: "a + dd x *\<^sub>R x \<in> rel_frontier S"
           using dd1 by auto
         moreover have "a + dd x *\<^sub>R x \<in> open_segment a (a + k *\<^sub>R x)"
@@ -2483,7 +2365,7 @@
           apply (metis (no_types) \<open>k \<noteq> 0\<close> divide_inverse_commute inverse_eq_divide mult.left_commute right_inverse)
           done
         ultimately show ?thesis
-          using segsub by (auto simp add: rel_frontier_def)
+          using segsub by (auto simp: rel_frontier_def)
       qed
       moreover have False if "k < dd x"
         using x k that rel_frontier_def
@@ -2497,7 +2379,7 @@
   have "continuous_on (affine hull S - {a}) ((\<lambda>x. a + dd x *\<^sub>R x) \<circ> (\<lambda>z. z - a))"
     by (intro * continuous_intros continuous_on_compose)
   with affS have contdd: "continuous_on (T - {a}) ((\<lambda>x. a + dd x *\<^sub>R x) \<circ> (\<lambda>z. z - a))"
-    by (blast intro: continuous_on_subset elim: )
+    by (blast intro: continuous_on_subset)
   show ?thesis
   proof
     show "homotopic_with (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
@@ -2510,11 +2392,10 @@
            if "x \<in> T - {a}" for x
       proof (clarsimp simp: in_segment, intro conjI)
         fix u::real assume u: "0 \<le> u" "u \<le> 1"
-        show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<in> T"
-          apply (rule convexD [OF \<open>convex T\<close>])
-          using that u apply (auto simp add: )
-          apply (metis add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 relS subsetD)
-          done
+        have "a + dd (x - a) *\<^sub>R (x - a) \<in> T"
+          by (metis DiffD1 DiffD2 add.commute add.right_neutral affS dd1 diff_add_cancel relS singletonI subsetCE that)
+        then show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<in> T"
+          using convexD [OF \<open>convex T\<close>] that u by simp
         have iff: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + d *\<^sub>R (x - a)) = a \<longleftrightarrow>
                   (1 - u + u * d) *\<^sub>R (x - a) = 0" for d
           by (auto simp: algebra_simps)
@@ -2541,7 +2422,7 @@
       show "a + dd (x - a) *\<^sub>R (x - a) = x" if x: "x \<in> rel_frontier S" for x
       proof -
         have "x \<noteq> a"
-          using that arelS by (auto simp add: rel_frontier_def)
+          using that arelS by (auto simp: rel_frontier_def)
         have False if "dd (x - a) < 1"
         proof -
           have "x \<in> closure S"
@@ -2551,7 +2432,7 @@
           have  xaffS: "x \<in> affine hull S"
             using affS relS x by auto
           then have "0 < dd (x - a)" and inS: "a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
-            using dd1 by (auto simp add: \<open>x \<noteq> a\<close>)
+            using dd1 by (auto simp: \<open>x \<noteq> a\<close>)
           moreover have "a + dd (x - a) *\<^sub>R (x - a) \<in> open_segment a x"
             using  \<open>x \<noteq> a\<close> \<open>0 < dd (x - a)\<close>
             apply (simp add: in_segment)
@@ -2559,7 +2440,7 @@
             apply (simp add: algebra_simps that)
             done
           ultimately show ?thesis
-            using segsub by (auto simp add: rel_frontier_def)
+            using segsub by (auto simp: rel_frontier_def)
         qed
         moreover have False if "1 < dd (x - a)"
           using x that dd2 [of "x - a" 1] \<open>x \<noteq> a\<close> closure_affine_hull
@@ -2578,7 +2459,7 @@
   assumes "bounded S" "convex S" "a \<in> rel_interior S"
     shows "rel_frontier S retract_of (affine hull S - {a})"
 apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S "affine hull S" a])
-apply (auto simp add: affine_imp_convex rel_frontier_affine_hull retract_of_def assms)
+apply (auto simp: affine_imp_convex rel_frontier_affine_hull retract_of_def assms)
 done
 
 corollary rel_boundary_retract_of_punctured_affine_hull:
@@ -2643,7 +2524,7 @@
     using assms by (auto simp: path_component_def)
   then show ?thesis
     apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def)
-    apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g o fst)z)) *\<^sub>R (snd z - (g o fst)z)" in exI)
+    apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g \<circ> fst)z)) *\<^sub>R (snd z - (g \<circ> fst)z)" in exI)
     apply (intro conjI continuous_intros)
     apply (rule continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
     done
@@ -2767,7 +2648,7 @@
     using hom by (force simp: homeomorphic_def)
   then have "continuous_on (f ` T) g"
     by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def)
-  then have contgf: "continuous_on T (g o f)"
+  then have contgf: "continuous_on T (g \<circ> f)"
     by (metis continuous_on_compose contf)
   have gfTC: "(g \<circ> f) ` T \<subseteq> C"
   proof -
@@ -2779,7 +2660,7 @@
                       "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
     by (metis Dugundji [OF C cloUT contgf gfTC])
   show ?thesis
-  proof (rule_tac g = "h o r o f'" in that)
+  proof (rule_tac g = "h \<circ> r \<circ> f'" in that)
     show "continuous_on U (h \<circ> r \<circ> f')"
       apply (intro continuous_on_compose f')
        using continuous_on_subset contr f' apply blast
@@ -2811,7 +2692,7 @@
   have [simp]: "S' \<subseteq> U" using clo closedin_limpt by blast
   show ?thesis
   proof (simp add: retraction_def retract_of_def, intro exI conjI)
-    show "continuous_on U (g o h')"
+    show "continuous_on U (g \<circ> h')"
       apply (intro continuous_on_compose h')
       apply (meson hom continuous_on_subset h' homeomorphism_cont1)
       done
@@ -2853,7 +2734,7 @@
     using clo closedin_imp_subset by auto
   show "T retract_of U"
   proof (simp add: retraction_def retract_of_def, intro exI conjI)
-    show "continuous_on U (g o h')"
+    show "continuous_on U (g \<circ> h')"
       apply (intro continuous_on_compose h')
       apply (meson hom continuous_on_subset h' homeomorphism_cont1)
       done
@@ -2919,7 +2800,7 @@
     using hom by (force simp: homeomorphic_def)
   have "continuous_on (f ` T) g"
     by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def homgh)
-  then have contgf: "continuous_on T (g o f)"
+  then have contgf: "continuous_on T (g \<circ> f)"
     by (intro continuous_on_compose contf)
   have gfTC: "(g \<circ> f) ` T \<subseteq> C"
   proof -
@@ -2933,7 +2814,7 @@
               and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
     by (metis Dugundji [OF C cloUT contgf gfTC])
   show ?thesis
-  proof (rule_tac V = "U \<inter> f' -` D" and g = "h o r o f'" in that)
+  proof (rule_tac V = "U \<inter> f' -` D" and g = "h \<circ> r \<circ> f'" in that)
     show "T \<subseteq> U \<inter> f' -` D"
       using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
       by fastforce
@@ -2976,7 +2857,7 @@
     by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo])
   have "S' retract_of V"
   proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>S' \<subseteq> V\<close>)
-    show "continuous_on V (g o h')"
+    show "continuous_on V (g \<circ> h')"
       apply (intro continuous_on_compose h')
       apply (meson hom continuous_on_subset h' homeomorphism_cont1)
       done
@@ -3029,7 +2910,7 @@
     using clo closedin_imp_subset by auto
   have "T retract_of V"
   proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>T \<subseteq> V\<close>)
-    show "continuous_on V (g o h')"
+    show "continuous_on V (g \<circ> h')"
       apply (intro continuous_on_compose h')
       apply (meson hom continuous_on_subset h' homeomorphism_cont1)
       done
@@ -3086,7 +2967,7 @@
     using Diff_subset_conv \<open>U - Z \<subseteq> W\<close> by blast
   ultimately show ?thesis
     apply (rule_tac V=V and W = "U-W" in that)
-    using openin_imp_subset apply (force simp:)+
+    using openin_imp_subset apply force+
     done
 qed
 
@@ -3146,7 +3027,7 @@
   proof (simp add: retraction_def retract_of_def, intro exI conjI)
     show "S' \<subseteq> W" "S' \<subseteq> h -` X"
       using him WS' closedin_imp_subset by blast+
-    show "continuous_on (W \<inter> h -` X) (f o r o h)"
+    show "continuous_on (W \<inter> h -` X) (f \<circ> r \<circ> h)"
     proof (intro continuous_on_compose)
       show "continuous_on (W \<inter> h -` X) h"
         by (meson conth continuous_on_subset inf_le1)
@@ -3356,7 +3237,7 @@
 apply (clarsimp elim!: all_forward)
 apply (erule impCE, metis subset_trans)
 apply (clarsimp elim!: ex_forward)
-apply (rule_tac x="r o g" in exI)
+apply (rule_tac x="r \<circ> g" in exI)
 by (metis comp_apply continuous_on_compose continuous_on_subset subsetD imageI image_comp image_mono subset_trans)
 
 lemma AR_retract_of_AR:
@@ -3642,7 +3523,7 @@
   obtain r0
     where "S \<inter> T \<subseteq> W0" and contr0: "continuous_on W0 r0" and "r0 ` W0 \<subseteq> S \<inter> T"
       and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
-    using ret  by (force simp add: retract_of_def retraction_def)
+    using ret  by (force simp: retract_of_def retraction_def)
   have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
     using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin)
   define r where "r \<equiv> \<lambda>x. if x \<in> W0 then r0 x else x"
@@ -3667,8 +3548,7 @@
                 and opeSW1: "openin (subtopology euclidean S') W1"
                 and "g ` W1 \<subseteq> S" and geqr: "\<And>x. x \<in> W0 \<union> S \<Longrightarrow> g x = r x"
     apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> _ \<open>r ` (W0 \<union> S) \<subseteq> S\<close> cloS'WS])
-     apply (rule continuous_on_subset [OF contr])
-    apply (blast intro:  elim: )+
+     apply (rule continuous_on_subset [OF contr], blast+)
     done
   have cloT'WT: "closedin (subtopology euclidean T') (W0 \<union> T)"
     by (meson closedin_subset_trans UT cloUT' \<open>T \<subseteq> T'\<close> \<open>W \<subseteq> T'\<close> cloUW cloWW0 
@@ -3677,13 +3557,12 @@
                 and opeSW2: "openin (subtopology euclidean T') W2"
                 and "h ` W2 \<subseteq> T" and heqr: "\<And>x. x \<in> W0 \<union> T \<Longrightarrow> h x = r x"
     apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> _ \<open>r ` (W0 \<union> T) \<subseteq> T\<close> cloT'WT])
-     apply (rule continuous_on_subset [OF contr])
-    apply (blast intro:  elim: )+
+     apply (rule continuous_on_subset [OF contr], blast+)
     done
   have "S' \<inter> T' = W"
     by (force simp: S'_def T'_def W_def)
   obtain O1 O2 where "open O1" "W1 = S' \<inter> O1" "open O2" "W2 = T' \<inter> O2"
-    using opeSW1 opeSW2 by (force simp add: openin_open)
+    using opeSW1 opeSW2 by (force simp: openin_open)
   show ?thesis
   proof
     have eq: "W1 - (W - U0) \<union> (W2 - (W - U0)) =
@@ -3692,25 +3571,23 @@
       by (auto simp: \<open>S' \<union> T' = U\<close> [symmetric] \<open>S' \<inter> T' = W\<close> [symmetric] \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close>)
     show "openin (subtopology euclidean U) (W1 - (W - U0) \<union> (W2 - (W - U0)))"
       apply (subst eq)
-      apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \<open>open O1\<close> \<open>open O2\<close>)
-      apply simp_all
+      apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \<open>open O1\<close> \<open>open O2\<close>, simp_all)
       done
     have cloW1: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W1 - (W - U0))"
       using cloUS' apply (simp add: closedin_closed)
       apply (erule ex_forward)
       using U0 \<open>W0 \<union> S \<subseteq> W1\<close>
-      apply (auto simp add: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
+      apply (auto simp: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
       done
     have cloW2: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W2 - (W - U0))"
       using cloUT' apply (simp add: closedin_closed)
       apply (erule ex_forward)
       using U0 \<open>W0 \<union> T \<subseteq> W2\<close>
-      apply (auto simp add: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
+      apply (auto simp: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
       done
     have *: "\<forall>x\<in>S \<union> T. (if x \<in> S' then g x else h x) = x"
       using ST \<open>S' \<inter> T' = W\<close> cloT'WT closedin_subset geqr heqr 
-      apply (auto simp: r_def)
-       apply fastforce
+      apply (auto simp: r_def, fastforce)
       using \<open>S \<subseteq> S'\<close> \<open>T \<subseteq> T'\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W1 = S' \<inter> O1\<close>  by auto
     have "\<exists>r. continuous_on (W1 - (W - U0) \<union> (W2 - (W - U0))) r \<and>
               r ` (W1 - (W - U0) \<union> (W2 - (W - U0))) \<subseteq> S \<union> T \<and> 
@@ -3725,7 +3602,7 @@
       done
     then show "S \<union> T retract_of W1 - (W - U0) \<union> (W2 - (W - U0))"
       using  \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close> ST opeUU0 U0
-      by (auto simp add: retract_of_def retraction_def)
+      by (auto simp: retract_of_def retraction_def)
   qed
 qed
 
@@ -4059,15 +3936,15 @@
     by (auto simp: closest_point_self)
   have "rel_frontier S retract_of affine hull S - {a}"
     by (simp add: assms a rel_frontier_retract_of_punctured_affine_hull)
-  also have "... retract_of {x. closest_point (affine hull S) x \<noteq> a}"
+  also have "\<dots> retract_of {x. closest_point (affine hull S) x \<noteq> a}"
     apply (simp add: retract_of_def retraction_def ahS)
     apply (rule_tac x="closest_point (affine hull S)" in exI)
-    apply (auto simp add: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point)
+    apply (auto simp: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point)
     done
   finally have "rel_frontier S retract_of {x. closest_point (affine hull S) x \<noteq> a}" .
   moreover have "openin (subtopology euclidean UNIV) (UNIV \<inter> closest_point (affine hull S) -` (- {a}))"
     apply (rule continuous_openin_preimage_gen)
-    apply (auto simp add: False affine_imp_convex continuous_on_closest_point)
+    apply (auto simp: False affine_imp_convex continuous_on_closest_point)
     done
   ultimately show ?thesis
     unfolding ENR_def
@@ -4116,7 +3993,7 @@
       apply (rule continuous_on_cases_local [OF clS clT])
       using r by (auto simp: continuous_on_id)
   qed (use r in auto)
-  also have "... retract_of U"
+  also have "\<dots> retract_of U"
     by (rule Un)
   finally show ?thesis .
 qed
@@ -4499,7 +4376,7 @@
              and him: "h ` ({0..1} \<times> S) \<subseteq> U"
              and [simp]: "\<And>x. h(0, x) = f x" "\<And>x. h(1::real, x) = g x"
        using assms by (auto simp: homotopic_with_def)
-  define h' where "h' \<equiv>  \<lambda>z. if snd z \<in> S then h z else (f o snd) z"
+  define h' where "h' \<equiv>  \<lambda>z. if snd z \<in> S then h z else (f \<circ> snd) z"
   define B where "B \<equiv> {0::real} \<times> T \<union> {0..1} \<times> S"
   have clo0T: "closedin (subtopology euclidean ({0..1} \<times> T)) ({0::real} \<times> T)"
     by (simp add: closedin_subtopology_refl closedin_Times)
@@ -4542,7 +4419,7 @@
                       "retraction V B r" for V r
       using that
       apply (clarsimp simp add: retraction_def)
-      apply (rule Vk [of V "h' o r"], assumption+)
+      apply (rule Vk [of V "h' \<circ> r"], assumption+)
         apply (metis continuous_on_compose conth' continuous_on_subset) 
       using \<open>h' ` B \<subseteq> U\<close> apply force+
       done
@@ -4629,7 +4506,7 @@
 proof
   assume ?lhs
   then obtain c where c: "homotopic_with (\<lambda>x. True) S T (\<lambda>x. c) f"
-    by (blast intro: homotopic_with_symD elim: )
+    by (blast intro: homotopic_with_symD)
   have "closedin (subtopology euclidean UNIV) S"
     using \<open>closed S\<close> closed_closedin by fastforce
   then obtain g where "continuous_on UNIV g" "range g \<subseteq> T"
@@ -4645,10 +4522,10 @@
   then obtain c where "homotopic_with (\<lambda>h. True) UNIV T g (\<lambda>x. c)"
     using nullhomotopic_from_contractible [of UNIV g T] contractible_UNIV by blast
   then show ?lhs
-    apply (rule_tac x="c" in exI)
+    apply (rule_tac x=c in exI)
     apply (rule homotopic_with_eq [of _ _ _ g "\<lambda>x. c"])
     apply (rule homotopic_with_subset_left)
-    apply (auto simp add: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
+    apply (auto simp: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
     done
 qed
 
@@ -4672,7 +4549,7 @@
            (is "?lhs = ?rhs")
 proof (cases "r = 0")
   case True with fim show ?thesis
-    apply (auto simp: )
+    apply auto
     using fim continuous_on_const apply fastforce
     by (metis contf contractible_sing nullhomotopic_into_contractible)
 next
@@ -4717,11 +4594,11 @@
     obtain g where "range g \<subseteq> sphere 0 1" "continuous_on UNIV g"
                         "\<And>x. x \<in> S \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
       using notr
-      by (auto simp add: nullhomotopic_into_sphere_extension
+      by (auto simp: nullhomotopic_into_sphere_extension
                  [OF \<open>closed S\<close> continuous_on_Borsuk_map [OF \<open>a \<notin> S\<close>] False s01])
     with \<open>a \<notin> S\<close> show  "~ ?lhs"
       apply (clarsimp simp: Borsuk_map_into_sphere [of a S, symmetric] dest!: nog)
-      apply (drule_tac x="g" in spec)
+      apply (drule_tac x=g in spec)
       using continuous_on_subset by fastforce 
   next
     assume "~ ?lhs"
@@ -5070,7 +4947,7 @@
         then obtain k where "y \<in> V k" and j: "\<forall>j<k. y \<notin> V j"
           by (metis image_iff V wop)
         with him t show "\<zeta>(t, y) \<in> T"
-          by (subst eq) (force simp:)+
+          by (subst eq) force+
       qed
       fix X y
       assume "X \<in> \<V>" "y \<in> X"