# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1694973395 -3600
# Node ID f8595f6d39a59336ca4644c57b985f51f8ef0816
# Parent  18ea58bdcf77b0929faea2a123fd136668dce4c4
(pointlessly) get rid of some simp calls within "proof"

diff -r 18ea58bdcf77 -r f8595f6d39a5 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Sat Sep 16 06:38:44 2023 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Sun Sep 17 18:56:35 2023 +0100
@@ -46,11 +46,9 @@
   assumes "convex C" "T \<subseteq> C" and z: "z \<in> rel_interior C" and dis: "disjnt S (rel_interior C)"
   shows "S \<inter> (convex hull (insert z T)) = S \<inter> (convex hull T)" (is "?lhs = ?rhs")
 proof
-  have "T = {} \<Longrightarrow> z \<notin> S"
+  have *: "T = {} \<Longrightarrow> z \<notin> S"
     using dis z by (auto simp add: disjnt_def)
-  then show "?lhs \<subseteq> ?rhs"
-  proof (clarsimp simp add: convex_hull_insert_segments)
-    fix x y
+  { fix x y
     assume "x \<in> S" and y: "y \<in> convex hull T" and "x \<in> closed_segment z y"
     have "y \<in> closure C"
       by (metis y \<open>convex C\<close> \<open>T \<subseteq> C\<close> closure_subset contra_subsetD convex_hull_eq hull_mono)
@@ -58,10 +56,12 @@
       by (meson \<open>x \<in> S\<close> dis disjnt_iff)
     moreover have "x \<in> open_segment z y \<union> {z, y}"
       using \<open>x \<in> closed_segment z y\<close> closed_segment_eq_open by blast
-    ultimately show "x \<in> convex hull T"
+    ultimately have "x \<in> convex hull T"
       using rel_interior_closure_convex_segment [OF \<open>convex C\<close> z]
       using y z by blast
-  qed
+  }
+  with * show "?lhs \<subseteq> ?rhs"
+    by (auto simp add: convex_hull_insert_segments)
   show "?rhs \<subseteq> ?lhs"
     by (meson hull_mono inf_mono subset_insertI subset_refl)
 qed
@@ -164,15 +164,18 @@
 lemma in_interior_closure_convex_segment:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" and a: "a \<in> interior S" and b: "b \<in> closure S"
-    shows "open_segment a b \<subseteq> interior S"
-proof (clarsimp simp: in_segment)
-  fix u::real
-  assume u: "0 < u" "u < 1"
-  have "(1 - u) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>R (b - a)"
-    by (simp add: algebra_simps)
-  also have "... \<in> interior S" using mem_interior_closure_convex_shrink [OF assms] u
-    by simp
-  finally show "(1 - u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" .
+  shows "open_segment a b \<subseteq> interior S"
+proof -
+  { fix u::real
+    assume u: "0 < u" "u < 1"
+    have "(1 - u) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>R (b - a)"
+      by (simp add: algebra_simps)
+    also have "... \<in> interior S" using mem_interior_closure_convex_shrink [OF assms] u
+      by simp
+    finally have "(1 - u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" .
+  }
+  then show ?thesis
+    by (clarsimp simp: in_segment)
 qed
 
 lemma convex_closure_interior:
@@ -193,11 +196,9 @@
         using \<open>a \<in> interior S\<close> closure_subset by blast
     next
       case False
-      show ?thesis
-      proof (clarsimp simp add: closure_def islimpt_approachable)
-        fix e::real
+      { fix e::real
         assume xnotS: "x \<notin> interior S" and "0 < e"
-        show "\<exists>x'\<in>interior S. x' \<noteq> x \<and> dist x' x < e"
+        have "\<exists>x'\<in>interior S. x' \<noteq> x \<and> dist x' x < e"
         proof (intro bexI conjI)
           show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<noteq> x"
             using False \<open>0 < e\<close> by (auto simp: algebra_simps min_def)
@@ -207,7 +208,9 @@
             using \<open>0 < e\<close> False
             by (auto simp add: min_def a intro: mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x])
         qed
-      qed
+      }
+      then show ?thesis
+        by (auto simp add: closure_def islimpt_approachable)
     qed
   qed
   then show ?thesis
