# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1525009571 -3600
# Node ID 2cab37094fc451cb49076c0950e10749f57f454b
# Parent  ebd179b82e20e7a6e1512a61155b6ff02372611d
more defer/prefer

diff -r ebd179b82e20 -r 2cab37094fc4 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Apr 28 21:37:45 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Apr 29 14:46:11 2018 +0100
@@ -837,15 +837,13 @@
     qed
   } note ** = this
   show ?thesis
-  unfolding has_field_derivative_def
+    unfolding has_field_derivative_def
   proof (rule has_derivative_sequence [OF cvs _ _ x])
-    show "\<forall>n. \<forall>x\<in>s. (f n has_derivative (( * ) (f' n x))) (at x within s)"
-      by (metis has_field_derivative_def df)
-  next show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
+  show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
     by (rule tf)
-  next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
+  next show "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
     by (blast intro: **)
-  qed
+  qed (metis has_field_derivative_def df)
 qed
 
 lemma has_complex_derivative_series:
@@ -884,7 +882,7 @@
       by (metis df has_field_derivative_def mult_commute_abs)
   next show " ((\<lambda>n. f n x) sums l)"
     by (rule sf)
-  next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
+  next show "\<And>e. e>0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
     by (blast intro: **)
   qed
 qed
@@ -896,7 +894,7 @@
   assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
-  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
+  shows  "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
 proof -
   from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
     unfolding uniformly_convergent_on_def by blast
@@ -905,7 +903,6 @@
     by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
   then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
     "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
-  from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
   from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
     by (simp add: has_field_derivative_def s)
   have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
@@ -915,15 +912,6 @@
     by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
 qed
 
-lemma field_differentiable_series':
-  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
-  assumes "convex s" "open s"
-  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
-  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
-  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
-  shows   "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x0)"
-  using field_differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
-
 subsection\<open>Bound theorem\<close>
 
 lemma field_differentiable_bound:
diff -r ebd179b82e20 -r 2cab37094fc4 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Sat Apr 28 21:37:45 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Sun Apr 29 14:46:11 2018 +0100
@@ -1197,13 +1197,13 @@
 
 lemma has_derivative_inverse_basic:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  assumes "(f has_derivative f') (at (g y))"
-    and "bounded_linear g'"
+  assumes derf: "(f has_derivative f') (at (g y))"
+    and ling': "bounded_linear g'"
     and "g' \<circ> f' = id"
-    and "continuous (at y) g"
-    and "open t"
-    and "y \<in> t"
-    and "\<forall>z\<in>t. f (g z) = z"
+    and contg: "continuous (at y) g"
+    and "open T"
+    and "y \<in> T"
+    and fg: "\<And>z. z \<in> T \<Longrightarrow> f (g z) = z"
   shows "(g has_derivative g') (at y)"
 proof -
   interpret f': bounded_linear f'
@@ -1214,70 +1214,48 @@
     using bounded_linear.pos_bounded[OF assms(2)] by blast
   have lem1: "\<forall>e>0. \<exists>d>0. \<forall>z.
     norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)"
-  proof (rule, rule)
+  proof (intro allI impI)
     fix e :: real
     assume "e > 0"
     with C(1) have *: "e / C > 0" by auto
-    obtain d0 where d0:
-        "0 < d0"
-        "\<forall>ya. norm (ya - g y) < d0 \<longrightarrow> norm (f ya - f (g y) - f' (ya - g y)) \<le> e / C * norm (ya - g y)"
-      using assms(1)
-      unfolding has_derivative_at_alt
-      using * by blast
-    obtain d1 where d1:
-        "0 < d1"
-        "\<forall>x. 0 < dist x y \<and> dist x y < d1 \<longrightarrow> dist (g x) (g y) < d0"
-      using assms(4)
-      unfolding continuous_at Lim_at
-      using d0(1) by blast
-    obtain d2 where d2:
-        "0 < d2"
-        "\<forall>ya. dist ya y < d2 \<longrightarrow> ya \<in> t"
-      using assms(5)
-      unfolding open_dist
-      using assms(6) by blast
+    obtain d0 where  "0 < d0" and d0:
+        "\<And>u. norm (u - g y) < d0 \<Longrightarrow> norm (f u - f (g y) - f' (u - g y)) \<le> e / C * norm (u - g y)"
+      using derf * unfolding has_derivative_at_alt by blast
+    obtain d1 where "0 < d1" and d1: "\<And>x. \<lbrakk>0 < dist x y; dist x y < d1\<rbrakk> \<Longrightarrow> dist (g x) (g y) < d0"
+      using contg \<open>0 < d0\<close> unfolding continuous_at Lim_at by blast
+    obtain d2 where "0 < d2" and d2: "\<And>u. dist u y < d2 \<Longrightarrow> u \<in> T"
+      using \<open>open T\<close> \<open>y \<in> T\<close> unfolding open_dist by blast
     obtain d where d: "0 < d" "d < d1" "d < d2"
-      using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
-    then show "\<exists>d>0. \<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
-      apply (rule_tac x=d in exI)
-      apply rule
-      defer
-      apply rule
-      apply rule
-    proof -
+      using real_lbound_gt_zero[OF \<open>0 < d1\<close> \<open>0 < d2\<close>] by blast
+    show "\<exists>d>0. \<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
+    proof (intro exI allI impI conjI)
       fix z
       assume as: "norm (z - y) < d"
