src/HOL/Analysis/Convex_Euclidean_Space.thy

         by (simp add: sum.reindex[unfolded inj_on_def] algebra_simps
             sum_subtractf scaleR_left.sum[symmetric] sum_diff1 that)
     qed (use \<open>F \<subseteq> insert a S\<close> in auto)
   qed
   then show ?thesis
-    unfolding affine_hull_explicit span_explicit by auto
+    unfolding affine_hull_explicit span_explicit by blast
 qed
 
 lemma affine_hull_insert_span:
   assumes "a \<notin> S"
   shows "affine hull (insert a S) = {a + v | v . v \<in> span {x - a | x.  x \<in> S}}"

   have *: "{x - a |x. x \<in> S - {a}} = (\<lambda>x. x - a) ` (S - {a})"
     by auto
   have **: "card {x - a |x. x \<in> S - {a}} = card (S - {a})"
     by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def)
   have "dim {x - a |x. x \<in> S - {a}} \<le> dim S"
-    using \<open>a\<in>S\<close> by (auto simp: span_superset span_diff intro: subset_le_dim)
+    using \<open>a\<in>S\<close> by (auto simp: span_base span_diff intro: subset_le_dim)
   also have "\<dots> < dim S + 1" by auto
   also have "\<dots> \<le> card (S - {a})"
     using assms
     using card_Diff_singleton[OF assms(1) \<open>a\<in>S\<close>]
     by auto

     using dim_subset_UNIV[of B] by simp
   from ex_card[OF this] obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B"
     by auto
   let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
   have "\<exists>f. linear f \<and> f ` B = d \<and> f ` span B = ?t \<and> inj_on f (span B)"
-  proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_inc)
+  proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_superset)
     show "d \<subseteq> {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
       using d inner_not_same_Basis by blast
   qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms)
   with t \<open>card B = dim B\<close> d show ?thesis by auto
 qed