@@ -232,11 +235,9 @@
   have "conic hull S \<subseteq> span S"
     by (simp add: hull_minimal span_superset)
   moreover
-  have "affine hull S \<subseteq> conic hull S"
-  proof clarsimp
-    fix x
+  { fix x
     assume "x \<in> affine hull S"
-    show "x \<in> conic hull S"
+    have "x \<in> conic hull S"
     proof (cases "x=0")
       case True
       then show ?thesis
@@ -252,7 +253,9 @@
       then show ?thesis
         by (simp add: conic_hull_explicit)
     qed
-  qed
+  }
+  then have "affine hull S \<subseteq> conic hull S"
+    by auto
   ultimately show ?thesis
     by blast
 qed
@@ -313,16 +316,13 @@
   assumes "finite S"
     and "0 \<notin> S"
   shows "convex hull (insert 0 S) = {y. \<exists>u. (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S \<le> 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y}"
-proof (simp add: convex_hull_finite set_eq_iff assms, safe)
-  fix x and u :: "'a \<Rightarrow> real"
-  assume "0 \<le> u 0" "\<forall>x\<in>S. 0 \<le> u x" "u 0 + sum u S = 1"
-  then show "\<exists>v. (\<forall>x\<in>S. 0 \<le> v x) \<and> sum v S \<le> 1 \<and> (\<Sum>x\<in>S. v x *\<^sub>R x) = (\<Sum>x\<in>S. u x *\<^sub>R x)"
-    by force
-next
-  fix x and u :: "'a \<Rightarrow> real"
-  assume "\<forall>x\<in>S. 0 \<le> u x" "sum u S \<le> 1"
-  then show "\<exists>v. 0 \<le> v 0 \<and> (\<forall>x\<in>S. 0 \<le> v x) \<and> v 0 + sum v S = 1 \<and> (\<Sum>x\<in>S. v x *\<^sub>R x) = (\<Sum>x\<in>S. u x *\<^sub>R x)"
-    by (rule_tac x="\<lambda>x. if x = 0 then 1 - sum u S else u x" in exI) (auto simp: sum_delta_notmem assms if_smult)
+proof -
+  { fix x and u :: "'a \<Rightarrow> real"
+    assume "\<forall>x\<in>S. 0 \<le> u x" "sum u S \<le> 1"
+    then have "\<exists>v. 0 \<le> v 0 \<and> (\<forall>x\<in>S. 0 \<le> v x) \<and> v 0 + sum v S = 1 \<and> (\<Sum>x\<in>S. v x *\<^sub>R x) = (\<Sum>x\<in>S. u x *\<^sub>R x)"
+      by (rule_tac x="\<lambda>x. if x = 0 then 1 - sum u S else u x" in exI) (auto simp: sum_delta_notmem assms if_smult)
+  }
+  then show ?thesis by (auto simp: convex_hull_finite set_eq_iff assms)
 qed
 
 lemma substd_simplex:
@@ -1444,13 +1444,11 @@
 
 lemma rel_interior_inter_aux: "\<Inter>{rel_interior S |S. S \<in> I} \<subseteq> \<Inter>I"
 proof -