-      then have "z \<in> t"
+      then have "z \<in> T"
         using d2 d unfolding dist_norm by auto
       have "norm (g z - g y - g' (z - y)) \<le> norm (g' (f (g z) - y - f' (g z - g y)))"
         unfolding g'.diff f'.diff
-        unfolding assms(3)[unfolded o_def id_def, THEN fun_cong]
-        unfolding assms(7)[rule_format,OF \<open>z\<in>t\<close>]
-        apply (subst norm_minus_cancel[symmetric])
-        apply auto
-        done
+        unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] fg[OF \<open>z\<in>T\<close>]
+        by (simp add: norm_minus_commute)
       also have "\<dots> \<le> norm (f (g z) - y - f' (g z - g y)) * C"
         by (rule C(2))
       also have "\<dots> \<le> (e / C) * norm (g z - g y) * C"
-        apply (rule mult_right_mono)
-        apply (rule d0(2)[rule_format,unfolded assms(7)[rule_format,OF \<open>y\<in>t\<close>]])
-        apply (cases "z = y")
-        defer
-        apply (rule d1(2)[unfolded dist_norm,rule_format])
-        using as d C d0
-        apply auto
-        done
+      proof -
+        have "norm (g z - g y) < d0"
+          by (metis as cancel_comm_monoid_add_class.diff_cancel d(2) \<open>0 < d0\<close> d1 diff_gt_0_iff_gt diff_strict_mono dist_norm dist_self zero_less_dist_iff)
+        then show ?thesis
+          by (metis C(1) \<open>y \<in> T\<close> d0 fg real_mult_le_cancel_iff1)
+      qed
       also have "\<dots> \<le> e * norm (g z - g y)"
         using C by (auto simp add: field_simps)
       finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
         by simp
-    qed auto
+    qed (use d in auto)
   qed
   have *: "(0::real) < 1 / 2"
     by auto
-  obtain d where d:
-      "0 < d"
-      "\<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> 1 / 2 * norm (g z - g y)"
+  obtain d where "0 < d" and d:
+      "\<And>z. norm (z - y) < d \<Longrightarrow> norm (g z - g y - g' (z - y)) \<le> 1/2 * norm (g z - g y)"
     using lem1 * by blast
   define B where "B = C * 2"
   have "B > 0"
@@ -1287,51 +1265,37 @@
     have "norm (g z - g y) \<le> norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))"
       by (rule norm_triangle_sub)
     also have "\<dots> \<le> norm (g' (z - y)) + 1 / 2 * norm (g z - g y)"
-      apply (rule add_left_mono)
-      using d and z
-      apply auto
-      done
+      by (rule add_left_mono) (use d z in auto)
     also have "\<dots> \<le> norm (z - y) * C + 1 / 2 * norm (g z - g y)"
-      apply (rule add_right_mono)
-      using C
-      apply auto
-      done
+      by (rule add_right_mono) (use C in auto)
     finally show "norm (g z - g y) \<le> B * norm (z - y)"
       unfolding B_def
       by (auto simp add: field_simps)
   qed
   show ?thesis
     unfolding has_derivative_at_alt
-    apply rule
-    apply (rule assms)
-    apply rule
-    apply rule
-  proof -
+  proof (intro conjI assms allI impI)
     fix e :: real
     assume "e > 0"
     then have *: "e / B > 0" by (metis \<open>B > 0\<close> divide_pos_pos)
-    obtain d' where d':
-        "0 < d'"
-        "\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
+    obtain d' where "0 < d'" and d':
+        "\<And>z. norm (z - y) < d' \<Longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
       using lem1 * by blast
     obtain k where k: "0 < k" "k < d" "k < d'"
