src/HOL/Analysis/Change_Of_Vars.thy

     using dim_subset_UNIV by blast
   moreover have False if less: "dim {x. f x = 0} < DIM('a)"
   proof -
     obtain d where "d \<noteq> 0" and d: "\<And>y. f y = 0 \<Longrightarrow> d \<bullet> y = 0"
       using orthogonal_to_subspace_exists [OF less] orthogonal_def
-      by (metis (mono_tags, lifting) mem_Collect_eq span_clauses(1))
+      by (metis (mono_tags, lifting) mem_Collect_eq span_superset)
     then obtain k where "k > 0"
       and k: "\<And>e. e > 0 \<Longrightarrow> \<exists>y. y \<in> S - {0} \<and> norm y < e \<and> k * norm y \<le> \<bar>d \<bullet> y\<bar>"
       using lb by blast
     have "\<exists>h. \<forall>n. ((h n \<in> S \<and> h n \<noteq> 0 \<and> k * norm (h n) \<le> \<bar>d \<bullet> h n\<bar>) \<and> norm (h n) < 1 / real (Suc n)) \<and>
                norm (h (Suc n)) < norm (h n)"