-  {
-    fix y
+  { fix y
     assume "y \<in> \<Inter>{rel_interior S |S. S \<in> I}"
     then have y: "\<forall>S \<in> I. y \<in> rel_interior S"
       by auto
-    {
-      fix S
+    { fix S
       assume "S \<in> I"
       then have "y \<in> S"
         using rel_interior_subset y by auto
@@ -2345,32 +2343,31 @@
   proof
     assume adl: "a + d *\<^sub>R l \<in> rel_interior S"
     obtain e where "e > 0"
-             and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' (a + d *\<^sub>R l) < e \<Longrightarrow> x' \<in> rel_interior S"
+      and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' (a + d *\<^sub>R l) < e \<Longrightarrow> x' \<in> rel_interior S"
       using relin_Ex adl by blast
+    have "d + e / norm l \<le> x"
+      if "0 < x" and nonrel: "a + x *\<^sub>R l \<notin> rel_interior S" for x
+    proof (cases "x < d")
+      case True with inint nonrel \<open>0 < x\<close>
+      show ?thesis by auto
+    next
+      case False
+      then have dle: "x < d + e / norm l \<Longrightarrow> dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e"
+        by (simp add: field_simps \<open>l \<noteq> 0\<close>)
+      have ain: "a + x *\<^sub>R l \<in> affine hull S"
+        by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
+      show ?thesis
+        using e [OF ain] nonrel dle by force
+    qed
+    then
     have "d + e / norm l \<le> Inf {d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
-    proof (rule cInf_greatest [OF nonMT], clarsimp)
-      fix x::real
-      assume "0 < x" and nonrel: "a + x *\<^sub>R l \<notin> rel_interior S"
-      show "d + e / norm l \<le> x"
-      proof (cases "x < d")
-        case True with inint nonrel \<open>0 < x\<close>
-          show ?thesis by auto
-      next
-        case False
-          then have dle: "x < d + e / norm l \<Longrightarrow> dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e"
-            by (simp add: field_simps \<open>l \<noteq> 0\<close>)
-          have ain: "a + x *\<^sub>R l \<in> affine hull S"
-            by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
-          show ?thesis
-            using e [OF ain] nonrel dle by force
-      qed
-    qed
+      by (force simp add: intro: cInf_greatest [OF nonMT])
     then show False
       using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] field_simps)
   qed
-  moreover have "a + d *\<^sub>R l \<in> closure S"
-  proof (clarsimp simp: closure_approachable)
-    fix \<eta>::real assume "0 < \<eta>"
+  moreover 
+  have "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>" if "0 < \<eta>" for \<eta>::real
+  proof -
     have 1: "a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l \<in> S"
     proof (rule subsetD [OF rel_interior_subset inint])
       show "d - min d (\<eta> / 2 / norm l) < d"
@@ -2381,10 +2378,12 @@
     also have "... < \<eta>"
       using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: field_simps)
     finally have 2: "norm l * min d (\<eta> / (norm l * 2)) < \<eta>" .
-    show "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>"
+    show ?thesis
       using 1 2 \<open>0 < d\<close> \<open>0 < \<eta>\<close> 
       by (rule_tac x="a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l" in bexI) (auto simp: algebra_simps)
   qed
+  then have "a + d *\<^sub>R l \<in> closure S"
+    by (auto simp: closure_approachable)
   ultimately have infront: "a + d *\<^sub>R l \<in> rel_frontier S"
     by (simp add: rel_frontier_def)
   show ?thesis
@@ -3029,12 +3028,15 @@
              (if card(S) \<le> DIM('a) then {}
               else {y. \<exists>u. (\<forall>x \<in> S. 0 < u x) \<and> sum u S = 1 \<and> (\<Sum>x\<in>S. u x *\<^sub>R x) = y})"  
    (is "_ = (if _ then _ else ?rhs)")
-proof (clarsimp simp: aff_independent_finite empty_interior_convex_hull assms)
-  assume S: "\<not> card S \<le> DIM('a)"
-  have "interior (convex hull S) = rel_interior(convex hull S)"
-    using assms S by (simp add: affine_independent_span_gt rel_interior_interior)
-  then show "interior(convex hull S) = ?rhs"
-    by (simp add: assms S rel_interior_convex_hull_explicit)
+proof -
+  { assume S: "\<not> card S \<le> DIM('a)"
+    have "interior (convex hull S) = rel_interior(convex hull S)"
+      using assms S by (simp add: affine_independent_span_gt rel_interior_interior)
+    then have "interior(convex hull S) = ?rhs"
+      by (simp add: assms S rel_interior_convex_hull_explicit)
+  } 
+  then show ?thesis
+    by (auto simp: aff_independent_finite empty_interior_convex_hull assms)
 qed
 
 lemma interior_convex_hull_explicit:
@@ -3084,22 +3086,26 @@
   fixes a :: "'a::euclidean_space"
   shows  "interior(open_segment a b) =
                  (if 2 \<le> DIM('a) then {} else open_segment a b)"
-proof (simp add: not_le, intro conjI impI)
-  assume "2 \<le> DIM('a)"
-  then show "interior (open_segment a b) = {}"
+proof (cases "2 \<le> DIM('a)")
+  case True
+  then have "interior (open_segment a b) = {}"
     using interior_closed_segment_ge2 interior_mono segment_open_subset_closed by blast
+  with True show ?thesis
+    by auto 
 next
-  assume le2: "DIM('a) < 2"
-  show "interior (open_segment a b) = open_segment a b"
+  case ge2: False
+  have "interior (open_segment a b) = open_segment a b"
   proof (cases "a = b")
     case True then show ?thesis by auto
   next
     case False
-    with le2 have "affine hull (open_segment a b) = UNIV"
+    with ge2 have "affine hull (open_segment a b) = UNIV"
       by (simp add: False affine_independent_span_gt)
     then show "interior (open_segment a b) = open_segment a b"
       using rel_interior_interior rel_interior_open_segment by blast
   qed
+  with ge2 show ?thesis 
+    by auto
 qed
 
 lemma interior_closed_segment:
@@ -4870,12 +4876,15 @@
 lemma bounded_hyperplane_eq_trivial:
   fixes a :: "'a::euclidean_space"
   shows "bounded {x. a \<bullet> x = r} \<longleftrightarrow> (if a = 0 then r \<noteq> 0 else DIM('a) = 1)"
-proof (simp add: bounded_hyperplane_eq_trivial_0, clarify)
-  assume "r \<noteq> 0" "a \<noteq> 0"
-  have "aff_dim {x. y \<bullet> x = 0} = aff_dim {x. a \<bullet> x = r}" if "y \<noteq> 0" for y::'a
-    by (metis that \<open>a \<noteq> 0\<close> aff_dim_hyperplane)
-  then show "bounded {x. a \<bullet> x = r} = (DIM('a) = Suc 0)"
-    by (metis One_nat_def \<open>a \<noteq> 0\<close> affine_bounded_eq_lowdim affine_hyperplane bounded_hyperplane_eq_trivial_0)
+proof -
+  { assume "r \<noteq> 0" "a \<noteq> 0"
+    have "aff_dim {x. y \<bullet> x = 0} = aff_dim {x. a \<bullet> x = r}" if "y \<noteq> 0" for y::'a
+      by (metis that \<open>a \<noteq> 0\<close> aff_dim_hyperplane)
+    then have "bounded {x. a \<bullet> x = r} = (DIM('a) = Suc 0)"
+      by (metis One_nat_def \<open>a \<noteq> 0\<close> affine_bounded_eq_lowdim affine_hyperplane bounded_hyperplane_eq_trivial_0)
+  } 
+  then show ?thesis
+    by (auto simp: bounded_hyperplane_eq_trivial_0)
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>General case without assuming closure and getting non-strict separation\<close>
@@ -5218,29 +5227,26 @@
     have cc0: "cc x = 0" if "x \<in> S" "x \<notin> T \<inter> T'" for x
       using le [OF \<open>x \<in> S\<close>] that c0
       by (force simp: cc_def cc'_def split: if_split_asm)
+    have ge0: "\<forall>x\<in>T \<inter> T'. 0 \<le> (cc(a := c a)) x"
+      by (simp add: c0 cc_def)
+    have "sum (cc(a := c a)) (insert a (T \<inter> T')) = c a + sum (cc(a := c a)) (T \<inter> T')"
+      by (simp add: anot)
+    also have "... = c a + sum (cc(a := c a)) S"
+      using \<open>T \<subseteq> S\<close> False cc0 cc_def \<open>a \<notin> S\<close> by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
+    also have "... = c a + (1 - c a)"
+      by (metis \<open>a \<notin> S\<close> fun_upd_other sum.cong sumSS'(1))
+    finally have 1: "sum (cc(a := c a)) (insert a (T \<inter> T')) = 1"
+      by simp
+    have "(\<Sum>x\<in>insert a (T \<inter> T'). (cc(a := c a)) x *\<^sub>R x) = c a *\<^sub>R a + (\<Sum>x \<in> T \<inter> T'. (cc(a := c a)) x *\<^sub>R x)"
+      by (simp add: anot)
+    also have "... = c a *\<^sub>R a + (\<Sum>x \<in> S. (cc(a := c a)) x *\<^sub>R x)"
+      using \<open>T \<subseteq> S\<close> False cc0 by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
+    also have "... = c a *\<^sub>R a + x - c a *\<^sub>R a"
+      by (simp add: wsumSS \<open>a \<notin> S\<close> if_smult sum_delta_notmem)
+    finally have self: "(\<Sum>x\<in>insert a (T \<inter> T'). (cc(a := c a)) x *\<^sub>R x) = x"
+      by simp
     show ?thesis
-    proof (simp add: convex_hull_finite, intro exI conjI)
-      show "\<forall>x\<in>T \<inter> T'. 0 \<le> (cc(a := c a)) x"
-        by (simp add: c0 cc_def)
-      show "0 \<le> (cc(a := c a)) a"
-        by (simp add: c0)
-      have "sum (cc(a := c a)) (insert a (T \<inter> T')) = c a + sum (cc(a := c a)) (T \<inter> T')"
-        by (simp add: anot)
-      also have "... = c a + sum (cc(a := c a)) S"
-        using \<open>T \<subseteq> S\<close> False cc0 cc_def \<open>a \<notin> S\<close> by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
-      also have "... = c a + (1 - c a)"
-        by (metis \<open>a \<notin> S\<close> fun_upd_other sum.cong sumSS'(1))
-      finally show "sum (cc(a := c a)) (insert a (T \<inter> T')) = 1"
-        by simp
-      have "(\<Sum>x\<in>insert a (T \<inter> T'). (cc(a := c a)) x *\<^sub>R x) = c a *\<^sub>R a + (\<Sum>x \<in> T \<inter> T'. (cc(a := c a)) x *\<^sub>R x)"
-        by (simp add: anot)
-      also have "... = c a *\<^sub>R a + (\<Sum>x \<in> S. (cc(a := c a)) x *\<^sub>R x)"
-        using \<open>T \<subseteq> S\<close> False cc0 by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
-      also have "... = c a *\<^sub>R a + x - c a *\<^sub>R a"
-        by (simp add: wsumSS \<open>a \<notin> S\<close> if_smult sum_delta_notmem)
-      finally show "(\<Sum>x\<in>insert a (T \<inter> T'). (cc(a := c a)) x *\<^sub>R x) = x"
-        by simp
-    qed
+      by (force simp: convex_hull_finite c0 intro!: ge0 1 self exI [where x = "cc(a := c a)"])
   next
     case 2
     then have "sum cc' S \<le> sum cc S"
@@ -5251,29 +5257,26 @@
     have cc0: "cc' x = 0" if "x \<in> S" "x \<notin> T \<inter> T'" for x
       using le [OF \<open>x \<in> S\<close>] that c'0
       by (force simp: cc_def cc'_def split: if_split_asm)
+    have ge0: "\<forall>x\<in>T \<inter> T'. 0 \<le> (cc'(a := c' a)) x"
+      by (simp add: c'0 cc'_def)
+    have "sum (cc'(a := c' a)) (insert a (T \<inter> T')) = c' a + sum (cc'(a := c' a)) (T \<inter> T')"
+      by (simp add: anot)
+    also have "... = c' a + sum (cc'(a := c' a)) S"
+      using \<open>T \<subseteq> S\<close> False cc0 by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
+    also have "... = c' a + (1 - c' a)"
+      by (metis \<open>a \<notin> S\<close> fun_upd_other sum.cong sumSS')
+    finally have 1: "sum (cc'(a := c' a)) (insert a (T \<inter> T')) = 1"
+      by simp
+    have "(\<Sum>x\<in>insert a (T \<inter> T'). (cc'(a := c' a)) x *\<^sub>R x) = c' a *\<^sub>R a + (\<Sum>x \<in> T \<inter> T'. (cc'(a := c' a)) x *\<^sub>R x)"
+      by (simp add: anot)
+    also have "... = c' a *\<^sub>R a + (\<Sum>x \<in> S. (cc'(a := c' a)) x *\<^sub>R x)"
+      using \<open>T \<subseteq> S\<close> False cc0 by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
+    also have "... = c a *\<^sub>R a + x - c a *\<^sub>R a"
+      by (simp add: wsumSS \<open>a \<notin> S\<close> if_smult sum_delta_notmem)
+    finally have self: "(\<Sum>x\<in>insert a (T \<inter> T'). (cc'(a := c' a)) x *\<^sub>R x) = x"
+      by simp
     show ?thesis
-    proof (simp add: convex_hull_finite, intro exI conjI)
-      show "\<forall>x\<in>T \<inter> T'. 0 \<le> (cc'(a := c' a)) x"
-        by (simp add: c'0 cc'_def)
-      show "0 \<le> (cc'(a := c' a)) a"
-        by (simp add: c'0)
-      have "sum (cc'(a := c' a)) (insert a (T \<inter> T')) = c' a + sum (cc'(a := c' a)) (T \<inter> T')"
-        by (simp add: anot)
-      also have "... = c' a + sum (cc'(a := c' a)) S"
-        using \<open>T \<subseteq> S\<close> False cc0 by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
-      also have "... = c' a + (1 - c' a)"
-        by (metis \<open>a \<notin> S\<close> fun_upd_other sum.cong sumSS')
-      finally show "sum (cc'(a := c' a)) (insert a (T \<inter> T')) = 1"
-        by simp
-      have "(\<Sum>x\<in>insert a (T \<inter> T'). (cc'(a := c' a)) x *\<^sub>R x) = c' a *\<^sub>R a + (\<Sum>x \<in> T \<inter> T'. (cc'(a := c' a)) x *\<^sub>R x)"
-        by (simp add: anot)
-      also have "... = c' a *\<^sub>R a + (\<Sum>x \<in> S. (cc'(a := c' a)) x *\<^sub>R x)"
-        using \<open>T \<subseteq> S\<close> False cc0 by (fastforce intro!: sum.mono_neutral_left split: if_split_asm)
-      also have "... = c a *\<^sub>R a + x - c a *\<^sub>R a"
-        by (simp add: wsumSS \<open>a \<notin> S\<close> if_smult sum_delta_notmem)
-      finally show "(\<Sum>x\<in>insert a (T \<inter> T'). (cc'(a := c' a)) x *\<^sub>R x) = x"
-        by simp
-    qed
+      by (force simp: convex_hull_finite c'0 intro!: ge0 1 self exI [where x = "cc'(a := c' a)"])
   qed
 qed
 
@@ -5584,17 +5587,20 @@
     also have "... = card ((\<lambda>x. e *\<^sub>R x) ` B)"
       using \<open>0 < e\<close>  by (force simp: inj_on_def card_image)
     also have "... \<le> dim ((\<lambda>x. - a + x) ` S)"
-    proof (simp, rule independent_card_le_dim)
+    proof -
       have e': "cball 0 e \<inter> (\<lambda>x. x - a) ` T \<subseteq> (\<lambda>x. x - a) ` S"
         using e by (auto simp: dist_norm norm_minus_commute subset_eq)
       have "(\<lambda>x. e *\<^sub>R x) ` B \<subseteq> cball 0 e \<inter> (\<lambda>x. x - a) ` T"
         using Bsub \<open>0 < e\<close> eq1 subT' \<open>a \<in> T\<close> by (auto simp: subspace_def)
-      then show "(\<lambda>x. e *\<^sub>R x) ` B \<subseteq> (\<lambda>x. x - a) ` S"
+      then have "(\<lambda>x. e *\<^sub>R x) ` B \<subseteq> (\<lambda>x. x - a) ` S"
         using e' by blast
+      moreover
       have "inj_on ((*\<^sub>R) e) (span B)"
         using \<open>0 < e\<close> inj_on_def by fastforce
-      then show "independent ((\<lambda>x. e *\<^sub>R x) ` B)"
+      then have "independent ((\<lambda>x. e *\<^sub>R x) ` B)"
         using linear_scale_self \<open>independent B\<close> linear_dependent_inj_imageD by blast
+      ultimately show ?thesis
+        by (auto simp: intro!: independent_card_le_dim)
     qed
     also have "... = aff_dim S"
       using \<open>a \<in> S\<close> aff_dim_eq_dim hull_inc by (force cong: image_cong_simp)