-      using real_lbound_gt_zero[OF d(1) d'(1)] by blast
+      using real_lbound_gt_zero[OF \<open>0 < d\<close> \<open>0 < d'\<close>] by blast
     show "\<exists>d>0. \<forall>ya. norm (ya - y) < d \<longrightarrow> norm (g ya - g y - g' (ya - y)) \<le> e * norm (ya - y)"
-      apply (rule_tac x=k in exI)
-      apply auto
-    proof -
+    proof (intro exI allI impI conjI)
       fix z
       assume as: "norm (z - y) < k"
       then have "norm (g z - g y - g' (z - y)) \<le> e / B * norm(g z - g y)"
         using d' k by auto
       also have "\<dots> \<le> e * norm (z - y)"
         unfolding times_divide_eq_left pos_divide_le_eq[OF \<open>B>0\<close>]
-        using lem2[of z]
-        using k as using \<open>e > 0\<close>
+        using lem2[of z] k as \<open>e > 0\<close>
         by (auto simp add: field_simps)
       finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)"
         by simp
-    qed(insert k, auto)
+    qed (use k in auto)
   qed
 qed
 
@@ -1344,25 +1308,22 @@
     and "g' \<circ> f' = id"
     and "continuous (at (f x)) g"
     and "g (f x) = x"
-    and "open t"
-    and "f x \<in> t"
-    and "\<forall>y\<in>t. f (g y) = y"
+    and "open T"
+    and "f x \<in> T"
+    and "\<And>y. y \<in> T \<Longrightarrow> f (g y) = y"
   shows "(g has_derivative g') (at (f x))"
-  apply (rule has_derivative_inverse_basic)
-  using assms
-  apply auto
-  done
+  by (rule has_derivative_inverse_basic) (use assms in auto)
 
 text \<open>This is the version in Dieudonne', assuming continuity of f and g.\<close>
 
 lemma has_derivative_inverse_dieudonne:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  assumes "open s"
-    and "open (f ` s)"
-    and "continuous_on s f"
-    and "continuous_on (f ` s) g"
-    and "\<forall>x\<in>s. g (f x) = x"
-    and "x \<in> s"
+  assumes "open S"
+    and "open (f ` S)"
+    and "continuous_on S f"
+    and "continuous_on (f ` S) g"
+    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+    and "x \<in> S"
     and "(f has_derivative f') (at x)"
     and "bounded_linear g'"
     and "g' \<circ> f' = id"
@@ -1377,11 +1338,11 @@
 
 lemma has_derivative_inverse:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  assumes "compact s"
-    and "x \<in> s"
-    and "f x \<in> interior (f ` s)"
-    and "continuous_on s f"
-    and "\<forall>y\<in>s. g (f y) = y"
+  assumes "compact S"
+    and "x \<in> S"
+    and fx: "f x \<in> interior (f ` S)"
+    and "continuous_on S f"
+    and "\<And>y. y \<in> S \<Longrightarrow> g (f y) = y"
     and "(f has_derivative f') (at x)"
     and "bounded_linear g'"
     and "g' \<circ> f' = id"
@@ -1389,20 +1350,17 @@
 proof -
   {
     fix y
-    assume "y \<in> interior (f ` s)"
-    then obtain x where "x \<in> s" and *: "y = f x"
-      unfolding image_iff
-      using interior_subset
-      by auto
+    assume "y \<in> interior (f ` S)"
+    then obtain x where "x \<in> S" and *: "y = f x"
+      by (meson imageE interior_subset subsetCE)
     have "f (g y) = y"
-      unfolding * and assms(5)[rule_format,OF \<open>x\<in>s\<close>] ..
+      unfolding * and assms(5)[rule_format,OF \<open>x\<in>S\<close>] ..
   } note * = this
   show ?thesis
-    apply (rule has_derivative_inverse_basic_x[OF assms(6-8)])
-    apply (rule continuous_on_interior[OF _ assms(3)])
-    apply (rule continuous_on_inv[OF assms(4,1)])
-    apply (rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
-    apply (metis *)
+    apply (rule has_derivative_inverse_basic_x[OF assms(6-8), where T = "interior (f ` S)"])
+    apply (rule continuous_on_interior[OF _ fx])
+    apply (rule continuous_on_inv)
+    apply (simp_all add: assms *)
     done
 qed
 
@@ -1411,13 +1369,13 @@
 
 lemma brouwer_surjective:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "compact t"
-    and "convex t"
-    and "t \<noteq> {}"
-    and "continuous_on t f"
-    and "\<forall>x\<in>s. \<forall>y\<in>t. x + (y - f y) \<in> t"
-    and "x \<in> s"
-  shows "\<exists>y\<in>t. f y = x"
+  assumes "compact T"
+    and "convex T"
+    and "T \<noteq> {}"
+    and "continuous_on T f"
+    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
+    and "x \<in> S"
+  shows "\<exists>y\<in>T. f y = x"
 proof -
   have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
     by (auto simp add: algebra_simps)
@@ -1432,10 +1390,10 @@
 
 lemma brouwer_surjective_cball:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "e > 0"
-    and "continuous_on (cball a e) f"
-    and "\<forall>x\<in>s. \<forall>y\<in>cball a e. x + (y - f y) \<in> cball a e"
-    and "x \<in> s"
+  assumes "continuous_on (cball a e) f"
+    and "e > 0"
+    and "x \<in> S"
+    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
   shows "\<exists>y\<in>cball a e. f y = x"
   apply (rule brouwer_surjective)
   apply (rule compact_cball convex_cball)+
@@ -1448,14 +1406,14 @@
 
 lemma sussmann_open_mapping:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
-  assumes "open s"
-    and "continuous_on s f"
-    and "x \<in> s"
+  assumes "open S"
+    and "continuous_on S f"
+    and "x \<in> S"
     and "(f has_derivative f') (at x)"
     and "bounded_linear g'" "f' \<circ> g' = id"
-    and "t \<subseteq> s"
-    and "x \<in> interior t"
-  shows "f x \<in> interior (f ` t)"
+    and "T \<subseteq> S"
+    and "x \<in> interior T"
+  shows "f x \<in> interior (f ` T)"
 proof -
   interpret f': bounded_linear f'
     using assms
@@ -1473,31 +1431,17 @@
     using assms(4)
     unfolding has_derivative_at_alt
     using * by blast
-  obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> t"
+  obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
     using assms(8)
     unfolding mem_interior_cball
     by blast
   have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
   obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
     using real_lbound_gt_zero[OF *] by blast
-  have "\<forall>z\<in>cball (f x) (e / 2). \<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z"
-    apply rule
-    apply (rule brouwer_surjective_cball[where s="cball (f x) (e/2)"])
-    prefer 3
-    apply rule
-    apply rule
-  proof-
-    show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
-      unfolding g'.diff
-      apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
-      apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
-      apply (rule continuous_on_subset[OF assms(2)])
-      apply rule
-      apply (unfold image_iff)
-      apply (erule bexE)
+  have lem: "\<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" if "z\<in>cball (f x) (e / 2)" for z
+  proof (rule brouwer_surjective_cball)
+    have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
     proof-
-      fix y z
-      assume as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))"
       have "dist x z = norm (g' (f x) - g' y)"
         unfolding as(2) and dist_norm by auto
       also have "\<dots> \<le> norm (f x - y) * B"
