diff -r d2daeef3ce47 -r 36209dfb981e src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed May 02 12:48:08 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed May 02 23:32:47 2018 +0100
@@ -3249,10 +3249,10 @@
     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
@@ -3357,10 +3357,7 @@
     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
@@ -3434,7 +3431,7 @@
   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"
@@ -3450,7 +3447,7 @@
 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"
@@ -6818,8 +6815,7 @@
   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)