# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1603139361 -3600
# Node ID 7956d958ef5bb182c84a091475252fa3dd09d57c
# Parent  fa4bb287ea5678b38fd9e39a34e447502bc06910
tidying and de-applying

diff -r fa4bb287ea56 -r 7956d958ef5b src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Sat Oct 17 18:36:08 2020 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy	Mon Oct 19 21:29:21 2020 +0100
@@ -32,9 +32,7 @@
     fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space"
   assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)"
   shows "(sphere a r homeomorphic sphere b s)"
-  apply (rule homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres'])
-  using assms  apply auto
-  done
+  using assms homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres'] by auto
 
 subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
 
@@ -128,13 +126,15 @@
         assume "x \<in> affine hull S" and nox: "norm x = 1"
         then have "x \<noteq> 0" by auto
         obtain d where "0 < d" and dx: "(d *\<^sub>R x) \<in> rel_frontier S"
-                   and ri: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (e *\<^sub>R x) \<in> rel_interior S"
+          and ri: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (e *\<^sub>R x) \<in> rel_interior S"
           using ray_to_rel_frontier [OF \<open>bounded S\<close> 0] \<open>x \<in> affine hull S\<close> \<open>x \<noteq> 0\<close> by auto
         show "x \<in> (\<lambda>x. x /\<^sub>R norm x) ` (S - rel_interior S)"
-          apply (rule_tac x="d *\<^sub>R x" in image_eqI)
-          using \<open>0 < d\<close>
-          using dx \<open>closed S\<close> apply (auto simp: rel_frontier_def field_split_simps nox)
-          done
+        proof
+          show "x = d *\<^sub>R x /\<^sub>R norm (d *\<^sub>R x)"
+            using \<open>0 < d\<close> by (auto simp: nox)
+          show "d *\<^sub>R x \<in> S - rel_interior S"
+            using dx \<open>closed S\<close> by (auto simp: rel_frontier_def)
+        qed
       qed
     qed
   qed (rule inj_on_proj)
@@ -145,11 +145,12 @@
   have surf_nz: "\<And>x. x \<in> ?SPHER \<Longrightarrow> surf x \<noteq> 0"
     by (metis "0" DiffE homeomorphism_def imageI surf)
   have cont_nosp: "continuous_on (?SPHER) (\<lambda>x. norm x *\<^sub>R ((surf o proj) x))"
-    apply (rule continuous_intros)+
-    apply (rule continuous_on_subset [OF cont_proj], force)
-    apply (rule continuous_on_subset [OF cont_surf])
-    apply (force simp: homeomorphism_image1 [OF surf] dest: proj_spherI)
-    done
+  proof (intro continuous_intros)
+    show "continuous_on (sphere 0 1 \<inter> affine hull S) proj"
+      by (rule continuous_on_subset [OF cont_proj], force)
+    show "continuous_on (proj ` (sphere 0 1 \<inter> affine hull S)) surf"
+      by (intro continuous_on_subset [OF cont_surf]) (force simp: homeomorphism_image1 [OF surf] dest: proj_spherI)
+  qed
   have surfpS: "\<And>x. \<lbrakk>norm x = 1; x \<in> affine hull S\<rbrakk> \<Longrightarrow> surf (proj x) \<in> S"
     by (metis (full_types) DiffE \<open>0 \<in> S\<close> homeomorphism_def image_eqI norm_zero proj_spherI real_vector.scale_zero_left scaleR_one surf)
   have *: "\<exists>y. norm y = 1 \<and> y \<in> affine hull S \<and> x = surf (proj y)"
@@ -179,44 +180,37 @@
   have co01: "compact ?SPHER"
     by (simp add: compact_Int_closed)
   show "?SMINUS homeomorphic ?SPHER"
-    apply (subst homeomorphic_sym)
-    apply (rule homeomorphic_compact [OF co01 cont_nosp [unfolded o_def] no_sp_im inj_spher])
-    done
+    using homeomorphic_def surf by blast
   have proj_scaleR: "\<And>a x. 0 < a \<Longrightarrow> proj (a *\<^sub>R x) = proj x"
     by (simp add: proj_def)
   have cont_sp0: "continuous_on (affine hull S - {0}) (surf o proj)"
-    apply (rule continuous_on_compose [OF continuous_on_subset [OF cont_proj]], force)
-    apply (rule continuous_on_subset [OF cont_surf])
-    using homeomorphism_image1 proj_spherI surf by fastforce
+  proof (rule continuous_on_compose [OF continuous_on_subset [OF cont_proj]])
+    show "continuous_on (proj ` (affine hull S - {0})) surf"
+      using homeomorphism_image1 proj_spherI surf by (intro continuous_on_subset [OF cont_surf]) fastforce
+  qed auto
   obtain B where "B>0" and B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
     by (metis compact_imp_bounded \<open>compact S\<close> bounded_pos_less less_eq_real_def)
   have cont_nosp: "continuous (at x within ?CBALL) (\<lambda>x. norm x *\<^sub>R surf (proj x))"
          if "norm x \<le> 1" "x \<in> affine hull S" for x
   proof (cases "x=0")
     case True
-    show ?thesis using True
+    have "(norm \<longlongrightarrow> 0) (at 0 within cball 0 1 \<inter> affine hull S)"
+      by (simp add: tendsto_norm_zero eventually_at)
+    with True show ?thesis 
       apply (simp add: continuous_within)
       apply (rule lim_null_scaleR_bounded [where B=B])
-      apply (simp_all add: tendsto_norm_zero eventually_at)
-      apply (rule_tac x=B in exI)
-      using B surfpS proj_def projI apply (auto simp: \<open>B > 0\<close>)
-      done
+      using B \<open>0 < B\<close> local.proj_def projI surfpS by (auto simp: eventually_at)
   next
     case False
     then have "\<forall>\<^sub>F x in at x. (x \<in> affine hull S - {0}) = (x \<in> affine hull S)"
-      apply (simp add: eventually_at)
-      apply (rule_tac x="norm x" in exI)
-      apply (auto simp: False)
-      done
-    with cont_sp0 have *: "continuous (at x within affine hull S) (\<lambda>x. surf (proj x))"
-      apply (simp add: continuous_on_eq_continuous_within)
-      apply (drule_tac x=x in bspec, force simp: False that)
-      apply (simp add: continuous_within Lim_transform_within_set)
-      done
+      by (force simp: False eventually_at)
+    moreover 
+    have "continuous (at x within affine hull S - {0}) (\<lambda>x. surf (proj x))"
+      using cont_sp0 False that by (auto simp add: continuous_on_eq_continuous_within)
+    ultimately have *: "continuous (at x within affine hull S) (\<lambda>x. surf (proj x))"
+      by (simp add: continuous_within Lim_transform_within_set continuous_on_eq_continuous_within)
     show ?thesis
-      apply (rule continuous_within_subset [where s = "affine hull S", OF _ Int_lower2])
-      apply (rule continuous_intros *)+
-      done
+      by (intro continuous_within_subset [where s = "affine hull S", OF _ Int_lower2] continuous_intros *)
   qed
   have cont_nosp2: "continuous_on ?CBALL (\<lambda>x. norm x *\<^sub>R ((surf o proj) x))"
     by (simp add: continuous_on_eq_continuous_within cont_nosp)
@@ -230,9 +224,7 @@
       by (simp add: proj_def)
     have "norm y \<le> 1" using that by simp
     have "surf (proj (y /\<^sub>R norm y)) \<in> S"
-      apply (rule surfpS)
-      using proj_def projI yaff
-      by (auto simp: False)
+      using False local.proj_def nproj1 projI surfpS yaff by blast
     then have "surf (proj y) \<in> S"
       by (simp add: False proj_def)
     then show "norm y *\<^sub>R surf (proj y) \<in> S"
@@ -262,11 +254,12 @@
       using starI [OF that] by (meson starI [OF that] le_less_linear norm_ge_zero zero_le_divide_iff)
     then have nole: "norm x \<le> norm (surf (proj x))"
       by (simp add: le_divide_eq_1)
+    let ?inx = "x /\<^sub>R norm (surf (proj x))"
     show ?thesis
-      apply (rule_tac x="inverse(norm(surf (proj x))) *\<^sub>R x" in image_eqI)
-      apply (metis (no_types, hide_lams) mult.commute scaleproj abs_inverse abs_norm_cancel divide_inverse norm_scaleR nxx positive_imp_inverse_positive proj_scaleR psp sproj_nz zero_less_norm_iff)
-      apply (auto simp: field_split_simps nole affineI)
-      done
+    proof
+      show "x = norm ?inx *\<^sub>R surf (proj ?inx)"
+        by (simp add: field_simps) (metis inverse_eq_divide nxx positive_imp_inverse_positive proj_scaleR psp scaleproj sproj_nz zero_less_norm_iff)
+      qed (auto simp: field_split_simps nole affineI)
   qed
   ultimately have im_cball: "(\<lambda>x. norm x *\<^sub>R surf (proj x)) ` ?CBALL = S"
     by blast
@@ -295,9 +288,7 @@
   have co01: "compact ?CBALL"
     by (simp add: compact_Int_closed)
   show "S homeomorphic ?CBALL"
-    apply (subst homeomorphic_sym)
-    apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball])
-    done
+    using homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball] homeomorphic_sym by blast
 qed
 
 corollary
@@ -416,16 +407,22 @@
   also have "... = cball 0 1 \<inter> span ?aS"
     using eqspanS affine_hull_translation by blast
   also have "... homeomorphic cball 0 1 \<inter> span ?bT"