@@ -1516,9 +1460,16 @@
       finally have "z \<in> cball x e1"
         unfolding mem_cball
         by force
-      then show "z \<in> s"
+      then show "z \<in> S"
         using e1 assms(7) by auto
     qed
+    show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
+      unfolding g'.diff
+      apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
+       apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
+      apply (rule continuous_on_subset[OF assms(2)])
+      using z
+      by blast
   next
     fix y z
     assume as: "y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e"
@@ -1528,7 +1479,7 @@
       apply (rule mult_right_mono)
       using as(2)[unfolded mem_cball dist_norm] and B
       unfolding norm_minus_commute
-      apply auto
+       apply auto
       done
     also have "\<dots> < e0"
       using e and B
@@ -1563,7 +1514,7 @@
     finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
       unfolding mem_cball dist_norm
       by auto
-  qed (insert e, auto) note lem = this
+  qed (use e that in auto) 
   show ?thesis
     unfolding mem_interior
     apply (rule_tac x="e/2" in exI)
@@ -1589,13 +1540,13 @@
       done
     also have "\<dots> \<le> e1"
       using e B unfolding less_divide_eq by auto
-    finally have "x + g'(z - f x) \<in> t"
+    finally have "x + g'(z - f x) \<in> T"
       apply -
       apply (rule e1(2)[unfolded subset_eq,rule_format])
       unfolding mem_cball dist_norm
       apply auto
       done
-    then show "y \<in> f ` t"
+    then show "y \<in> f ` T"
       using z by auto
   qed (insert e, auto)
 qed
@@ -1750,9 +1701,9 @@
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes "a \<in> s"
       and "open s"
-      and "bounded_linear g'"
+      and bling: "bounded_linear g'"
       and "g' \<circ> f' a = id"
-      and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x)"
+      and derf: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x)"
       and "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < e"
   obtains r where "r > 0" "ball a r \<subseteq> s" "inj_on f (ball a r)"
 proof -
@@ -1760,11 +1711,7 @@
     using assms by auto
   note f'g' = assms(4)[unfolded id_def o_def,THEN cong]
   have "g' (f' a (\<Sum>Basis)) = (\<Sum>Basis)" "(\<Sum>Basis) \<noteq> (0::'n)"
-    defer
-    apply (subst euclidean_eq_iff)
-    using f'g'
-    apply auto
-    done
+    using f'g' by auto
   then have *: "0 < onorm g'"
     unfolding onorm_pos_lt[OF assms(3)]
     by fastforce
@@ -1812,17 +1759,11 @@
         have *: "(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)"
           unfolding o_def and diff
           using f'g' by auto
+        have blin: "bounded_linear (f' a)"
+          using \<open>a \<in> s\<close> derf by blast
         show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
-          unfolding ph' *
-          apply (simp add: comp_def)
-          apply (rule bounded_linear.has_derivative[OF assms(3)])
-          apply (rule derivative_intros)
-          defer
-          apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
-          apply (rule has_derivative_at_withinI)
-          using assms(5) and \<open>u \<in> s\<close> \<open>a \<in> s\<close>
-          apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
-          done
+          unfolding ph' * comp_def
+          by (rule \<open>u \<in> s\<close> derivative_eq_intros has_derivative_at_withinI [OF derf] bounded_linear.has_derivative [OF blin]  bounded_linear.has_derivative [OF bling] |simp)+
         have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
           apply (rule_tac[!] bounded_linear_sub)
           apply (rule_tac[!] has_derivative_bounded_linear)
@@ -1896,21 +1837,20 @@
   qed
 qed
 
-lemma has_derivative_sequence_lipschitz:
+lemma has_derivative_sequence_Lipschitz:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  assumes "convex s"
-    and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
-    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
-  shows "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
+  assumes "convex S"
+    and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
+    and "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
+    and "e > 0"
+  shows "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S.
     norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
-proof (rule, rule)
-  fix e :: real
-  assume "e > 0"
-  then have *: "2 * (1/2* e) = e" "1/2 * e >0"
-    by auto
-  obtain N where "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> 1 / 2 * e * norm h"
+proof -
+  have *: "2 * (1/2* e) = e" "1/2 * e >0"
+    using \<open>e>0\<close> by auto
+  obtain N where "\<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> 1 / 2 * e * norm h"
     using assms(3) *(2) by blast
-  then show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
+  then show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
     apply (rule_tac x=N in exI)
     apply (rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *])
     using assms \<open>e > 0\<close>
@@ -1920,22 +1860,22 @@
 
 lemma has_derivative_sequence:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
-  assumes "convex s"
-    and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
-    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
-    and "x0 \<in> s"
+  assumes "convex S"
+    and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
+    and "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
+    and "x0 \<in> S"
     and "((\<lambda>n. f n x0) \<longlongrightarrow> l) sequentially"
-  shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g'(x)) (at x within s)"
+  shows "\<exists>g. \<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g'(x)) (at x within S)"
 proof -
-  have lem1: "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
+  have lem1: "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S.
       norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
-    using assms(1,2,3) by (rule has_derivative_sequence_lipschitz)
-  have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
+    using assms(1,2,3) by (rule has_derivative_sequence_Lipschitz)
+  have "\<exists>g. \<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
     apply (rule bchoice)
     unfolding convergent_eq_Cauchy
   proof
     fix x
