src/HOL/Analysis/Convex_Euclidean_Space.thy

 proof -
   obtain a where a: "a \<in> S"
     using assms by auto
   then have h0: "independent  ((\<lambda>x. -a + x) ` (S-{a}))"
     using affine_dependent_iff_dependent2 assms by auto
-  then obtain B where B:
+  obtain B where B:
     "(\<lambda>x. -a+x) ` (S - {a}) \<subseteq> B \<and> B \<subseteq> (\<lambda>x. -a+x) ` V \<and> independent B \<and> (\<lambda>x. -a+x) ` V \<subseteq> span B"
-     using maximal_independent_subset_extend[of "(\<lambda>x. -a+x) ` (S-{a})" "(\<lambda>x. -a + x) ` V"] assms
-     by blast
+    using assms
+    by (blast intro: maximal_independent_subset_extend[OF _ h0, of "(\<lambda>x. -a + x) ` V"])
   define T where "T = (\<lambda>x. a+x) ` insert 0 B"
   then have "T = insert a ((\<lambda>x. a+x) ` B)"
     by auto
   then have "affine hull T = (\<lambda>x. a+x) ` span B"
     using affine_hull_insert_span_gen[of a "((\<lambda>x. a+x) ` B)"] translation_assoc[of "-a" a B]

   next
     case False
     then have "card ((\<lambda>x. -a + x) ` (B - {a})) > 0"
       using fin by auto
     moreover have h1: "card ((\<lambda>x. -a + x) ` (B-{a})) = card (B-{a})"
-       apply (rule card_image)
-       using translate_inj_on
-       apply (auto simp del: uminus_add_conv_diff)
-       done
+      by (rule card_image) (use translate_inj_on in blast)
     ultimately have "card (B-{a}) > 0" by auto
     then have *: "finite (B - {a})"
       using card_gt_0_iff[of "(B - {a})"] by auto
     then have "card (B - {a}) = card B - 1"
       using card_Diff_singleton assms by auto

     and "S \<subseteq> T"
     and "dim S \<ge> dim T"
   shows "S = T"
 proof -
   obtain B where B: "B \<le> S" "independent B \<and> S \<subseteq> span B" "card B = dim S"
-    using basis_exists[of S] by auto
+    using basis_exists[of S] by metis
   then have "span B \<subseteq> S"
     using span_mono[of B S] span_eq[of S] assms by metis
   then have "span B = S"
     using B by auto
   have "dim S = dim T"

 qed
 
 corollary dim_eq_span:
   fixes S :: "'a::euclidean_space set"
   shows "\<lbrakk>S \<subseteq> T; dim T \<le> dim S\<rbrakk> \<Longrightarrow> span S = span T"
-by (simp add: span_mono subspace_dim_equal subspace_span)
+by (simp add: span_mono subspace_dim_equal)
 
 lemma dim_eq_full:
     fixes S :: "'a :: euclidean_space set"
     shows "dim S = DIM('a) \<longleftrightarrow> span S = UNIV"
 apply (rule iffI)

       done
   qed
   define k where "k = Max (f ` c)"
   have "convex_on (convex hull c) f"
     apply(rule convex_on_subset[OF assms(2)])
-    apply(rule subset_trans[OF _ e(1)])
-    apply(rule c1)
+    apply(rule subset_trans[OF c1 e(1)])
     done
   then have k: "\<forall>y\<in>convex hull c. f y \<le> k"
     apply (rule_tac convex_on_convex_hull_bound, assumption)
     by (simp add: k_def c)
   have "e \<le> e * real DIM('a)"