src/HOL/Analysis/Homeomorphism.thy

   obtain T where "subspace T" and Tsub: "T \<subseteq> {x. i \<bullet> x = 0}"
              and dimT: "dim T = dim ((+) (- a) ` S)"
     apply (rule choose_subspace_of_subspace [of "dim ((+) (- a) ` S)" "{x::'n. i \<bullet> x = 0}"])
      apply (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>])
      apply (metis DIM_positive Suc_pred dd not_le not_less_eq_eq)
-    apply (metis span_eq subspace_hyperplane)
+    apply (metis span_eq_iff subspace_hyperplane)
     done
   have "subspace (span ((+) (- a) ` S))"
     using subspace_span by blast
   then obtain h k where "linear h" "linear k"
                and heq: "h ` span ((+) (- a) ` S) = T"

     apply (auto simp: dimT)
     done
   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_inc by fastforce
+    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)