-    assume "x \<in> s"
+    assume "x \<in> S"
     show "Cauchy (\<lambda>n. f n x)"
     proof (cases "x = x0")
       case True
@@ -1945,7 +1885,7 @@
       case False
       show ?thesis
         unfolding Cauchy_def
-      proof (rule, rule)
+      proof (intro allI impI)
         fix e :: real
         assume "e > 0"
         hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto
@@ -1955,12 +1895,11 @@
           using *(1) by blast
         obtain N where N:
           "\<forall>m\<ge>N. \<forall>n\<ge>N.
-            \<forall>xa\<in>s. \<forall>y\<in>s. norm (f m xa - f n xa - (f m y - f n y)) \<le>
+            \<forall>xa\<in>S. \<forall>y\<in>S. norm (f m xa - f n xa - (f m y - f n y)) \<le>
               e / 2 / norm (x - x0) * norm (xa - y)"
         using lem1 *(2) by blast
         show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
-          apply (rule_tac x="max M N" in exI)
-        proof rule+
+        proof (intro exI allI impI)
           fix m n
           assume as: "max M N \<le>m" "max M N\<le>n"
           have "dist (f m x) (f n x) \<le>
@@ -1968,7 +1907,7 @@
             unfolding dist_norm
             by (rule norm_triangle_sub)
           also have "\<dots> \<le> norm (f m x0 - f n x0) + e / 2"
-            using N[rule_format,OF _ _ \<open>x\<in>s\<close> \<open>x0\<in>s\<close>, of m n] and as and False
+            using N[rule_format,OF _ _ \<open>x\<in>S\<close> \<open>x0\<in>S\<close>, of m n] and as and False
             by auto
           also have "\<dots> < e / 2 + e / 2"
             apply (rule add_strict_right_mono)
@@ -1982,27 +1921,24 @@
       qed
     qed
   qed
-  then obtain g where g: "\<forall>x\<in>s. (\<lambda>n. f n x) \<longlonglongrightarrow> g x" ..
-  have lem2: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)"
+  then obtain g where g: "\<forall>x\<in>S. (\<lambda>n. f n x) \<longlonglongrightarrow> g x" ..
+  have lem2: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)"
   proof (rule, rule)
     fix e :: real
     assume *: "e > 0"
     obtain N where
-      N: "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
+      N: "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
       using lem1 * by blast
-    show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
+    show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
       apply (rule_tac x=N in exI)
     proof rule+
       fix n x y
-      assume as: "N \<le> n" "x \<in> s" "y \<in> s"
+      assume as: "N \<le> n" "x \<in> S" "y \<in> S"
       have "((\<lambda>m. norm (f n x - f n y - (f m x - f m y))) \<longlongrightarrow> norm (f n x - f n y - (g x - g y))) sequentially"
         by (intro tendsto_intros g[rule_format] as)
       moreover have "eventually (\<lambda>m. norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)) sequentially"
         unfolding eventually_sequentially
-        apply (rule_tac x=N in exI)
-        apply rule
-        apply rule
-      proof -
+      proof (intro exI allI impI)
         fix m
         assume "N \<le> m"
         then show "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)"
@@ -2013,11 +1949,11 @@
         by (simp add: tendsto_upperbound)
     qed
   qed
-  have "\<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within s)"
+  have "\<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within S)"
     unfolding has_derivative_within_alt2
   proof (intro ballI conjI)
     fix x
-    assume "x \<in> s"
+    assume "x \<in> S"
     then show "((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
       by (simp add: g)
     have lem3: "\<forall>u. ((\<lambda>n. f' n x u) \<longlongrightarrow> g' x u) sequentially"
@@ -2030,7 +1966,7 @@
       proof (cases "u = 0")
         case True
         have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e * norm u) sequentially"
-          using assms(3)[folded eventually_sequentially] and \<open>0 < e\<close> and \<open>x \<in> s\<close>
+          using assms(3)[folded eventually_sequentially] and \<open>0 < e\<close> and \<open>x \<in> S\<close>
           by (fast elim: eventually_mono)
         then show ?thesis
           using \<open>u = 0\<close> and \<open>0 < e\<close> by (auto elim: eventually_mono)
@@ -2038,7 +1974,7 @@
         case False
         with \<open>0 < e\<close> have "0 < e / norm u" by simp
         then have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e / norm u * norm u) sequentially"
-          using assms(3)[folded eventually_sequentially] and \<open>x \<in> s\<close>
+          using assms(3)[folded eventually_sequentially] and \<open>x \<in> S\<close>
           by (fast elim: eventually_mono)
         then show ?thesis
           using \<open>u \<noteq> 0\<close> by simp
@@ -2048,7 +1984,7 @@
     proof
       fix x' y z :: 'a
       fix c :: real
-      note lin = assms(2)[rule_format,OF \<open>x\<in>s\<close>,THEN has_derivative_bounded_linear]
+      note lin = assms(2)[rule_format,OF \<open>x\<in>S\<close>,THEN has_derivative_bounded_linear]
       show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
         apply (rule tendsto_unique[OF trivial_limit_sequentially])
         apply (rule lem3[rule_format])
@@ -2064,9 +2000,9 @@
         apply (rule lem3[rule_format])+
         done
       obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
-        using assms(3) \<open>x \<in> s\<close> by (fast intro: zero_less_one)
+        using assms(3) \<open>x \<in> S\<close> by (fast intro: zero_less_one)
       have "bounded_linear (f' N x)"
