src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

     defer
     apply (erule bexE)
   proof -
     fix y
     assume as: "y\<in>cbox (x - ?d) (x + ?d)"
-    {
-      fix i :: 'a
-      assume i: "i \<in> Basis"
-      have "x \<bullet> i \<le> d + y \<bullet> i" "y \<bullet> i \<le> d + x \<bullet> i"
-        using as[unfolded mem_box, THEN bspec[where x=i]] i
-        by (auto simp: inner_simps)
-      then have "1 \<ge> inverse d * (x \<bullet> i - y \<bullet> i)" "1 \<ge> inverse d * (y \<bullet> i - x \<bullet> i)"
-        apply (rule_tac[!] mult_left_le_imp_le[OF _ assms])
-        unfolding mult.assoc[symmetric]
-        using assms
-        by (auto simp add: field_simps)
-      then have "inverse d * (x \<bullet> i * 2) \<le> 2 + inverse d * (y \<bullet> i * 2)"
-        "inverse d * (y \<bullet> i * 2) \<le> 2 + inverse d * (x \<bullet> i * 2)"
-        using `0<d` by (auto simp add: field_simps) }
     then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
-      unfolding mem_box using assms
-      by (auto simp add: field_simps inner_simps simp del: inverse_eq_divide)
-    then show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
-      apply -
-      apply (rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
-      using assms
-      apply auto
-      done
+      using assms by (simp add: mem_box field_simps inner_simps)
+    with `0 < d` show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
+      by (intro bexI[of _ "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) auto
   next
     fix y z
     assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
     have "\<And>i. i\<in>Basis \<Longrightarrow> 0 \<le> d * (z \<bullet> i) \<and> d * (z \<bullet> i) \<le> d"
       using assms as(1)[unfolded mem_box]

         have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y"
           using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
           using `0 < t` `2 < t` and `y \<in> s` `w \<in> s`
           by (auto simp add:field_simps)
         also have "\<dots> = (f w + t * f y) / (1 + t)"
-          using `t > 0` unfolding divide_inverse by (auto simp add: field_simps)
+          using `t > 0` by (auto simp add: divide_simps)
         also have "\<dots> < e + f y"
           using `t > 0` * `e > 0` by (auto simp add: field_simps)
         finally have "f x - f y < e" by auto
       }
       ultimately show ?thesis by auto