src/HOL/Analysis/Homeomorphism.thy

--- a/src/HOL/Analysis/Homeomorphism.thy	Wed May 02 13:49:38 2018 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy	Thu May 03 15:07:14 2018 +0200
@@ -881,9 +881,8 @@
     using aff_dim_convex_Int_open [OF \<open>convex U\<close> open_ball]
     by (fastforce simp add: Int_commute)
   have "rel_frontier S homeomorphic rel_frontier (ball z 1 \<inter> U)"
-    apply (rule homeomorphic_rel_frontiers_convex_bounded_sets)
-    apply (auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms)
-    done
+    by (rule homeomorphic_rel_frontiers_convex_bounded_sets)
+       (auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms)
   also have "... = sphere z 1 \<inter> U"
     using convex_affine_rel_frontier_Int [of "ball z 1" U]
     by (simp add: \<open>affine U\<close> bne)
@@ -903,9 +902,8 @@
       by (force simp: h [symmetric] image_comp o_def kh)
   qed (auto intro: continuous_on_subset hcon kcon simp: kh hk)
   also have "... homeomorphic T"
-    apply (rule homeomorphic_punctured_affine_sphere_affine)
-    using a him
-    by (auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>)
+    by (rule homeomorphic_punctured_affine_sphere_affine)
+       (use a him in \<open>auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>\<close>)
   finally show ?thesis .
 qed
 
@@ -965,7 +963,7 @@
   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_clauses(1) span_linear_image by blast
+    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}"
@@ -989,8 +987,8 @@
     apply (simp add: homeomorphic_def homeomorphism_def)
     apply (rule_tac x="g \<circ> h" in exI)
     apply (rule_tac x="k \<circ> f" in exI)
-    apply (auto simp: ghcont kfcont span_clauses(1) homeomorphism_apply2 [OF fg] image_comp)
-    apply (force simp: o_def homeomorphism_apply2 [OF fg] span_clauses(1))
+    apply (auto simp: ghcont kfcont span_superset homeomorphism_apply2 [OF fg] image_comp)
+    apply (force simp: o_def homeomorphism_apply2 [OF fg] span_superset)
     done
   finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" .
   show ?thesis