-        using assms(2) \<open>x \<in> s\<close> by fast
+        using assms(2) \<open>x \<in> S\<close> by fast
       from bounded_linear.bounded [OF this]
       obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
       {
@@ -2082,36 +2018,36 @@
       }
       then show "\<exists>K. \<forall>h. norm (g' x h) \<le> norm h * K" by fast
     qed
-    show "\<forall>e>0. eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within s)"
+    show "\<forall>e>0. eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within S)"
     proof (rule, rule)
       fix e :: real
       assume "e > 0"
       then have *: "e / 3 > 0"
         by auto
-      obtain N1 where N1: "\<forall>n\<ge>N1. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e / 3 * norm h"
+      obtain N1 where N1: "\<forall>n\<ge>N1. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e / 3 * norm h"
         using assms(3) * by blast
       obtain N2 where
-          N2: "\<forall>n\<ge>N2. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e / 3 * norm (x - y)"
+          N2: "\<forall>n\<ge>N2. \<forall>x\<in>S. \<forall>y\<in>S. norm (f n x - f n y - (g x - g y)) \<le> e / 3 * norm (x - y)"
         using lem2 * by blast
       let ?N = "max N1 N2"
-      have "eventually (\<lambda>y. norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)) (at x within s)"
-        using assms(2)[unfolded has_derivative_within_alt2] and \<open>x \<in> s\<close> and * by fast
-      moreover have "eventually (\<lambda>y. y \<in> s) (at x within s)"
+      have "eventually (\<lambda>y. norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)) (at x within S)"
+        using assms(2)[unfolded has_derivative_within_alt2] and \<open>x \<in> S\<close> and * by fast
+      moreover have "eventually (\<lambda>y. y \<in> S) (at x within S)"
         unfolding eventually_at by (fast intro: zero_less_one)
-      ultimately show "\<forall>\<^sub>F y in at x within s. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
+      ultimately show "\<forall>\<^sub>F y in at x within S. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
       proof (rule eventually_elim2)
         fix y
-        assume "y \<in> s"
+        assume "y \<in> S"
         assume "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)"
         moreover have "norm (g y - g x - (f ?N y - f ?N x)) \<le> e / 3 * norm (y - x)"
-          using N2[rule_format, OF _ \<open>y \<in> s\<close> \<open>x \<in> s\<close>]
+          using N2[rule_format, OF _ \<open>y \<in> S\<close> \<open>x \<in> S\<close>]
           by (simp add: norm_minus_commute)
         ultimately have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)"
           using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"]
           by (auto simp add: algebra_simps)
         moreover
         have " norm (f' ?N x (y - x) - g' x (y - x)) \<le> e / 3 * norm (y - x)"
-          using N1 \<open>x \<in> s\<close> by auto
+          using N1 \<open>x \<in> S\<close> by auto
         ultimately show "norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
           using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"]
           by (auto simp add: algebra_simps)
@@ -2125,77 +2061,63 @@
 
 lemma has_antiderivative_sequence:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
-  assumes "convex s"
-    and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
-    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
-  shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g' x) (at x within s)"
-proof (cases "s = {}")
+  assumes "convex S"
+    and der: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
+    and no: "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
+  shows "\<exists>g. \<forall>x\<in>S. (g has_derivative g' x) (at x within S)"
+proof (cases "S = {}")
   case False
-  then obtain a where "a \<in> s"
+  then obtain a where "a \<in> S"
     by auto
-  have *: "\<And>P Q. \<exists>g. \<forall>x\<in>s. P g x \<and> Q g x \<Longrightarrow> \<exists>g. \<forall>x\<in>s. Q g x"
+  have *: "\<And>P Q. \<exists>g. \<forall>x\<in>S. P g x \<and> Q g x \<Longrightarrow> \<exists>g. \<forall>x\<in>S. Q g x"
     by auto
   show ?thesis
     apply (rule *)