-    proof (rule homeomorphicI [where f=f and g=g])
-      show fim1: "f ` (cball 0 1 \<inter> span ?aS) = cball 0 1 \<inter> span ?bT"
-        apply (rule subset_antisym)
-         using fim fno apply (force simp:, clarify)
-        by (metis IntI fg gim gno image_eqI mem_cball_0)
-      show "g ` (cball 0 1 \<inter> span ?bT) = cball 0 1 \<inter> span ?aS"
-        apply (rule subset_antisym)
-         using gim gno apply (force simp:, clarify)
-        by (metis IntI fim1 gf image_eqI)
-    qed (auto simp: fg gf)
+  proof (rule homeomorphicI)
+    show fim1: "f ` (cball 0 1 \<inter> span ?aS) = cball 0 1 \<inter> span ?bT"
+    proof
+      show "f ` (cball 0 1 \<inter> span ?aS) \<subseteq> cball 0 1 \<inter> span ?bT"
+        using fim fno by auto
+      show "cball 0 1 \<inter> span ?bT \<subseteq> f ` (cball 0 1 \<inter> span ?aS)"
+        by clarify (metis IntI fg gim gno image_eqI mem_cball_0)
+    qed
+    show "g ` (cball 0 1 \<inter> span ?bT) = cball 0 1 \<inter> span ?aS"
+    proof
+      show "g ` (cball 0 1 \<inter> span ?bT) \<subseteq> cball 0 1 \<inter> span ?aS"
+        using gim gno by auto
+      show "cball 0 1 \<inter> span ?aS \<subseteq> g ` (cball 0 1 \<inter> span ?bT)"
+        by clarify (metis IntI fim1 gf image_eqI)
+    qed
+  qed (auto simp: fg gf)
   also have "... = cball 0 1 \<inter> (+) (-b) ` (affine hull T)"
     using eqspanT affine_hull_translation by blast
   also have "... = (+) (-b) ` (cball b 1 \<inter> affine hull T)"
@@ -445,16 +442,22 @@
   also have "... = sphere 0 1 \<inter> span ?aS"
     using eqspanS affine_hull_translation by blast
   also have "... homeomorphic sphere 0 1 \<inter> span ?bT"
-    proof (rule homeomorphicI [where f=f and g=g])
-      show fim1: "f ` (sphere 0 1 \<inter> span ?aS) = sphere 0 1 \<inter> span ?bT"
-        apply (rule subset_antisym)
-        using fim fno apply (force simp:, clarify)
-        by (metis IntI fg gim gno image_eqI mem_sphere_0)
-      show "g ` (sphere 0 1 \<inter> span ?bT) = sphere 0 1 \<inter> span ?aS"
-        apply (rule subset_antisym)
-        using gim gno apply (force simp:, clarify)
-        by (metis IntI fim1 gf image_eqI)
-    qed (auto simp: fg gf)
+  proof (rule homeomorphicI)
+    show fim1: "f ` (sphere 0 1 \<inter> span ?aS) = sphere 0 1 \<inter> span ?bT"
+    proof
+      show "f ` (sphere 0 1 \<inter> span ?aS) \<subseteq> sphere 0 1 \<inter> span ?bT"
+        using fim fno by auto
+      show "sphere 0 1 \<inter> span ?bT \<subseteq> f ` (sphere 0 1 \<inter> span ?aS)"
+        by clarify (metis IntI fg gim gno image_eqI mem_sphere_0)
+    qed
+    show "g ` (sphere 0 1 \<inter> span ?bT) = sphere 0 1 \<inter> span ?aS"
+    proof
+      show "g ` (sphere 0 1 \<inter> span ?bT) \<subseteq> sphere 0 1 \<inter> span ?aS"
+        using gim gno by auto
+      show "sphere 0 1 \<inter> span ?aS \<subseteq> g ` (sphere 0 1 \<inter> span ?bT)"
+        by clarify (metis IntI fim1 gf image_eqI)
+    qed
+  qed (auto simp: fg gf)
   also have "... = sphere 0 1 \<inter> (+) (-b) ` (affine hull T)"
     using eqspanT affine_hull_translation by blast
   also have "... = (+) (-b) ` (sphere b 1 \<inter> affine hull T)"
@@ -502,35 +505,34 @@
     using \<open>norm b = 1\<close> \<open>b \<in> T\<close> by auto
   define f where "f \<equiv> \<lambda>x. 2 *\<^sub>R b + (2 / (1 - b\<bullet>x)) *\<^sub>R (x - b)"
   define g where "g \<equiv> \<lambda>y. b + (4 / (norm y ^ 2 + 4)) *\<^sub>R (y - 2 *\<^sub>R b)"
-  have [simp]: "\<And>x. \<lbrakk>x \<in> T; b\<bullet>x = 0\<rbrakk> \<Longrightarrow> f (g x) = x"
+  have fg[simp]: "\<And>x. \<lbrakk>x \<in> T; b\<bullet>x = 0\<rbrakk> \<Longrightarrow> f (g x) = x"
     unfolding f_def g_def by (simp add: algebra_simps field_split_simps add_nonneg_eq_0_iff)
   have no: "(norm (f x))\<^sup>2 = 4 * (1 + b \<bullet> x) / (1 - b \<bullet> x)"
     if "norm x = 1" and "b \<bullet> x \<noteq> 1" for x
-    using that
+    using that sum_sqs_eq [of 1 "b \<bullet> x"]
     apply (simp flip: dot_square_norm add: norm_eq_1 nonzero_eq_divide_eq)
     apply (simp add: f_def vector_add_divide_simps inner_simps)
-    apply (use sum_sqs_eq [of 1 "b \<bullet> x"]
-     in \<open>auto simp add: field_split_simps inner_commute\<close>)
+    apply (auto simp add: field_split_simps inner_commute)
     done
   have [simp]: "\<And>u::real. 8 + u * (u * 8) = u * 16 \<longleftrightarrow> u=1"
     by algebra
-  have [simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> g (f x) = x"
+  have gf[simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> g (f x) = x"
     unfolding g_def no by (auto simp: f_def field_split_simps)
-  have [simp]: "norm (g x) = 1" if "x \<in> T" and "b \<bullet> x = 0" for x
+  have g1: "norm (g x) = 1" if "x \<in> T" and "b \<bullet> x = 0" for x
     using that
     apply (simp only: g_def)
     apply (rule power2_eq_imp_eq)
     apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps)
     apply (simp add: algebra_simps inner_commute)
     done
-  have [simp]: "b \<bullet> g x \<noteq> 1" if "x \<in> T" and "b \<bullet> x = 0" for x
+  have ne1: "b \<bullet> g x \<noteq> 1" if "x \<in> T" and "b \<bullet> x = 0" for x
     using that unfolding g_def
     apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps add_nonneg_eq_0_iff)
     apply (auto simp: algebra_simps)
     done
   have "subspace T"
     by (simp add: assms subspace_affine)
-  have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> g x \<in> T"
+  have gT: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> g x \<in> T"
     unfolding g_def
     by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
   have "f ` {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<subseteq> {x. b\<bullet>x = 0}"
@@ -540,14 +542,12 @@
     unfolding f_def using assms \<open>subspace T\<close>
     by (auto simp add: inner_add_right inner_diff_right mem_affine_3_minus subspace_mul)
   moreover have "{x. b\<bullet>x = 0} \<inter> T \<subseteq> f ` ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T)"
-    apply clarify
-    apply (rule_tac x = "g x" in image_eqI, auto)
-    done
+    by clarify (metis (mono_tags) IntI ne1 fg gT g1 imageI mem_Collect_eq)
   ultimately have imf: "f ` ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T) = {x. b\<bullet>x = 0} \<inter> T"
     by blast
   have no4: "\<And>y. b\<bullet>y = 0 \<Longrightarrow> norm ((y\<bullet>y + 4) *\<^sub>R b + 4 *\<^sub>R (y - 2 *\<^sub>R b)) = y\<bullet>y + 4"
     apply (rule power2_eq_imp_eq)
-    apply (simp_all add: dot_square_norm [symmetric])
+    apply (simp_all flip: dot_square_norm)
     apply (auto simp: power2_eq_square algebra_simps inner_commute)
     done
   have [simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> b \<bullet> f x = 0"
@@ -564,9 +564,7 @@
     unfolding g_def
     by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
   moreover have "{x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T \<subseteq> g ` ({x. b\<bullet>x = 0} \<inter> T)"
-    apply clarify
-    apply (rule_tac x = "f x" in image_eqI, auto)
-    done
+    by clarify (metis (mono_tags, lifting) IntI gf image_iff imf mem_Collect_eq)
   ultimately have img: "g ` ({x. b\<bullet>x = 0} \<inter> T) = {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T"
     by blast
   have aff: "affine ({x. b\<bullet>x = 0} \<inter> T)"
@@ -580,9 +578,10 @@
   also have "... homeomorphic {x. b\<bullet>x = 0} \<inter> T"
     by (rule homeomorphicI [OF imf img contf contg]) auto
   also have "... homeomorphic p"
-    apply (rule homeomorphic_affine_sets [OF aff \<open>affine p\<close>])
-    apply (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF \<open>affine T\<close>] affT)
-    done
+  proof (rule homeomorphic_affine_sets [OF aff \<open>affine p\<close>])
+    show "aff_dim ({x. b \<bullet> x = 0} \<inter> T) = aff_dim p"
+      by (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF \<open>affine T\<close>] affT)
+  qed
   finally show ?thesis .
 qed
 
@@ -603,10 +602,8 @@
   also have "... = sphere 0 1 \<inter> ((*\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}"
     using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
   also have "... homeomorphic p"
-    apply (rule homeomorphic_punctured_affine_sphere_affine_01)
     using assms affine_translation [symmetric, of "- a"] aff_dim_translation_eq [of "- a"]
-         apply (auto simp: dist_norm norm_minus_commute affine_scaling inj)
-    done
+    by (intro homeomorphic_punctured_affine_sphere_affine_01) (auto simp: dist_norm norm_minus_commute affine_scaling inj)
   finally show ?thesis .
 qed
 
@@ -620,12 +617,10 @@
 corollary homeomorphic_punctured_sphere_hyperplane:
   fixes a :: "'a :: euclidean_space"
   assumes "0 < r" and b: "b \<in> sphere a r"
