src/HOL/Analysis/Homeomorphism.thy

   then have bne: "ball z 1 \<inter> U \<noteq> {}" by force
   then have [simp]: "aff_dim(ball z 1 \<inter> U) = aff_dim U"
     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)
   finally have "rel_frontier S homeomorphic sphere z 1 \<inter> U" . 
   then obtain h k where him: "h ` rel_frontier S = sphere z 1 \<inter> U"

       using him a kh by auto metis
     show "k ` (sphere z 1 \<inter> U - {h a}) = rel_frontier S - {a}"
       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
 
 
 text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set

     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)
   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}"
     by (simp add: fg [unfolded homeomorphism_def])
   finally have gh_sub_sph: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> sphere 0 1 - {i}"

     by (simp add: homeomorphic_translation)
   also have Shom: "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S"
     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
     apply (rule_tac U = "ball 0 1 \<union> image (g o h) ((+) (- a) ` S)"
                 and T = "image (g o h) ((+) (- a) ` S)"