-    apply (rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
-    apply (metis assms(2) has_derivative_add_const)
-    apply (rule \<open>a \<in> s\<close>)
+    apply (rule has_derivative_sequence [OF \<open>convex S\<close> _ no, of "\<lambda>n x. f n x + (f 0 a - f n a)"])
+       apply (metis assms(2) has_derivative_add_const)
+    using \<open>a \<in> S\<close> 
     apply auto
     done
 qed auto
 
 lemma has_antiderivative_limit:
   fixes g' :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'b::banach"
-  assumes "convex s"
-    and "\<forall>e>0. \<exists>f f'. \<forall>x\<in>s.
-      (f has_derivative (f' x)) (at x within s) \<and> (\<forall>h. norm (f' x h - g' x h) \<le> e * norm h)"
-  shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g' x) (at x within s)"
+  assumes "convex S"
+    and "\<And>e. e>0 \<Longrightarrow> \<exists>f f'. \<forall>x\<in>S.
+           (f has_derivative (f' x)) (at x within S) \<and> (\<forall>h. norm (f' x h - g' x h) \<le> e * norm h)"
+  shows "\<exists>g. \<forall>x\<in>S. (g has_derivative g' x) (at x within S)"
 proof -
-  have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>s.
-    (f has_derivative (f' x)) (at x within s) \<and>
+  have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>S.
+    (f has_derivative (f' x)) (at x within S) \<and>
     (\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)"
     by (simp add: assms(2))
   obtain f where
-    *: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. (f x has_derivative f' xa) (at xa within s) \<and>
-      (\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
-    using *[THEN choice] ..
+    *: "\<And>x. \<exists>f'. \<forall>xa\<in>S. (f x has_derivative f' xa) (at xa within S) \<and>
+        (\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
+    using * by metis
   obtain f' where
-    f: "\<forall>x. \<forall>xa\<in>s. (f x has_derivative f' x xa) (at xa within s) \<and>
-      (\<forall>h. norm (f' x xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
-    using *[THEN choice] ..
+    f': "\<And>x. \<forall>z\<in>S. (f x has_derivative f' x z) (at z within S) \<and>
+            (\<forall>h. norm (f' x z h - g' z h) \<le> inverse (real (Suc x)) * norm h)"
+    using * by metis
   show ?thesis
-    apply (rule has_antiderivative_sequence[OF assms(1), of f f'])
-    defer
-    apply rule
-    apply rule
-  proof -
+  proof (rule has_antiderivative_sequence[OF \<open>convex S\<close>, of f f'])
     fix e :: real
     assume "e > 0"
     obtain N where N: "inverse (real (Suc N)) < e"
       using reals_Archimedean[OF \<open>e>0\<close>] ..
-    show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
-      apply (rule_tac x=N in exI)
-      apply rule
-      apply rule
-      apply rule
-      apply rule
-    proof -
+    show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
+    proof (intro exI allI ballI impI)
       fix n x h
-      assume n: "N \<le> n" and x: "x \<in> s"
+      assume n: "N \<le> n" and x: "x \<in> S"
       have *: "inverse (real (Suc n)) \<le> e"
         apply (rule order_trans[OF _ N[THEN less_imp_le]])
         using n
         apply (auto simp add: field_simps)
         done
       show "norm (f' n x h - g' x h) \<le> e * norm h"
-        using f[rule_format,THEN conjunct2, OF x, of n, THEN spec[where x=h]]
-        apply (rule order_trans)
-        using N *
-        apply (cases "h = 0")
-        apply auto
-        done
+        by (meson "*" mult_right_mono norm_ge_zero order.trans x f')
     qed
-  qed (insert f, auto)
+  qed (use f' in auto)
 qed
 
 
@@ -2203,12 +2125,12 @@
 
 lemma has_derivative_series:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
-  assumes "convex s"
-    and "\<And>n x. x \<in> s \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within s)"
-    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (sum (\<lambda>i. f' i x h) {..<n} - g' x h) \<le> e * norm h"
-    and "x \<in> s"
+  assumes "convex S"
+    and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
+    and "\<And>e. e>0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (sum (\<lambda>i. f' i x h) {..<n} - g' x h) \<le> e * norm h"
+    and "x \<in> S"
     and "(\<lambda>n. f n x) sums l"
-  shows "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums (g x) \<and> (g has_derivative g' x) (at x within s)"
+  shows "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums (g x) \<and> (g has_derivative g' x) (at x within S)"
   unfolding sums_def
   apply (rule has_derivative_sequence[OF assms(1) _ assms(3)])
   apply (metis assms(2) has_derivative_sum)
@@ -2219,20 +2141,19 @@
 
 lemma has_field_derivative_series:
   fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
-  assumes "convex s"
-  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
-  assumes "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
-  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
-  shows   "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
+  assumes "convex S"
+  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x within S)"
+  assumes "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)"
+  shows   "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)"
 unfolding has_field_derivative_def
 proof (rule has_derivative_series)
-  show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h"
-  proof (intro allI impI)
-    fix e :: real assume "e > 0"
-    with assms(3) obtain N where N: "\<And>n x. n \<ge> N \<Longrightarrow> x \<in> s \<Longrightarrow> norm ((\<Sum>i<n. f' i x) - g' x) < e"
+  show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" if "e > 0" for e
+  proof -
+    from that assms(3) obtain N where N: "\<And>n x. n \<ge> N \<Longrightarrow> x \<in> S \<Longrightarrow> norm ((\<Sum>i<n. f' i x) - g' x) < e"
       unfolding uniform_limit_iff eventually_at_top_linorder dist_norm by blast
     {
-      fix n :: nat and x h :: 'a assume nx: "n \<ge> N" "x \<in> s"
+      fix n :: nat and x h :: 'a assume nx: "n \<ge> N" "x \<in> S"
       have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) = norm ((\<Sum>i<n. f' i x) - g' x) * norm h"
         by (simp add: norm_mult [symmetric] ring_distribs sum_distrib_right)
       also from N[OF nx] have "norm ((\<Sum>i<n. f' i x) - g' x) \<le> e" by simp
@@ -2240,55 +2161,55 @@
         by (intro mult_right_mono) simp_all
       finally have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" .
     }
-    thus "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" by blast
+    thus "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" by blast
   qed
-qed (insert assms, auto simp: has_field_derivative_def)
+qed (use assms in \<open>auto simp: has_field_derivative_def\<close>)
 
 lemma has_field_derivative_series':
   fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
-  assumes "convex s"
-  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
-  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
-  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" "x \<in> interior s"
+  assumes "convex S"
+  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x within S)"
+  assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
+  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)" "x \<in> interior S"
   shows   "summable (\<lambda>n. f n x)" "((\<lambda>x. \<Sum>n. f n x) has_field_derivative (\<Sum>n. f' n x)) (at x)"
 proof -
-  from \<open>x \<in> interior s\<close> have "x \<in> s" using interior_subset by blast
+  from \<open>x \<in> interior S\<close> have "x \<in> S" using interior_subset by blast
   define g' where [abs_def]: "g' x = (\<Sum>i. f' i x)" for x
-  from assms(3) have "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+  from assms(3) have "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
     by (simp add: uniformly_convergent_uniform_limit_iff suminf_eq_lim g'_def)
   from has_field_derivative_series[OF assms(1,2) this assms(4,5)] obtain g where g:
-    "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
-    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
-  from g(1)[OF \<open>x \<in> s\<close>] show "summable (\<lambda>n. f n x)" by (simp add: sums_iff)
-  from g(2)[OF \<open>x \<in> s\<close>] \<open>x \<in> interior s\<close> have "(g has_field_derivative g' x) (at x)"
-    by (simp add: at_within_interior[of x s])
+    "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
+    "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
+  from g(1)[OF \<open>x \<in> S\<close>] show "summable (\<lambda>n. f n x)" by (simp add: sums_iff)
+  from g(2)[OF \<open>x \<in> S\<close>] \<open>x \<in> interior S\<close> have "(g has_field_derivative g' x) (at x)"
+    by (simp add: at_within_interior[of x S])
   also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow>
                 ((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)"
-    using eventually_nhds_in_nhd[OF \<open>x \<in> interior s\<close>] interior_subset[of s] g(1)
+    using eventually_nhds_in_nhd[OF \<open>x \<in> interior S\<close>] interior_subset[of S] g(1)
     by (intro DERIV_cong_ev) (auto elim!: eventually_mono simp: sums_iff)
   finally show "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)" .
 qed
 
 lemma differentiable_series:
   fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
-  assumes "convex s" "open s"
-  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
-  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
-  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
+  assumes "convex S" "open S"
+  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+  assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
+  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)" and x: "x \<in> S"
   shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)"
 proof -
-  from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+  from assms(4) obtain g' where A: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
     unfolding uniformly_convergent_on_def by blast
-  from x and \<open>open s\<close> have s: "at x within s = at x" by (rule at_within_open)
-  have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
-    by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
-  then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
-    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
+  from x and \<open>open S\<close> have S: "at x within S = at x" by (rule at_within_open)
+  have "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)"
+    by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
+  then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
+    "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
   from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
   from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
-    by (simp add: has_field_derivative_def s)
+    by (simp add: has_field_derivative_def S)
   have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
-    by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
+    by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
        (insert g, auto simp: sums_iff)
   thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
     by (auto simp: summable_def differentiable_def has_field_derivative_def)
@@ -2296,32 +2217,32 @@
 
 lemma differentiable_series':
   fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
-  assumes "convex s" "open s"
-  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
-  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
-  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
+  assumes "convex S" "open S"
+  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+  assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
+  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)"
   shows   "(\<lambda>x. \<Sum>n. f n x) differentiable (at x0)"
-  using differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
+  using differentiable_series[OF assms, of x0] \<open>x0 \<in> S\<close> by blast+
 
 text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
 
 definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
 
 lemma vector_derivative_unique_within:
-  assumes not_bot: "at x within s \<noteq> bot"
-    and f': "(f has_vector_derivative f') (at x within s)"
-    and f'': "(f has_vector_derivative f'') (at x within s)"
+  assumes not_bot: "at x within S \<noteq> bot"
+    and f': "(f has_vector_derivative f') (at x within S)"
+    and f'': "(f has_vector_derivative f'') (at x within S)"
   shows "f' = f''"
 proof -
   have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
   proof (rule frechet_derivative_unique_within)
-    show "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> s"
+    show "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> S"
     proof clarsimp
       fix e :: real assume "0 < e"
-      with islimpt_approachable_real[of x s] not_bot
-      obtain x' where "x' \<in> s" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
+      with islimpt_approachable_real[of x S] not_bot
+      obtain x' where "x' \<in> S" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
         by (auto simp add: trivial_limit_within)
-      then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> s"
+      then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> S"
         by (intro exI[of _ "x' - x"]) auto
     qed
   qed (insert f' f'', auto simp: has_vector_derivative_def)
@@ -2351,8 +2272,8 @@
 qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def)
 
 lemma vector_derivative_within:
-  assumes not_bot: "at x within s \<noteq> bot" and y: "(f has_vector_derivative y) (at x within s)"
-  shows "vector_derivative f (at x within s) = y"
+  assumes not_bot: "at x within S \<noteq> bot" and y: "(f has_vector_derivative y) (at x within S)"
+  shows "vector_derivative f (at x within S) = y"
   using y
   by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
      (auto simp: differentiable_def has_vector_derivative_def)
@@ -2381,11 +2302,11 @@
   by (metis has_field_derivative_def has_real_derivative)
 
 lemma has_vector_derivative_cong_ev:
-  assumes *: "eventually (\<lambda>x. x \<in> s \<longrightarrow> f x = g x) (nhds x)" "f x = g x"
-  shows "(f has_vector_derivative f') (at x within s) = (g has_vector_derivative f') (at x within s)"
+  assumes *: "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x = g x) (nhds x)" "f x = g x"
+  shows "(f has_vector_derivative f') (at x within S) = (g has_vector_derivative f') (at x within S)"
   unfolding has_vector_derivative_def has_derivative_def
   using *
-  apply (cases "at x within s \<noteq> bot")
+  apply (cases "at x within S \<noteq> bot")
   apply (intro refl conj_cong filterlim_cong)
   apply (auto simp: netlimit_within eventually_at_filter elim: eventually_mono)
   done