-      and "c \<noteq> 0"
-    shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}"
-apply (rule homeomorphic_punctured_sphere_affine)
-using assms
-apply (auto simp: affine_hyperplane of_nat_diff)
-done
+    and "c \<noteq> 0"
+  shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}"
+  using assms
+  by (intro homeomorphic_punctured_sphere_affine) (auto simp: affine_hyperplane of_nat_diff)
 
 proposition homeomorphic_punctured_sphere_affine_gen:
   fixes a :: "'a :: euclidean_space"
@@ -711,60 +706,56 @@
                and keq:"k ` T = span ((+) (- a) ` S)"
                and hinv [simp]:  "\<And>x. x \<in> span ((+) (- a) ` S) \<Longrightarrow> k(h x) = x"
                and kinv [simp]:  "\<And>x. x \<in> T \<Longrightarrow> h(k x) = x"
-    apply (rule isometries_subspaces [OF _ \<open>subspace T\<close>])
-    apply (auto simp: dimT)
-    done
+    by (auto simp: dimT intro: isometries_subspaces [OF _ \<open>subspace T\<close>] dimT)
   have hcont: "continuous_on A h" and kcont: "continuous_on B k" for A B
     using \<open>linear h\<close> \<open>linear k\<close> linear_continuous_on linear_conv_bounded_linear by blast+
   have ihhhh[simp]: "\<And>x. x \<in> S \<Longrightarrow> i \<bullet> h (x - a) = 0"
     using Tsub [THEN subsetD] heq span_superset by fastforce
   have "sphere 0 1 - {i} homeomorphic {x. i \<bullet> x = 0}"
-    apply (rule homeomorphic_punctured_sphere_affine)
-    using i
-    apply (auto simp: affine_hyperplane)
-    by (metis DIM_positive Suc_eq_plus1 add.left_neutral diff_add_cancel not_le not_less_eq_eq of_nat_1 of_nat_diff)
+  proof (rule homeomorphic_punctured_sphere_affine)
+    show "affine {x. i \<bullet> x = 0}"
+      by (auto simp: affine_hyperplane)
+    show "aff_dim {x. i \<bullet> x = 0} + 1 = int DIM('n)"
+      using i by clarsimp (metis DIM_positive Suc_pred add.commute of_nat_Suc)
+  qed (use i in auto)
   then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i \<bullet> x = 0} f g"
     by (force simp: homeomorphic_def)
-  have "h ` (+) (- a) ` S \<subseteq> T"
-    using heq span_superset span_linear_image by blast
-  then have "g ` h ` (+) (- a) ` S \<subseteq> g ` {x. i \<bullet> x = 0}"
-    using Tsub by (simp add: image_mono)
-  also have "... \<subseteq> sphere 0 1 - {i}"
-    by (simp add: fg [unfolded homeomorphism_def])
-  finally have gh_sub_sph: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> sphere 0 1 - {i}"
-    by (metis image_comp)
-  then have gh_sub_cb: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> cball 0 1"
-    by (metis Diff_subset order_trans sphere_cball)
-  have [simp]: "\<And>u. u \<in> S \<Longrightarrow> norm (g (h (u - a))) = 1"
-    using gh_sub_sph [THEN subsetD] by (auto simp: o_def)
-  have ghcont: "continuous_on ((\<lambda>x. x - a) ` S) (\<lambda>x. g (h x))"
-    apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force)
-    done
-  have kfcont: "continuous_on ((\<lambda>x. g (h (x - a))) ` S) (\<lambda>x. k (f x))"
-    apply (rule continuous_on_compose2 [OF kcont])
-    using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast)
-    done
-  have "S homeomorphic (+) (- a) ` S"
-    by (fact homeomorphic_translation)
-  also have "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S"
-    apply (simp add: homeomorphic_def homeomorphism_def cong: image_cong_simp)
-    apply (rule_tac x="g \<circ> h" in exI)
-    apply (rule_tac x="k \<circ> f" in exI)
-    apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp cong: image_cong_simp)
-    done
-  finally have Shom: "S homeomorphic (\<lambda>x. g (h x)) ` (\<lambda>x. x - a) ` S"
-    by (simp cong: image_cong_simp)
   show ?thesis
-    apply (rule_tac U = "ball 0 1 \<union> image (g o h) ((+) (- a) ` S)"
-                and T = "image (g o h) ((+) (- a) ` S)"
-                    in that)
-    apply (rule convex_intermediate_ball [of 0 1], force)
-    using gh_sub_cb apply force
-    apply force
-    apply (simp add: closedin_closed)
-    apply (rule_tac x="sphere 0 1" in exI)
-     apply (auto simp: Shom cong: image_cong_simp)
-    done
+  proof
+    have "h ` (+) (- a) ` S \<subseteq> T"
+      using heq span_superset span_linear_image by blast
+    then have "g ` h ` (+) (- a) ` S \<subseteq> g ` {x. i \<bullet> x = 0}"
+      using Tsub by (simp add: image_mono)
+    also have "... \<subseteq> sphere 0 1 - {i}"
+      by (simp add: fg [unfolded homeomorphism_def])
+    finally have gh_sub_sph: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> sphere 0 1 - {i}"
+      by (metis image_comp)
+    then have gh_sub_cb: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> cball 0 1"
+      by (metis Diff_subset order_trans sphere_cball)
+    have [simp]: "\<And>u. u \<in> S \<Longrightarrow> norm (g (h (u - a))) = 1"
+      using gh_sub_sph [THEN subsetD] by (auto simp: o_def)
+    show "convex (ball 0 1 \<union> (g \<circ> h) ` (+) (- a) ` S)"
+      by (meson ball_subset_cball convex_intermediate_ball gh_sub_cb sup.bounded_iff sup.cobounded1)
+    show "closedin (top_of_set (ball 0 1 \<union> (g \<circ> h) ` (+) (- a) ` S)) ((g \<circ> h) ` (+) (- a) ` S)"
+      unfolding closedin_closed
+      by (rule_tac x="sphere 0 1" in exI) auto
+    have ghcont: "continuous_on ((\<lambda>x. x - a) ` S) (\<lambda>x. g (h x))"
+      by (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force)
+    have kfcont: "continuous_on ((\<lambda>x. g (h (x - a))) ` S) (\<lambda>x. k (f x))"
+    proof (rule continuous_on_compose2 [OF kcont])
+      show "continuous_on ((\<lambda>x. g (h (x - a))) ` S) f"
+        using homeomorphism_cont1 [OF fg] gh_sub_sph by (fastforce intro: continuous_on_subset)
+    qed auto
+    have "S homeomorphic (+) (- a) ` S"
+      by (fact homeomorphic_translation)
+    also have "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S"
+      apply (simp add: homeomorphic_def homeomorphism_def cong: image_cong_simp)
+      apply (rule_tac x="g \<circ> h" in exI)
+      apply (rule_tac x="k \<circ> f" in exI)
+      apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp cong: image_cong_simp)
+      done
+    finally show "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" .
+  qed auto
 qed
 
 subsection\<open>Locally compact sets in an open set\<close>
@@ -790,10 +781,7 @@
   also have "... = \<Union>(t ` S) \<inter> closure S"
   proof
     show "\<Union>(v ` S) \<subseteq> \<Union>(t ` S) \<inter> closure S"
-      apply safe
-       apply (metis Int_iff subsetD UN_iff tv)
-      apply (simp add: closure_def rev_subsetD tv)
-      done
+      by clarify (meson IntD2 IntI UN_I closure_subset subsetD tv)
     have "t x \<inter> closure S \<subseteq> v x" if "x \<in> S" for x
     proof -
       have "t x \<inter> closure S \<subseteq> closure (t x \<inter> S)"
@@ -821,13 +809,14 @@
 lemma locally_compact_homeomorphism_projection_closed:
   assumes "locally compact S"
   obtains T and f :: "'a \<Rightarrow> 'a :: euclidean_space \<times> 'b :: euclidean_space"
-    where "closed T" "homeomorphism S T f fst"
+  where "closed T" "homeomorphism S T f fst"
 proof (cases "closed S")
   case True
-    then show ?thesis
-      apply (rule_tac T = "S \<times> {0}" and f = "\<lambda>x. (x, 0)" in that)
-      apply (auto simp: closed_Times homeomorphism_def continuous_intros)
-      done
+  show ?thesis
+  proof
+    show "homeomorphism S (S \<times> {0}) (\<lambda>x. (x, 0)) fst"
+      by (auto simp: homeomorphism_def continuous_intros)
+  qed (use True closed_Times in auto)
 next
   case False
     obtain U where "open U" and US: "U \<inter> closure S = S"
@@ -838,8 +827,10 @@
       by (simp add: \<open>open U\<close> closed_Compl)
     define f :: "'a \<Rightarrow> 'a \<times> 'b" where "f \<equiv> \<lambda>x. (x, One /\<^sub>R setdist {x} (- U))"
     have "continuous_on U (\<lambda>x. (x, One /\<^sub>R setdist {x} (- U)))"
-      apply (intro continuous_intros continuous_on_setdist)
-      by (simp add: Ucomp setdist_eq_0_sing_1)
+    proof (intro continuous_intros continuous_on_setdist)
+      show "\<forall>x\<in>U. setdist {x} (- U) \<noteq> 0"
+        by (simp add: Ucomp setdist_eq_0_sing_1)
+    qed
     then have homU: "homeomorphism U (f`U) f fst"
       by (auto simp: f_def homeomorphism_def image_iff continuous_intros)
     have cloS: "closedin (top_of_set U) S"
@@ -850,33 +841,27 @@
       by force
     have *: "r *\<^sub>R b = One \<Longrightarrow> b = (1 / r) *\<^sub>R One" for r and b::'b
       by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
-    have "f ` U = (\<lambda>z. (setdist {fst z} (- U) *\<^sub>R snd z)) -` {One}"
-      apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
-      apply (rule_tac x=a in image_eqI)
-      apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D)
-      done
+    have "\<And>a b::'b. setdist {a} (- U) *\<^sub>R b = One \<Longrightarrow> (a,b) \<in> (\<lambda>x. (x, (1 / setdist {x} (- U)) *\<^sub>R One)) ` U"
+      by (metis (mono_tags, lifting) "*" ComplI image_eqI setdist1D setdist_sing_in_set)
+    then have "f ` U = (\<lambda>z. (setdist {fst z} (- U) *\<^sub>R snd z)) -` {One}"
+      by (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
     then have clfU: "closed (f ` U)"
-      apply (rule ssubst)
-      apply (rule continuous_closed_vimage)
-      apply (auto intro: continuous_intros cont [unfolded o_def])
-      done
+      by (force intro: continuous_intros cont [unfolded o_def] continuous_closed_vimage)
     have "closed (f ` S)"
-       apply (rule closedin_closed_trans [OF _ clfU])
-       apply (rule homeomorphism_imp_closed_map [OF homU cloS])
-       done
+      by (metis closedin_closed_trans [OF _ clfU] homeomorphism_imp_closed_map [OF homU cloS])
     then show ?thesis
-      apply (rule that)
-      apply (rule homeomorphism_of_subsets [OF homU])
-      using US apply auto
-      done
+      by (metis US homU homeomorphism_of_subsets inf_sup_ord(1) that)
 qed
 
 lemma locally_compact_closed_Int_open:
   fixes S :: "'a :: euclidean_space set"
-  shows
-    "locally compact S \<longleftrightarrow> (\<exists>U u. closed U \<and> open u \<and> S = U \<inter> u)"
-by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact)
-
+  shows "locally compact S \<longleftrightarrow> (\<exists>U V. closed U \<and> open V \<and> S = U \<inter> V)" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (metis closed_closure inf_commute locally_compact_open_Int_closure)
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (meson closed_imp_locally_compact locally_compact_Int open_imp_locally_compact)
+qed
 
 lemma lowerdim_embeddings:
   assumes  "DIM('a) < DIM('b)"
@@ -910,17 +895,17 @@
       by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps)
     have *: "(\<Sum>a \<in> Basis. a \<bullet> basf b * (x \<bullet> basg a)) = x \<bullet> b" if "b \<in> Basis" for x b
       using sbf that by auto
-    show gf: "g (f x) = x" for x
-      apply (rule euclidean_eqI)
-      apply (simp add: f_def g_def inner_sum_left scaleR_sum_left algebra_simps)
-      apply (simp add: Groups_Big.sum_distrib_left [symmetric] *)
-      done
+    show gf: "g (f x) = x" for x      
+    proof (rule euclidean_eqI)
+      show "\<And>b. b \<in> Basis \<Longrightarrow> g (f x) \<bullet> b = x \<bullet> b"
+        using f_def g_def sbf by auto
+    qed
     show "basf(0,1) \<in> Basis"
       using b01 sbf by auto
     then show "f(x,0) \<bullet> basf(0,1) = 0" for x
-      apply (simp add: f_def inner_sum_left)
-      apply (rule comm_monoid_add_class.sum.neutral)
-      using b01 inner_not_same_Basis by fastforce
+      unfolding f_def inner_sum_left
+      using b01 inner_not_same_Basis 
+      by (fastforce intro: comm_monoid_add_class.sum.neutral)
   qed
 qed
 
@@ -942,15 +927,14 @@
   have "S homeomorphic U"
     using homU homeomorphic_def by blast
   also have "... homeomorphic f ` U"
-    apply (rule homeomorphicI [OF refl gfU])
-       apply (meson \<open>inj f\<close> \<open>linear f\<close> homeomorphism_cont2 linear_homeomorphism_image)
-    using \<open>linear g\<close> linear_continuous_on linear_conv_bounded_linear apply blast
-    apply (auto simp: o_def)
-    done
+  proof (rule homeomorphicI [OF refl gfU])
+    show "continuous_on U f"
+      by (meson \<open>inj f\<close> \<open>linear f\<close> homeomorphism_cont2 linear_homeomorphism_image)
+    show "continuous_on (f ` U) g"
+      using \<open>linear g\<close> linear_continuous_on linear_conv_bounded_linear by blast
+  qed (auto simp: o_def)
   finally show ?thesis
-    apply (rule_tac T = "f ` U" in that)
-    apply (rule closed_injective_linear_image [OF \<open>closed U\<close> \<open>linear f\<close> \<open>inj f\<close>], assumption)
-    done
+    using \<open>closed U\<close> \<open>inj f\<close> \<open>linear f\<close> closed_injective_linear_image that by blast
 qed
 
 
@@ -989,38 +973,15 @@
 proposition homeomorphic_convex_compact_cball:
   fixes e :: real
     and S :: "'a::euclidean_space set"
-  assumes "convex S"
-    and "compact S"
-    and "interior S \<noteq> {}"
-    and "e > 0"
+  assumes S: "convex S" "compact S" "interior S \<noteq> {}" and "e > 0"
   shows "S homeomorphic (cball (b::'a) e)"
-proof -
+proof (rule homeomorphic_trans[OF _ homeomorphic_balls(2)])
   obtain a where "a \<in> interior S"
-    using assms(3) by auto
-  then obtain d where "d > 0" and d: "cball a d \<subseteq> S"
-    unfolding mem_interior_cball by auto
-  let ?d = "inverse d" and ?n = "0::'a"
-  have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` S"
-    apply rule
-    apply (rule_tac x="d *\<^sub>R x + a" in image_eqI)
-    defer
-    apply (rule d[unfolded subset_eq, rule_format])
-    using \<open>d > 0\<close>
-    unfolding mem_cball dist_norm
-    apply (auto simp add: mult_right_le_one_le)
-    done
-  then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` S homeomorphic cball ?n 1"
-    using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` S",
-      OF convex_affinity compact_affinity]
-    using assms(1,2)
-    by (auto simp add: scaleR_right_diff_distrib)
-  then show ?thesis
-    apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
-    apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" S "?d *\<^sub>R -a"]])
-    using \<open>d>0\<close> \<open>e>0\<close>
-    apply (auto simp add: scaleR_right_diff_distrib)
-    done
-qed
+    using assms by auto
+  then show "S homeomorphic cball (0::'a) 1"
+    by (metis (no_types) aff_dim_cball S compact_cball convex_cball 
+        homeomorphic_convex_lemma interior_rel_interior_gen zero_less_one)
+qed (use \<open>e>0\<close> in auto)
 
 corollary homeomorphic_convex_compact:
   fixes S :: "'a::euclidean_space set"
@@ -1035,9 +996,7 @@
   fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
   assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
     shows "(cbox a b) homeomorphic (cbox c d)"
-apply (rule homeomorphic_convex_compact)
-using assms apply auto
-done
+  by (simp add: assms homeomorphic_convex_compact)
 
 lemma homeomorphic_closed_intervals_real:
   fixes a::real and b and c::real and d
@@ -1065,7 +1024,7 @@
   by (simp add: covering_space_def)
 
 lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
-  apply (simp add: homeomorphism_def covering_space_def, clarify)
+  apply (clarsimp simp add: homeomorphism_def covering_space_def)
   apply (rule_tac x=T in exI, simp)
   apply (rule_tac x="{S}" in exI, auto)
   done
@@ -1075,10 +1034,8 @@
   obtains T u q where "x \<in> T" "openin (top_of_set c) T"
                       "p x \<in> u" "openin (top_of_set S) u"
                       "homeomorphism T u p q"
-using assms
-apply (simp add: covering_space_def, clarify)
-  apply (drule_tac x="p x" in bspec, force)
-  by (metis IntI UnionE vimage_eq) 
+  using assms
+  by (clarsimp simp add: covering_space_def) (metis IntI UnionE vimage_eq) 
 
 
 lemma covering_space_local_homeomorphism_alt:
@@ -1091,8 +1048,7 @@
   obtain x where "p x = y" "x \<in> c"
     using assms covering_space_imp_surjective by blast
   show ?thesis
-    apply (rule covering_space_local_homeomorphism [OF p \<open>x \<in> c\<close>])
-    using that \<open>p x = y\<close> by blast
+    using that \<open>p x = y\<close> by (auto intro: covering_space_local_homeomorphism [OF p \<open>x \<in> c\<close>])
 qed
 
 proposition covering_space_open_map:
@@ -1120,7 +1076,6 @@
                   and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
       using covs [OF \<open>y \<in> S\<close>] by auto
     obtain x where "x \<in> c" "p x \<in> U" "x \<in> T" "p x = y"
-      apply simp
       using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast
     with VS obtain V where "x \<in> V" "V \<in> VS" by auto
     then obtain q where q: "homeomorphism V U p q" using homVS by blast
@@ -1128,19 +1083,18 @@
       using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
     have ocv: "openin (top_of_set c) V"
       by (simp add: \<open>V \<in> VS\<close> openVS)
-    have "openin (top_of_set U) (U \<inter> q -` (T \<inter> V))"
-      apply (rule continuous_on_open [THEN iffD1, rule_format])
-       using homeomorphism_def q apply blast
-      using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def
-      by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
+    have "openin (top_of_set (q ` U)) (T \<inter> V)"
+      using q unfolding homeomorphism_def
+      by (metis T inf.absorb_iff2 ocv openin_imp_subset openin_subtopology_Int subtopology_subtopology)
+    then have "openin (top_of_set U) (U \<inter> q -` (T \<inter> V))"
+      using continuous_on_open homeomorphism_def q by blast
     then have os: "openin (top_of_set S) (U \<inter> q -` (T \<inter> V))"
       using openin_trans [of U] by (simp add: Collect_conj_eq U)
     show ?thesis
-      apply (rule_tac x = "p ` (T \<inter> V)" in exI)
-      apply (rule conjI)
-      apply (simp only: ptV os)
-      using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> T\<close> apply blast
-      done
+    proof (intro exI conjI)
+      show "openin (top_of_set S) (p ` (T \<inter> V))"
+        by (simp only: ptV os)
+    qed (use \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> T\<close> in auto)
   qed
   with openin_subopen show ?thesis by blast
 qed
@@ -1169,11 +1123,12 @@
     fix z
     assume z: "z \<in> U" "g1 z - g2 z = 0"
     obtain v w q where "g1 z \<in> v" and ocv: "openin (top_of_set c) v"
-                   and "p (g1 z) \<in> w" and osw: "openin (top_of_set S) w"
-                   and hom: "homeomorphism v w p q"
-      apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov])
-       using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+
-      done
+      and "p (g1 z) \<in> w" and osw: "openin (top_of_set S) w"
+      and hom: "homeomorphism v w p q"
+    proof (rule covering_space_local_homeomorphism [OF cov])
+      show "g1 z \<in> c"
+        using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) by blast
+    qed auto
     have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
     have gg: "U \<inter> g -` v = U \<inter> g -` (v \<inter> g ` U)" for g
       by auto
@@ -1185,14 +1140,17 @@
       using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open)
     then have 2: "openin (top_of_set U) (U \<inter> g2 -` v)"
       unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
+    let ?T = "(U \<inter> g1 -` v) \<inter> (U \<inter> g2 -` v)"
     show "\<exists>T. openin (top_of_set U) T \<and> z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
-      using z
-      apply (rule_tac x = "(U \<inter> g1 -` v) \<inter> (U \<inter> g2 -` v)" in exI)
-      apply (intro conjI)
-      apply (rule openin_Int [OF 1 2])
-      using \<open>g1 z \<in> v\<close>  \<open>g2 z \<in> v\<close>  apply (force simp:, clarify)
-      apply (metis \<open>U \<subseteq> T\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
-      done
+    proof (intro exI conjI)
+      show "openin (top_of_set U) ?T"
+        using "1" "2" by blast
+      show "z \<in> ?T"
+        using z by (simp add: \<open>g1 z \<in> v\<close> \<open>g2 z \<in> v\<close>)
+      show "?T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
+        using hom 
+        by (clarsimp simp: homeomorphism_def) (metis \<open>U \<subseteq> T\<close> fg1 fg2 subsetD)
+    qed
   qed
   have c12: "closedin (top_of_set U) G12"
     unfolding G12_def
@@ -1224,10 +1182,12 @@
     shows "locally \<psi> S"
 proof -
   have "locally \<psi> (p ` C)"
-    apply (rule locally_open_map_image [OF loc])
-    using cov covering_space_imp_continuous apply blast
-    using cov covering_space_imp_surjective covering_space_open_map apply blast
-    by (simp add: pim)
+  proof (rule locally_open_map_image [OF loc])
+    show "continuous_on C p"
+      using cov covering_space_imp_continuous by blast
+    show "\<And>T. openin (top_of_set C) T \<Longrightarrow> openin (top_of_set (p ` C)) (p ` T)"
+      using cov covering_space_imp_surjective covering_space_open_map by blast
+  qed (simp add: pim)
   then show ?thesis
     using covering_space_imp_surjective [OF cov] by metis
 qed
@@ -1299,25 +1259,28 @@
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "covering_space C p S"
   shows "locally compact S \<longleftrightarrow> locally compact C"
-  apply (rule covering_space_locally_eq [OF assms])
-   apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
-  using compact_continuous_image by blast
+proof (rule covering_space_locally_eq [OF assms])
+  show "\<And>T. \<lbrakk>T \<subseteq> C; compact T\<rbrakk> \<Longrightarrow> compact (p ` T)"
+    by (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
+qed (use compact_continuous_image in blast)
 
 lemma covering_space_locally_connected_eq:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "covering_space C p S"
     shows "locally connected S \<longleftrightarrow> locally connected C"
-  apply (rule covering_space_locally_eq [OF assms])
-   apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
-  using connected_continuous_image by blast
+proof (rule covering_space_locally_eq [OF assms])
+  show "\<And>T. \<lbrakk>T \<subseteq> C; connected T\<rbrakk> \<Longrightarrow> connected (p ` T)"
+    by (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
+qed (use connected_continuous_image in blast)
 
 lemma covering_space_locally_path_connected_eq:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "covering_space C p S"
     shows "locally path_connected S \<longleftrightarrow> locally path_connected C"
-  apply (rule covering_space_locally_eq [OF assms])
-   apply (meson path_connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
-  using path_connected_continuous_image by blast
+proof (rule covering_space_locally_eq [OF assms])
+  show "\<And>T. \<lbrakk>T \<subseteq> C; path_connected T\<rbrakk> \<Longrightarrow> path_connected (p ` T)"
+    by (meson path_connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
+qed (use path_connected_continuous_image in blast)
 
 
 lemma covering_space_locally_compact:
@@ -1436,18 +1399,18 @@
       case (Suc n)
       then obtain V k where opeUV: "openin (top_of_set U) V"
                         and "y \<in> V"
-                        and contk: "continuous_on ({0..real n / real N} \<times> V) k"
-                        and kim: "k ` ({0..real n / real N} \<times> V) \<subseteq> C"
+                        and contk: "continuous_on ({0..n/N} \<times> V) k"
+                        and kim: "k ` ({0..n/N} \<times> V) \<subseteq> C"
                         and keq: "\<And>z. z \<in> V \<Longrightarrow> k (0, z) = f z"
-                        and heq: "\<And>z. z \<in> {0..real n / real N} \<times> V \<Longrightarrow> h z = p (k z)"
+                        and heq: "\<And>z. z \<in> {0..n/N} \<times> V \<Longrightarrow> h z = p (k z)"
         using Suc_leD by auto
       have "n \<le> N"
         using Suc.prems by auto
-      obtain t where "t \<in> tk" and t: "{real n / real N .. (1 + real n) / real N} \<subseteq> K t"
+      obtain t where "t \<in> tk" and t: "{n/N .. (1 + real n) / N} \<subseteq> K t"
       proof (rule bexE [OF \<delta>])
-        show "{real n / real N .. (1 + real n) / real N} \<subseteq> {0..1}"
+        show "{n/N .. (1 + real n) / N} \<subseteq> {0..1}"
           using Suc.prems by (auto simp: field_split_simps)
-        show diameter_less: "diameter {real n / real N .. (1 + real n) / real N} < \<delta>"
+        show diameter_less: "diameter {n/N .. (1 + real n) / N} < \<delta>"
           using \<open>0 < \<delta>\<close> N by (auto simp: field_split_simps)
       qed blast
       have t01: "t \<in> {0..1}"
@@ -1457,28 +1420,26 @@
                  and "pairwise disjnt \<V>"
                  and homuu: "\<And>U. U \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism U (UU (X t)) p q"
         using inUS [OF t01] UU by meson
-      have n_div_N_in: "real n / real N \<in> {real n / real N .. (1 + real n) / real N}"
+      have n_div_N_in: "n/N \<in> {n/N .. (1 + real n) / N}"
         using N by (auto simp: field_split_simps)
-      with t have nN_in_kkt: "real n / real N \<in> K t"
+      with t have nN_in_kkt: "n/N \<in> K t"
         by blast
-      have "k (real n / real N, y) \<in> C \<inter> p -` UU (X t)"
+      have "k (n/N, y) \<in> C \<inter> p -` UU (X t)"
       proof (simp, rule conjI)
-        show "k (real n / real N, y) \<in> C"
+        show "k (n/N, y) \<in> C"
           using \<open>y \<in> V\<close> kim keq by force
-        have "p (k (real n / real N, y)) = h (real n / real N, y)"
+        have "p (k (n/N, y)) = h (n/N, y)"
           by (simp add: \<open>y \<in> V\<close> heq)
         also have "... \<in> h ` (({0..1} \<inter> K t) \<times> (U \<inter> NN t))"
-          apply (rule imageI)
            using \<open>y \<in> V\<close> t01 \<open>n \<le> N\<close>
-          apply (simp add: nN_in_kkt \<open>y \<in> U\<close> inUS field_split_simps)
-          done
+           by (simp add: nN_in_kkt \<open>y \<in> U\<close> inUS field_split_simps)
         also have "... \<subseteq> UU (X t)"
           using him t01 by blast
-        finally show "p (k (real n / real N, y)) \<in> UU (X t)" .
+        finally show "p (k (n/N, y)) \<in> UU (X t)" .
       qed
-      with \<V> have "k (real n / real N, y) \<in> \<Union>\<V>"
+      with \<V> have "k (n/N, y) \<in> \<Union>\<V>"
         by blast
-      then obtain W where W: "k (real n / real N, y) \<in> W" and "W \<in> \<V>"
+      then obtain W where W: "k (n/N, y) \<in> W" and "W \<in> \<V>"
         by blast
       then obtain p' where opeC': "openin (top_of_set C) W"
                        and hom': "homeomorphism W (UU (X t)) p p'"
@@ -1487,15 +1448,18 @@
         using openin_imp_subset by blast
       define W' where "W' = UU(X t)"
       have opeVW: "openin (top_of_set V) (V \<inter> (k \<circ> Pair (n / N)) -` W)"
-        apply (rule continuous_openin_preimage [OF _ _ opeC'])
-         apply (intro continuous_intros continuous_on_subset [OF contk])
-        using kim apply (auto simp: \<open>y \<in> V\<close> W)
-        done
+      proof (rule continuous_openin_preimage [OF _ _ opeC'])
+        show "continuous_on V (k \<circ> Pair (n/N))"
+          by (intro continuous_intros continuous_on_subset [OF contk], auto)
+        show "(k \<circ> Pair (n/N)) ` V \<subseteq> C"
+          using kim by (auto simp: \<open>y \<in> V\<close> W)
+      qed
       obtain N' where opeUN': "openin (top_of_set U) N'"
-                  and "y \<in> N'" and kimw: "k ` ({(real n / real N)} \<times> N') \<subseteq> W"
-        apply (rule_tac N' = "(V \<inter> (k \<circ> Pair (n / N)) -` W)" in that)
-        apply (fastforce simp:  \<open>y \<in> V\<close> W intro!: openin_trans [OF opeVW opeUV])+
-        done
+                and "y \<in> N'" and kimw: "k ` ({(n/N)} \<times> N') \<subseteq> W"
+      proof
+        show "openin (top_of_set U) (V \<inter> (k \<circ> Pair (n/N)) -` W)"
+          using opeUV opeVW openin_trans by blast
+      qed (use \<open>y \<in> V\<close> W in \<open>force+\<close>)
       obtain Q Q' where opeUQ: "openin (top_of_set U) Q"
                     and cloUQ': "closedin (top_of_set U) Q'"
                     and "y \<in> Q" "Q \<subseteq> Q'"
@@ -1517,68 +1481,78 @@
       qed
       then have "y \<in> Q'" "Q \<subseteq> (U \<inter> NN(t)) \<inter> N' \<inter> V"
         by blast+
-      have neq: "{0..real n / real N} \<union> {real n / real N..(1 + real n) / real N} = {0..(1 + real n) / real N}"
+      have neq: "{0..n/N} \<union> {n/N..(1 + real n) / N} = {0..(1 + real n) / N}"
         apply (auto simp: field_split_simps)
         by (metis mult_zero_left of_nat_0_le_iff of_nat_0_less_iff order_trans real_mult_le_cancel_iff1)
-      then have neqQ': "{0..real n / real N} \<times> Q' \<union> {real n / real N..(1 + real n) / real N} \<times> Q' = {0..(1 + real n) / real N} \<times> Q'"
+      then have neqQ': "{0..n/N} \<times> Q' \<union> {n/N..(1 + real n) / N} \<times> Q' = {0..(1 + real n) / N} \<times> Q'"
         by blast
-      have cont: "continuous_on ({0..(1 + real n) / real N} \<times> Q')
-        (\<lambda>x. if x \<in> {0..real n / real N} \<times> Q' then k x else (p' \<circ> h) x)"
+      have cont: "continuous_on ({0..(1 + real n) / N} \<times> Q') (\<lambda>x. if x \<in> {0..n/N} \<times> Q' then k x else (p' \<circ> h) x)"
         unfolding neqQ' [symmetric]
       proof (rule continuous_on_cases_local, simp_all add: neqQ' del: comp_apply)
-        show "closedin (top_of_set ({0..(1 + real n) / real N} \<times> Q'))
-                       ({0..real n / real N} \<times> Q')"
-          apply (simp add: closedin_closed)
-          apply (rule_tac x="{0 .. real n / real N} \<times> UNIV" in exI)
-          using n_div_N_in apply (auto simp: closed_Times)
-          done
-        show "closedin (top_of_set ({0..(1 + real n) / real N} \<times> Q'))
-                       ({real n / real N..(1 + real n) / real N} \<times> Q')"
-          apply (simp add: closedin_closed)
-          apply (rule_tac x="{real n / real N .. (1 + real n) / real N} \<times> UNIV" in exI)
-          apply (auto simp: closed_Times)
-          by (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans)
-        show "continuous_on ({0..real n / real N} \<times> Q') k"
-          apply (rule continuous_on_subset [OF contk])
-          using Q' by auto
-        have "continuous_on ({real n / real N..(1 + real n) / real N} \<times> Q') h"
+        have "\<exists>T. closed T \<and> {0..n/N} \<times> Q' = {0..(1+n)/N} \<times> Q' \<inter> T"
+          using n_div_N_in 
+          by (rule_tac x="{0 .. n/N} \<times> UNIV" in exI) (auto simp: closed_Times)
+        then show "closedin (top_of_set ({0..(1 + real n) / N} \<times> Q')) ({0..n/N} \<times> Q')"
+          by (simp add: closedin_closed)
+        have "\<exists>T. closed T \<and> {n/N..(1+n)/N} \<times> Q' = {0..(1+n)/N} \<times> Q' \<inter> T"
+          by (rule_tac x="{n/N..(1+n)/N} \<times> UNIV" in exI) (auto simp: closed_Times order_trans [rotated])
+        then show "closedin (top_of_set ({0..(1 + real n) / N} \<times> Q')) ({n/N..(1 + real n) / N} \<times> Q')"
+          by (simp add: closedin_closed)
+        show "continuous_on ({0..n/N} \<times> Q') k"
+          using Q' by (auto intro: continuous_on_subset [OF contk])
+        have "continuous_on ({n/N..(1 + real n) / N} \<times> Q') h"
         proof (rule continuous_on_subset [OF conth])
-          show "{real n / real N..(1 + real n) / real N} \<times> Q' \<subseteq> {0..1} \<times> U"
-            using \<open>N > 0\<close>
-            apply auto
-              apply (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans)
-            using Suc.prems order_trans apply fastforce
-            apply (metis IntE  cloUQ' closedin_closed)
-            done
+          show "{n/N..(1 + real n) / N} \<times> Q' \<subseteq> {0..1} \<times> U"
+          proof (clarsimp, intro conjI)
+            fix a b
+            assume "b \<in> Q'" and a: "n/N \<le> a" "a \<le> (1 + real n) / N"
+            have "0 \<le> n/N" "(1 + real n) / N \<le> 1"
+              using a Suc.prems by (auto simp: divide_simps)
+            with a show "0 \<le> a"  "a \<le> 1"
+              by linarith+
+            show "b \<in> U"
+              using \<open>b \<in> Q'\<close> cloUQ' closedin_imp_subset by blast
+          qed
         qed
-        moreover have "continuous_on (h ` ({real n / real N..(1 + real n) / real N} \<times> Q')) p'"
+        moreover have "continuous_on (h ` ({n/N..(1 + real n) / N} \<times> Q')) p'"
         proof (rule continuous_on_subset [OF homeomorphism_cont2 [OF hom']])
-          have "h ` ({real n / real N..(1 + real n) / real N} \<times> Q') \<subseteq> h ` (({0..1} \<inter> K t) \<times> (U \<inter> NN t))"
-            apply (rule image_mono)
-            using \<open>0 < \<delta>\<close> \<open>N > 0\<close> Suc.prems apply auto
-              apply (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans)
-            using Suc.prems order_trans apply fastforce
-            using t Q' apply auto
-            done
-          with him show "h ` ({real n / real N..(1 + real n) / real N} \<times> Q') \<subseteq> UU (X t)"
+          have "h ` ({n/N..(1 + real n) / N} \<times> Q') \<subseteq> h ` (({0..1} \<inter> K t) \<times> (U \<inter> NN t))"
+          proof (rule image_mono)
+            show "{n/N..(1 + real n) / N} \<times> Q' \<subseteq> ({0..1} \<inter> K t) \<times> (U \<inter> NN t)"
+            proof (clarsimp, intro conjI)
+              fix a::real and b
+              assume "b \<in> Q'" "n/N \<le> a" "a \<le> (1 + real n) / N"
+              show "0 \<le> a"
+                by (meson \<open>n/N \<le> a\<close> divide_nonneg_nonneg of_nat_0_le_iff order_trans)
+              show "a \<le> 1"
+                using Suc.prems \<open>a \<le> (1 + real n) / N\<close> order_trans by force
+              show "a \<in> K t"
+                using \<open>a \<le> (1 + real n) / N\<close> \<open>n/N \<le> a\<close> t by auto
+              show "b \<in> U"
+                using \<open>b \<in> Q'\<close> cloUQ' closedin_imp_subset by blast
+              show "b \<in> NN t"
+                using Q' \<open>b \<in> Q'\<close> by auto
+            qed
+          qed
+          with him show "h ` ({n/N..(1 + real n) / N} \<times> Q') \<subseteq> UU (X t)"
             using t01 by blast
         qed
-        ultimately show "continuous_on ({real n / real N..(1 + real n) / real N} \<times> Q') (p' \<circ> h)"
+        ultimately show "continuous_on ({n/N..(1 + real n) / N} \<times> Q') (p' \<circ> h)"
           by (rule continuous_on_compose)
-        have "k (real n / real N, b) = p' (h (real n / real N, b))" if "b \<in> Q'" for b
+        have "k (n/N, b) = p' (h (n/N, b))" if "b \<in> Q'" for b
         proof -
-          have "k (real n / real N, b) \<in> W"
+          have "k (n/N, b) \<in> W"
             using that Q' kimw  by force
-          then have "k (real n / real N, b) = p' (p (k (real n / real N, b)))"
+          then have "k (n/N, b) = p' (p (k (n/N, b)))"
             by (simp add:  homeomorphism_apply1 [OF hom'])
           then show ?thesis
             using Q' that by (force simp: heq)
         qed
-        then show "\<And>x. x \<in> {real n / real N..(1 + real n) / real N} \<times> Q' \<and>
-                  x \<in> {0..real n / real N} \<times> Q' \<Longrightarrow> k x = (p' \<circ> h) x"
+        then show "\<And>x. x \<in> {n/N..(1 + real n) / N} \<times> Q' \<and>
+                  x \<in> {0..n/N} \<times> Q' \<Longrightarrow> k x = (p' \<circ> h) x"
           by auto
       qed
-      have h_in_UU: "h (x, y) \<in> UU (X t)" if "y \<in> Q" "\<not> x \<le> real n / real N" "0 \<le> x" "x \<le> (1 + real n) / real N" for x y
+      have h_in_UU: "h (x, y) \<in> UU (X t)" if "y \<in> Q" "\<not> x \<le> n/N" "0 \<le> x" "x \<le> (1 + real n) / N" for x y
       proof -
         have "x \<le> 1"
           using Suc.prems that order_trans by force
@@ -1596,31 +1570,29 @@
           by (metis him t01)
         finally show ?thesis .
       qed
-      let ?k = "(\<lambda>x. if x \<in> {0..real n / real N} \<times> Q' then k x else (p' \<circ> h) x)"
+      let ?k = "(\<lambda>x. if x \<in> {0..n/N} \<times> Q' then k x else (p' \<circ> h) x)"
       show ?case
       proof (intro exI conjI)
-        show "continuous_on ({0..real (Suc n) / real N} \<times> Q) ?k"
-          apply (rule continuous_on_subset [OF cont])
-          using \<open>Q \<subseteq> Q'\<close> by auto
-        have "\<And>a b. \<lbrakk>a \<le> real n / real N; b \<in> Q'; 0 \<le> a\<rbrakk> \<Longrightarrow> k (a, b) \<in> C"
+        show "continuous_on ({0..real (Suc n) / N} \<times> Q) ?k"
+          using \<open>Q \<subseteq> Q'\<close> by (auto intro: continuous_on_subset [OF cont])
+        have "\<And>x y. \<lbrakk>x \<le> n/N; y \<in> Q'; 0 \<le> x\<rbrakk> \<Longrightarrow> k (x, y) \<in> C"
           using kim Q' by force
-        moreover have "\<And>a b. \<lbrakk>b \<in> Q; 0 \<le> a; a \<le> (1 + real n) / real N; \<not> a \<le> real n / real N\<rbrakk> \<Longrightarrow> p' (h (a, b)) \<in> C"
-          apply (rule \<open>W \<subseteq> C\<close> [THEN subsetD])
-          using homeomorphism_image2 [OF hom', symmetric]  h_in_UU  Q' \<open>Q \<subseteq> Q'\<close> \<open>W \<subseteq> C\<close>
-          apply auto
-          done
-        ultimately show "?k ` ({0..real (Suc n) / real N} \<times> Q) \<subseteq> C"
+        moreover have "p' (h (x, y)) \<in> C" if "y \<in> Q" "\<not> x \<le> n/N" "0 \<le> x" "x \<le> (1 + real n) / N" for x y
+        proof (rule \<open>W \<subseteq> C\<close> [THEN subsetD])
+          show "p' (h (x, y)) \<in> W"
+            using homeomorphism_image2 [OF hom', symmetric]  h_in_UU  Q' \<open>Q \<subseteq> Q'\<close> \<open>W \<subseteq> C\<close> that by auto
+        qed
+        ultimately show "?k ` ({0..real (Suc n) / N} \<times> Q) \<subseteq> C"
           using Q' \<open>Q \<subseteq> Q'\<close> by force
         show "\<forall>z\<in>Q. ?k (0, z) = f z"
           using Q' keq  \<open>Q \<subseteq> Q'\<close> by auto
-        show "\<forall>z \<in> {0..real (Suc n) / real N} \<times> Q. h z = p(?k z)"
-          using \<open>Q \<subseteq> U \<inter> NN t \<inter> N' \<inter> V\<close> heq apply clarsimp
-          using h_in_UU Q' \<open>Q \<subseteq> Q'\<close> apply (auto simp: homeomorphism_apply2 [OF hom', symmetric])
-          done
+        show "\<forall>z \<in> {0..real (Suc n) / N} \<times> Q. h z = p(?k z)"
+          using \<open>Q \<subseteq> U \<inter> NN t \<inter> N' \<inter> V\<close> heq Q' \<open>Q \<subseteq> Q'\<close> 
+            by (auto simp: homeomorphism_apply2 [OF hom'] dest: h_in_UU)
         qed (auto simp: \<open>y \<in> Q\<close> opeUQ)
     qed
     show ?thesis
-      using*[OF order_refl] N \<open>0 < \<delta>\<close> by (simp add: split: if_split_asm)
+      using *[OF order_refl] N \<open>0 < \<delta>\<close> by (simp add: split: if_split_asm)
   qed
   then obtain V fs where opeV: "\<And>y. y \<in> U \<Longrightarrow> openin (top_of_set U) (V y)"
           and V: "\<And>y. y \<in> U \<Longrightarrow> y \<in> V y"
@@ -1641,9 +1613,7 @@
       by (simp add: Abstract_Topology.openin_Times opeV)
     show "\<And>i. i \<in> U \<Longrightarrow> continuous_map
               (subtopology (top_of_set ({0..1} \<times> U)) ({0..1} \<times> V i)) euclidean (fs i)"
-      using contfs
-      apply simp
-      by (metis continuous_map_iff_continuous continuous_on_subset openin_imp_subset openin_subtopology_self subtopology_subtopology)
+      by (metis contfs subtopology_subtopology continuous_map_iff_continuous Times_Int_Times VU inf.absorb_iff2 inf.idem)
     show "fs i x = fs j x"  if "i \<in> U" "j \<in> U" and x: "x \<in> topspace ?X \<inter> {0..1} \<times> V i \<inter> {0..1} \<times> V j"
          for i j x
     proof -
@@ -1654,8 +1624,7 @@
         show "fs i (0, y) = fs j (0, y)"
           using*V by (simp add: \<open>y \<in> V i\<close> \<open>y \<in> V j\<close> that)
         show conth_y: "continuous_on ({0..1} \<times> {y}) h"
-          apply (rule continuous_on_subset [OF conth])
-          using VU \<open>y \<in> V j\<close> that by auto
+          using VU \<open>y \<in> V j\<close> that by (auto intro: continuous_on_subset [OF conth])
         show "h ` ({0..1} \<times> {y}) \<subseteq> S"
           using \<open>y \<in> V i\<close> assms(3) VU that by fastforce
         show "continuous_on ({0..1} \<times> {y}) (fs i)"
@@ -1714,10 +1683,10 @@
     apply (rule covering_space_lift_homotopy [OF cov _ _ _ contf fim])
     using him  by (auto simp: contf heq)
   show ?thesis
-    apply (rule_tac k="k \<circ> (\<lambda>z. Pair (snd z) (fst z))" in that)
-       apply (intro continuous_intros continuous_on_subset [OF contk])
-    using kim heqp apply (auto simp: k0)
-    done
+  proof
+    show "continuous_on (U \<times> {0..1}) (k \<circ> (\<lambda>z. (snd z, fst z)))"
+      by (intro continuous_intros continuous_on_subset [OF contk]) auto
+  qed (use kim heqp in \<open>auto simp: k0\<close>)
 qed
 
 corollary covering_space_lift_homotopic_function:
@@ -1769,10 +1738,10 @@
   then have gim: "(\<lambda>y. b) ` U \<subseteq> C"
     by blast
   show ?thesis
-    apply (rule covering_space_lift_homotopic_function
-                  [OF cov continuous_on_const gim _ homotopic_with_symD [OF hom]])
-    using b that apply auto
-    done
+  proof (rule covering_space_lift_homotopic_function [OF cov continuous_on_const gim])
+    show "\<And>y. y \<in> U \<Longrightarrow> p b = a"
+      using b by auto
+  qed (use that homotopic_with_symD [OF hom] in auto)
 qed
 
 subsection\<open> Lifting of general functions to covering space\<close>
@@ -1792,8 +1761,7 @@
       and pk: "\<And>z. z \<in> {0..1} \<times> {undefined} \<Longrightarrow> p(k z) = (g \<circ> fst) z"
   proof (rule covering_space_lift_homotopy [OF cov, of "{undefined}" "g \<circ> fst"])
     show "continuous_on ({0..1::real} \<times> {undefined::'c}) (g \<circ> fst)"
-      apply (intro continuous_intros)
-      using \<open>path g\<close> by (simp add: path_def)
+      using \<open>path g\<close> by (intro continuous_intros) (simp add: path_def)
     show "(g \<circ> fst) ` ({0..1} \<times> {undefined}) \<subseteq> S"
       using pag by (auto simp: path_image_def)
     show "(g \<circ> fst) (0, y) = p a" if "y \<in> {undefined}" for y::'c
@@ -1848,9 +1816,10 @@
              and kim: "k ` ({0..1} \<times> {0..1}) \<subseteq> C"
              and kh2: "\<And>y. y \<in> {0..1} \<Longrightarrow> k (y, 0) = h2 0"
              and hpk: "\<And>z. z \<in> {0..1} \<times> {0..1} \<Longrightarrow> h z = p (k z)"
-    apply (rule covering_space_lift_homotopy_alt [OF cov conth him, of "\<lambda>x. h2 0"])
-    using h1h2 ph1 ph2 apply (force simp: heq0 pathstart_def pathfinish_def)
-    using path_image_def pih2 by fastforce+
+  proof (rule covering_space_lift_homotopy_alt [OF cov conth him])
+    show "\<And>y. y \<in> {0..1} \<Longrightarrow> h (y, 0) = p (h2 0)"
+      by (metis atLeastAtMost_iff h1h2 heq0 order_refl pathstart_def ph1 zero_le_one)
+  qed (use path_image_def pih2 in \<open>fastforce+\<close>)
   have contg1: "continuous_on {0..1} g1" and contg2: "continuous_on {0..1} g2"
     using \<open>path g1\<close> \<open>path g2\<close> path_def by blast+
   have g1im: "g1 ` {0..1} \<subseteq> S" and g2im: "g2 ` {0..1} \<subseteq> S"
@@ -1888,8 +1857,7 @@
       show "(k \<circ> Pair 0) 1 = h1 1"
         using keqh1 by auto
       show "continuous_on {0..1} (\<lambda>a. (k \<circ> Pair a) 1)"
-        apply simp
-        by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
+        by (auto intro!: continuous_intros continuous_on_compose2 [OF contk]) 
       show "\<And>x. x \<in> {0..1} \<Longrightarrow> g1 1 = p ((k \<circ> Pair x) 1)"
         using heq1 hpk by auto
     qed (use contk kim g1im h1im that in \<open>auto simp: ph1\<close>)
@@ -1995,8 +1963,10 @@
         show "q' 0 = (h \<circ> (*\<^sub>R) 2) 0"
           by (metis \<open>pathstart q' = pathstart q\<close> comp_def h(3) pastq pathstart_def pth_4(2))
         show "continuous_on {0..1/2} (f \<circ> g \<circ> (*\<^sub>R) 2)"
-          apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path g\<close>] continuous_on_subset [OF contf])
-          using g(2) path_image_def by fastforce+
+        proof (intro continuous_intros continuous_on_path [OF \<open>path g\<close>] continuous_on_subset [OF contf])
+          show "g ` (*\<^sub>R) 2 ` {0..1/2} \<subseteq> U"
+            using g path_image_def by fastforce
+        qed auto
         show "(f \<circ> g \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> S"
           using g(2) path_image_def fim by fastforce
         show "(h \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> C"
@@ -2010,8 +1980,7 @@
         show "continuous_on {0..1/2} q'"
           by (simp add: continuous_on_path \<open>path q'\<close>)
         show "continuous_on {0..1/2} (h \<circ> (*\<^sub>R) 2)"
-          apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path h\<close>], force)
-          done
+          by (intro continuous_intros continuous_on_path [OF \<open>path h\<close>]) auto
       qed (use that in auto)
       moreover have "q' t = (reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) t" if "1/2 < t" "t \<le> 1" for t
       proof (rule covering_space_lift_unique [OF cov, of q' 1 "reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)" "{1/2<..1}" "f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)" t])
@@ -2019,9 +1988,10 @@
           using h' \<open>pathfinish q' = pathfinish q\<close> pafiq
           by (simp add: pathstart_def pathfinish_def reversepath_def)
         show "continuous_on {1/2<..1} (f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1))"
-          apply (intro continuous_intros continuous_on_compose continuous_on_path \<open>path g'\<close> continuous_on_subset [OF contf])
-          using g' apply simp_all
-          by (auto simp: path_image_def reversepath_def)
+        proof (intro continuous_intros continuous_on_path \<open>path g'\<close> continuous_on_subset [OF contf])
+          show "reversepath g' ` (\<lambda>t. 2 *\<^sub>R t - 1) ` {1/2<..1} \<subseteq> U"
+            using g' by (auto simp: path_image_def reversepath_def)
+        qed (use g' in auto)
         show "(f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) ` {1/2<..1} \<subseteq> S"
           using g'(2) path_image_def fim by (auto simp: image_subset_iff path_image_def reversepath_def)
         show "q' ` {1/2<..1} \<subseteq> C"
@@ -2036,9 +2006,7 @@
         show "continuous_on {1/2<..1} q'"
           by (auto intro: continuous_on_path [OF \<open>path q'\<close>])
         show "continuous_on {1/2<..1} (reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1))"
-          apply (intro continuous_intros continuous_on_compose continuous_on_path \<open>path h'\<close>)
-          using h' apply auto
-          done
+          by (intro continuous_intros continuous_on_path \<open>path h'\<close>) (use h' in auto)
       qed (use that in auto)
       ultimately have "q' t = (h +++ reversepath h') t" if "0 \<le> t" "t \<le> 1" for t
         using that by (simp add: joinpaths_def)
@@ -2090,13 +2058,10 @@
       proof -
         have "openin (top_of_set U) (U \<inter> f -` W)"
           using WV contf continuous_on_open_gen fim by auto
+        then obtain UO where "openin (top_of_set U) UO \<and> path_connected UO \<and> y \<in> UO \<and> UO \<subseteq> U \<inter> f -` W"
+          using U WV \<open>y \<in> U\<close> unfolding locally_path_connected by (meson IntI vimage_eq)
         then show ?thesis
-          using U WV
-          apply (auto simp: locally_path_connected)
-          apply (drule_tac x="U \<inter> f -` W" in spec)
-          apply (drule_tac x=y in spec)
-          apply (auto simp: \<open>y \<in> U\<close> intro: that)
-          done
+          by (meson \<open>y \<in> U\<close> image_subset_iff_subset_vimage le_inf_iff that)
       qed
       have "W' \<subseteq> C" "W \<subseteq> S"
         using opeCW' WV openin_imp_subset by auto
@@ -2107,9 +2072,7 @@
         have "openin (top_of_set S) (W \<inter> p' -` (W' \<inter> X))"
         proof (rule openin_trans)
           show "openin (top_of_set W) (W \<inter> p' -` (W' \<inter> X))"
-            apply (rule continuous_openin_preimage [OF contp' p'im])
-            using X \<open>W' \<subseteq> C\<close> apply (auto simp: openin_open)
-            done
+            using X \<open>W' \<subseteq> C\<close> by (intro continuous_openin_preimage [OF contp' p'im]) (auto simp: openin_open)
           show "openin (top_of_set S) W"
             using WV by blast
         qed
@@ -2125,9 +2088,8 @@
           assume y': "y' \<in> V" "y' \<in> U" "f y' \<in> W" "p' (f y') \<in> W'" "p' (f y') \<in> X"
           then obtain \<gamma> where "path \<gamma>" "path_image \<gamma> \<subseteq> V" "pathstart \<gamma> = y" "pathfinish \<gamma> = y'"
             by (meson \<open>path_connected V\<close> \<open>y \<in> V\<close> path_connected_def)
-          obtain pp qq where "path pp" "path_image pp \<subseteq> U"
-                             "pathstart pp = z" "pathfinish pp = y"
-                             "path qq" "path_image qq \<subseteq> C" "pathstart qq = a"
+          obtain pp qq where pp: "path pp" "path_image pp \<subseteq> U" "pathstart pp = z" "pathfinish pp = y"
+                         and qq: "path qq" "path_image qq \<subseteq> C" "pathstart qq = a"
                          and pqqeq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(qq t) = f(pp t)"
             using*[OF \<open>y \<in> U\<close>] by blast
           have finW: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> f (\<gamma> x) \<in> W"
@@ -2142,27 +2104,32 @@
               by (simp add: \<open>pathstart pp = z\<close>)
             show "pathfinish (pp +++ \<gamma>) = y'"
               by (simp add: \<open>pathfinish \<gamma> = y'\<close>)
-            have paqq: "pathfinish qq = pathstart (p' \<circ> f \<circ> \<gamma>)"
-              apply (simp add: \<open>pathstart \<gamma> = y\<close> pathstart_compose)
-              apply (metis (mono_tags, lifting) \<open>l y \<in> W'\<close> \<open>path pp\<close> \<open>path qq\<close> \<open>path_image pp \<subseteq> U\<close> \<open>path_image qq \<subseteq> C\<close>
-                           \<open>pathfinish pp = y\<close> \<open>pathstart pp = z\<close> \<open>pathstart qq = a\<close>
-                           homeomorphism_apply1 [OF homUW'] l pleq pqqeq \<open>y \<in> U\<close>)
-              done
+            have "pathfinish qq = l y"
+              using \<open>path pp\<close> \<open>path qq\<close> \<open>path_image pp \<subseteq> U\<close> \<open>path_image qq \<subseteq> C\<close> \<open>pathfinish pp = y\<close> \<open>pathstart pp = z\<close> \<open>pathstart qq = a\<close> l pqqeq by blast
+            also have "... = p' (f y)"
+              using \<open>l y \<in> W'\<close> homUW' homeomorphism_apply1 pleq that(2) by fastforce
+            finally have "pathfinish qq = p' (f y)" .
+            then have paqq: "pathfinish qq = pathstart (p' \<circ> f \<circ> \<gamma>)"
+              by (simp add: \<open>pathstart \<gamma> = y\<close> pathstart_compose)
             have "continuous_on (path_image \<gamma>) (p' \<circ> f)"
             proof (rule continuous_on_compose)
               show "continuous_on (path_image \<gamma>) f"
                 using \<open>path_image \<gamma> \<subseteq> V\<close> \<open>V \<subseteq> U\<close> contf continuous_on_subset by blast
               show "continuous_on (f ` path_image \<gamma>) p'"
-                apply (rule continuous_on_subset [OF contp'])
-                apply (auto simp: path_image_def pathfinish_def pathstart_def finW)
-                done
+              proof (rule continuous_on_subset [OF contp'])
+                show "f ` path_image \<gamma> \<subseteq> W"
+                  by (auto simp: path_image_def pathfinish_def pathstart_def finW)
+              qed
             qed
             then show "path (qq +++ (p' \<circ> f \<circ> \<gamma>))"
               using \<open>path \<gamma>\<close> \<open>path qq\<close> paqq path_continuous_image path_join_imp by blast
             show "path_image (qq +++ (p' \<circ> f \<circ> \<gamma>)) \<subseteq> C"
-              apply (rule subset_path_image_join)
-               apply (simp add: \<open>path_image qq \<subseteq> C\<close>)
-              by (metis \<open>W' \<subseteq> C\<close> \<open>path_image \<gamma> \<subseteq> V\<close> dual_order.trans fimW(1) image_comp image_mono p'im path_image_compose)
+            proof (rule subset_path_image_join)
+              show "path_image qq \<subseteq> C"
+                by (simp add: \<open>path_image qq \<subseteq> C\<close>)
+              show "path_image (p' \<circ> f \<circ> \<gamma>) \<subseteq> C"
+                by (metis \<open>W' \<subseteq> C\<close> \<open>path_image \<gamma> \<subseteq> V\<close> dual_order.trans fimW(1) image_comp image_mono p'im path_image_compose)
+            qed
             show "pathstart (qq +++ (p' \<circ> f \<circ> \<gamma>)) = a"
               by (simp add: \<open>pathstart qq = a\<close>)
             show "p ((qq +++ (p' \<circ> f \<circ> \<gamma>)) \<xi>) = f ((pp +++ \<gamma>) \<xi>)" if \<xi>: "\<xi> \<in> {0..1}" for \<xi>
@@ -2170,8 +2137,7 @@
               show "p (qq (2*\<xi>)) = f (pp (2*\<xi>))" if "\<xi>*2 \<le> 1"
                 using \<open>\<xi> \<in> {0..1}\<close> pqqeq that by auto
               show "p (p' (f (\<gamma> (2*\<xi> - 1)))) = f (\<gamma> (2*\<xi> - 1))" if "\<not> \<xi>*2 \<le> 1"
-                apply (rule homeomorphism_apply2 [OF homUW' finW])
-                using that \<xi> by auto
+                using that \<xi> by (auto intro: homeomorphism_apply2 [OF homUW' finW])
             qed
           qed
           with \<open>pathfinish \<gamma> = y'\<close>  \<open>p' (f y') \<in> X\<close> show "y' \<in> l -` X"