# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1526837854 -3600
# Node ID 0764ee22a4d19baa90a7d892da38385b197ef34b
# Parent  88dd06301dd30f5fcf0435db1256749bc10bc5e8
tidy up of Derivative

diff -r 88dd06301dd3 -r 0764ee22a4d1 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun May 20 18:37:34 2018 +0100
@@ -1154,7 +1154,7 @@
           vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})"
       apply (rule vector_derivative_at_within_ivl
                   [OF has_vector_derivative_transform_within_open
-                      [where f = "(shiftpath (1 - a) (shiftpath a g))" and s = "{0<..<1}-s"]])
+                      [where f = "(shiftpath (1 - a) (shiftpath a g))" and S = "{0<..<1}-s"]])
       using s g assms x
       apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
                         vector_derivative_within_interior vector_derivative_works [symmetric])
@@ -4453,7 +4453,7 @@
     case True then show ?thesis
       apply (simp add: continuous_within)
       apply (rule Lim_transform_away_within [of _ "z+1" _ "\<lambda>w::complex. (f w - f z)/(w - z)"])
-      using has_field_derivative_at_within DERIV_within_iff f'
+      using has_field_derivative_at_within has_field_derivative_iff f'
       apply (fastforce simp add:)+
       done
   next
@@ -5554,7 +5554,7 @@
     apply (rule w)
     done
   show ?thes2
-    apply (simp add: DERIV_within_iff del: power_Suc)
+    apply (simp add: has_field_derivative_iff del: power_Suc)
     apply (rule Lim_transform_within [OF tendsto_mult_left [OF *] \<open>0 < d\<close> ])
     apply (simp add: \<open>k \<noteq> 0\<close> **)
     done
diff -r 88dd06301dd3 -r 0764ee22a4d1 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun May 20 18:37:34 2018 +0100
@@ -17,7 +17,7 @@
 lemma has_derivative_mult_right:
   fixes c:: "'a :: real_normed_algebra"
   shows "((( * ) c) has_derivative (( * ) c)) F"
-by (rule has_derivative_mult_right [OF has_derivative_id])
+by (rule has_derivative_mult_right [OF has_derivative_ident])
 
 lemma has_derivative_of_real[derivative_intros, simp]:
   "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
@@ -382,7 +382,7 @@
 lemma holomorphic_on_Un [holomorphic_intros]:
   assumes "f holomorphic_on A" "f holomorphic_on B" "open A" "open B"
   shows   "f holomorphic_on (A \<union> B)"
-  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A] 
+  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A]
                              at_within_open[of _ B]  at_within_open[of _ "A \<union> B"] open_Un)
 
 lemma holomorphic_on_If_Un [holomorphic_intros]:
@@ -839,10 +839,10 @@
   show ?thesis
     unfolding has_field_derivative_def
   proof (rule has_derivative_sequence [OF cvs _ _ x])
-  show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
-    by (rule tf)
-  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: **)
+    show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
+      by (rule tf)
+  next show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
+      unfolding eventually_sequentially by (blast intro: **)
   qed (metis has_field_derivative_def df)
 qed
 
@@ -882,8 +882,8 @@
       by (metis df has_field_derivative_def mult_commute_abs)
   next show " ((\<lambda>n. f n x) sums l)"
     by (rule sf)
-  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: **)
+  next show "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
+      unfolding eventually_sequentially by (blast intro: **)
   qed
 qed
 
@@ -922,10 +922,8 @@
       and "x \<in> s"  "y \<in> s"
     shows "norm(f x - f y) \<le> B * norm(x - y)"
   apply (rule differentiable_bound [OF cvs])
-  apply (rule ballI, erule df [unfolded has_field_derivative_def])
-  apply (rule ballI, rule onorm_le, simp add: norm_mult mult_right_mono dn)
-  apply fact
-  apply fact
+  apply (erule df [unfolded has_field_derivative_def])
+  apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
   done
 
 subsection\<open>Inverse function theorem for complex derivatives\<close>
diff -r 88dd06301dd3 -r 0764ee22a4d1 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Sun May 20 18:37:34 2018 +0100
@@ -864,7 +864,7 @@
   proof -
     define h where [abs_def]: "h z = (z - \<xi>)^2 * f z" for z
     have h0: "(h has_field_derivative 0) (at \<xi>)"
-      apply (simp add: h_def Derivative.DERIV_within_iff)
+      apply (simp add: h_def has_field_derivative_iff)
       apply (rule Lim_transform_within [OF that, of 1])
       apply (auto simp: divide_simps power2_eq_square)
       done
@@ -879,7 +879,7 @@
         case False
         then have "f field_differentiable at z within S"
           using holomorphic_onD [OF holf, of z] \<open>z \<in> S\<close>
-          unfolding field_differentiable_def DERIV_within_iff
+          unfolding field_differentiable_def has_field_derivative_iff
           by (force intro: exI [where x="dist \<xi> z"] elim: Lim_transform_within_set [unfolded eventually_at])
         then show ?thesis
           by (simp add: h_def power2_eq_square derivative_intros)
@@ -1719,7 +1719,7 @@
   have "cnj \<circ> f \<circ> cnj field_differentiable at x within S \<inter> {z. Im z < 0}"
         if "x \<in> S" "Im x < 0" "f field_differentiable at (cnj x) within S \<inter> {z. 0 < Im z}" for x
     using that
-    apply (simp add: field_differentiable_def Derivative.DERIV_within_iff Lim_within dist_norm, clarify)
+    apply (simp add: field_differentiable_def has_field_derivative_iff Lim_within dist_norm, clarify)
     apply (rule_tac x="cnj f'" in exI)
     apply (elim all_forward ex_forward conj_forward imp_forward asm_rl, clarify)
     apply (drule_tac x="cnj xa" in bspec)
diff -r 88dd06301dd3 -r 0764ee22a4d1 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Sun May 20 18:37:34 2018 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Analysis/Derivative.thy
     Author:     John Harrison
-    Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light)
+    Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light); tidied by LCP
 *)
 
 section \<open>Multivariate calculus in Euclidean space\<close>
@@ -15,18 +15,6 @@
 
 subsection \<open>Derivatives\<close>
 
-subsubsection \<open>Combining theorems\<close>
-
-lemmas has_derivative_id = has_derivative_ident
-lemmas has_derivative_neg = has_derivative_minus
-lemmas has_derivative_sub = has_derivative_diff
-lemmas scaleR_right_has_derivative = has_derivative_scaleR_right
-lemmas scaleR_left_has_derivative = has_derivative_scaleR_left
-lemmas inner_right_has_derivative = has_derivative_inner_right
-lemmas inner_left_has_derivative = has_derivative_inner_left
-lemmas mult_right_has_derivative = has_derivative_mult_right
-lemmas mult_left_has_derivative = has_derivative_mult_left
-
 lemma has_derivative_add_const:
   "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
   by (intro derivative_eq_intros) auto
@@ -34,20 +22,6 @@
 
 subsection \<open>Derivative with composed bilinear function\<close>
 
-lemma has_derivative_bilinear_within:
-  assumes "(f has_derivative f') (at x within s)"
-    and "(g has_derivative g') (at x within s)"
-    and "bounded_bilinear h"
-  shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
-  using bounded_bilinear.FDERIV[OF assms(3,1,2)] .
-
-lemma has_derivative_bilinear_at:
-  assumes "(f has_derivative f') (at x)"
-    and "(g has_derivative g') (at x)"
-    and "bounded_bilinear h"
-  shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
-  using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
-
 text \<open>More explicit epsilon-delta forms.\<close>
 
 lemma has_derivative_within':
@@ -56,15 +30,14 @@
     (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
       norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
   unfolding has_derivative_within Lim_within dist_norm
-  unfolding diff_0_right
   by (simp add: diff_diff_eq)
 
 lemma has_derivative_at':
-  "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
-    (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
-      norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
-  using has_derivative_within' [of f f' x UNIV]
-  by simp
+  "(f has_derivative f') (at x) 
+   \<longleftrightarrow> bounded_linear f' \<and>
+       (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
+        norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
+  using has_derivative_within' [of f f' x UNIV] by simp
 
 lemma has_derivative_at_withinI:
   "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
@@ -80,7 +53,7 @@
   fixes f :: "real \<Rightarrow> real"
     and y :: "real"
   shows "(f has_derivative (( * ) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
-    ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
+         ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
 proof -
   have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
     ((\<lambda>t. (f t - f x) / (t - x) - y) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I))"
@@ -95,8 +68,6 @@
 
 subsubsection \<open>Caratheodory characterization\<close>
 
-lemmas DERIV_within_iff = has_field_derivative_iff
-
 lemma DERIV_caratheodory_within:
   "(f has_field_derivative l) (at x within S) \<longleftrightarrow>
    (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within S) g \<and> g x = l)"
@@ -108,7 +79,7 @@
     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
     show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
     show "continuous (at x within S) ?g" using \<open>?lhs\<close>
-      by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
+      by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
     show "?g x = l" by simp
   qed
 next
@@ -116,7 +87,7 @@
   then obtain g where
     "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within S) g" and "g x = l" by blast
   thus ?lhs
-    by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
+    by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
 qed
 
 subsection \<open>Differentiability\<close>
@@ -173,7 +144,7 @@
 lemma differentiable_on_mult [simp, derivative_intros]:
   fixes f :: "'M::real_normed_vector \<Rightarrow> 'a::real_normed_algebra"
   shows "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) differentiable_on S"
-  apply (simp add: differentiable_on_def differentiable_def)
+  unfolding differentiable_on_def differentiable_def
   using differentiable_def differentiable_mult by blast
 
 lemma differentiable_on_compose:
@@ -211,9 +182,9 @@
   by (blast intro: differentiable_scaleR)
 
 lemma has_derivative_sqnorm_at [derivative_intros, simp]:
-   "((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)"
-using has_derivative_bilinear_at [of id id a id id "(\<bullet>)"]
-by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)
+  "((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)"
+  using bounded_bilinear.FDERIV  [of "(\<bullet>)" id id a _ id id]
+  by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)
 
 lemma differentiable_sqnorm_at [derivative_intros, simp]:
   fixes a :: "'a :: {real_normed_vector,real_inner}"
@@ -378,29 +349,24 @@
 
 lemma frechet_derivative_unique_within:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "(f has_derivative f') (at x within S)"
-    and "(f has_derivative f'') (at x within S)"
-    and "\<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"
+  assumes 1: "(f has_derivative f') (at x within S)"
+    and 2: "(f has_derivative f'') (at x within S)"
+    and S: "\<And>i e. \<lbrakk>i\<in>Basis; e>0\<rbrakk> \<Longrightarrow> \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> S"
   shows "f' = f''"
 proof -
   note as = assms(1,2)[unfolded has_derivative_def]
   then interpret f': bounded_linear f' by auto
   from as interpret f'': bounded_linear f'' by auto
   have "x islimpt S" unfolding islimpt_approachable
-  proof (rule, rule)
+  proof (intro allI impI)
     fix e :: real
     assume "e > 0"
     obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> S"
       using assms(3) SOME_Basis \<open>e>0\<close> by blast
     then show "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
-      apply (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI)
-      unfolding dist_norm
-      apply (auto simp: SOME_Basis nonzero_Basis)
-      done
-  qed
+      by (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI) (auto simp: dist_norm SOME_Basis nonzero_Basis)  qed
   then have *: "netlimit (at x within S) = x"
-    apply (auto intro!: netlimit_within)
-    by (metis trivial_limit_within)
+    by (simp add: Lim_ident_at trivial_limit_within)
   show ?thesis
   proof (rule linear_eq_stdbasis)
     show "linear f'" "linear f''"
@@ -450,81 +416,65 @@
 
 lemma frechet_derivative_unique_within_closed_interval:
   fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
-    and "x \<in> cbox a b"
+  assumes ab: "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
+    and x: "x \<in> cbox a b"
     and "(f has_derivative f' ) (at x within cbox a b)"
     and "(f has_derivative f'') (at x within cbox a b)"
   shows "f' = f''"
-  apply(rule frechet_derivative_unique_within)
-  apply(rule assms(3,4))+
-proof (rule, rule, rule)
+proof (rule frechet_derivative_unique_within)
   fix e :: real
   fix i :: 'a
   assume "e > 0" and i: "i \<in> Basis"
   then show "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> cbox a b"
   proof (cases "x\<bullet>i = a\<bullet>i")
     case True
-    then show ?thesis
-      apply (rule_tac x="(min (b\<bullet>i - a\<bullet>i)  e) / 2" in exI)
-      using assms(1)[THEN bspec[where x=i]] and \<open>e>0\<close> and assms(2)
-      unfolding mem_box
-      using i
-      apply (auto simp add: field_simps inner_simps inner_Basis)
-      done
+    with ab[of i] \<open>e>0\<close> x i show ?thesis
+      by (rule_tac x="(min (b\<bullet>i - a\<bullet>i) e) / 2" in exI)
+         (auto simp add: mem_box field_simps inner_simps inner_Basis)
   next
-    note * = assms(2)[unfolded mem_box, THEN bspec, OF i]
     case False
     moreover have "a \<bullet> i < x \<bullet> i"
-      using False * by auto
+      using False i mem_box(2) x by force
     moreover {
       have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> a\<bullet>i *2 + x\<bullet>i - a\<bullet>i"
         by auto
       also have "\<dots> = a\<bullet>i + x\<bullet>i"
         by auto
       also have "\<dots> \<le> 2 * (x\<bullet>i)"
-        using * by auto
+        using \<open>a \<bullet> i < x \<bullet> i\<close> by auto
       finally have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> x \<bullet> i * 2"
         by auto
     }
     moreover have "min (x \<bullet> i - a \<bullet> i) e \<ge> 0"
-      using * and \<open>e>0\<close> by auto
+      by (simp add: \<open>0 < e\<close> \<open>a \<bullet> i < x \<bullet> i\<close> less_eq_real_def)
     then have "x \<bullet> i * 2 \<le> b \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e"
-      using * by auto
+      using i mem_box(2) x by force
     ultimately show ?thesis
-      apply (rule_tac x="- (min (x\<bullet>i - a\<bullet>i) e) / 2" in exI)
-      using assms(1)[THEN bspec, OF i] and \<open>e>0\<close> and assms(2)
-      unfolding mem_box
-      using i
-      apply (auto simp add: field_simps inner_simps inner_Basis)
-      done
+    using ab[of i] \<open>e>0\<close> x i 
+      by (rule_tac x="- (min (x\<bullet>i - a\<bullet>i) e) / 2" in exI)
+         (auto simp add: mem_box field_simps inner_simps inner_Basis)
   qed
-qed
+qed (use assms in auto)
 
 lemma frechet_derivative_unique_within_open_interval:
   fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "x \<in> box a b"
-    and "(f has_derivative f' ) (at x within box a b)"
-    and "(f has_derivative f'') (at x within box a b)"
+  assumes x: "x \<in> box a b"
+    and f: "(f has_derivative f' ) (at x within box a b)" "(f has_derivative f'') (at x within box a b)"
   shows "f' = f''"
 proof -
-  from assms(1) have *: "at x within box a b = at x"
-    by (metis at_within_interior interior_open open_box)
-  from assms(2,3) [unfolded *] show "f' = f''"
-    by (rule has_derivative_unique)
+  have "at x within box a b = at x"
+    by (metis x at_within_interior interior_open open_box)
+  with f show "f' = f''"
+    by (simp add: has_derivative_unique)
 qed
 
 lemma frechet_derivative_at:
   "(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
-  apply (rule has_derivative_unique[of f])
-  apply assumption
-  unfolding frechet_derivative_works[symmetric]
-  using differentiable_def
-  apply auto
-  done
+  using differentiable_def frechet_derivative_works has_derivative_unique by blast
 
 lemma frechet_derivative_within_cbox:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
+  assumes "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
     and "x \<in> cbox a b"
     and "(f has_derivative f') (at x within cbox a b)"
   shows "frechet_derivative f (at x within cbox a b) = f'"
@@ -547,7 +497,7 @@
     using deriv by (rule has_derivative_bounded_linear)
   show "f' h = 0"
   proof (cases "h = 0")
-    assume "h \<noteq> 0"
+    case False
     from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
       unfolding eventually_at by (force simp: dist_commute)
     have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
@@ -561,7 +511,7 @@
       using \<open>h \<noteq> 0\<close> by (auto simp add: d2 dist_norm pos_less_divide_eq)
     ultimately show "f' h = 0"
       by (rule DERIV_local_min)
-  qed (simp add: f'.zero)
+  qed simp
 qed
 
 lemma has_derivative_local_max:
@@ -574,21 +524,21 @@
 
 lemma differential_zero_maxmin:
   fixes f::"'a::real_normed_vector \<Rightarrow> real"
-  assumes "x \<in> s"
-    and "open s"
+  assumes "x \<in> S"
+    and "open S"
     and deriv: "(f has_derivative f') (at x)"
-    and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
+    and mono: "(\<forall>y\<in>S. f y \<le> f x) \<or> (\<forall>y\<in>S. f x \<le> f y)"
   shows "f' = (\<lambda>v. 0)"
   using mono
 proof
-  assume "\<forall>y\<in>s. f y \<le> f x"
-  with \<open>x \<in> s\<close> and \<open>open s\<close> have "eventually (\<lambda>y. f y \<le> f x) (at x)"
+  assume "\<forall>y\<in>S. f y \<le> f x"
+  with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f y \<le> f x) (at x)"
     unfolding eventually_at_topological by auto
   with deriv show ?thesis
     by (rule has_derivative_local_max)
 next
-  assume "\<forall>y\<in>s. f x \<le> f y"
-  with \<open>x \<in> s\<close> and \<open>open s\<close> have "eventually (\<lambda>y. f x \<le> f y) (at x)"
+  assume "\<forall>y\<in>S. f x \<le> f y"
+  with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f x \<le> f y) (at x)"
     unfolding eventually_at_topological by auto
   with deriv show ?thesis
     by (rule has_derivative_local_min)
@@ -613,28 +563,24 @@
     unfolding fun_eq_iff by simp
 qed
 
-lemma rolle:
+theorem Rolle:
   fixes f :: "real \<Rightarrow> real"
   assumes "a < b"
-    and "f a = f b"
-    and "continuous_on {a .. b} f"
-    and "\<forall>x\<in>{a <..< b}. (f has_derivative f' x) (at x)"
+    and fab: "f a = f b"
+    and contf: "continuous_on {a..b} f"
+    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   shows "\<exists>x\<in>{a <..< b}. f' x = (\<lambda>v. 0)"
 proof -
   have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)"
   proof -
-    have "(a + b) / 2 \<in> {a .. b}"
+    have "(a + b) / 2 \<in> {a..b}"
       using assms(1) by auto
-    then have *: "{a .. b} \<noteq> {}"
+    then have *: "{a..b} \<noteq> {}"
       by auto
-    obtain d where d:
-        "d \<in>cbox a b"
-        "\<forall>y\<in>cbox a b. f y \<le> f d"
-      using continuous_attains_sup[OF compact_Icc * assms(3)] by auto
-    obtain c where c:
-        "c \<in> cbox a b"
-        "\<forall>y\<in>cbox a b. f c \<le> f y"
-      using continuous_attains_inf[OF compact_Icc * assms(3)] by auto
+    obtain d where d: "d \<in>cbox a b" "\<forall>y\<in>cbox a b. f y \<le> f d"
+      using continuous_attains_sup[OF compact_Icc * contf] by auto
+    obtain c where c: "c \<in> cbox a b" "\<forall>y\<in>cbox a b. f c \<le> f y"
+      using continuous_attains_inf[OF compact_Icc * contf] by auto
     show ?thesis
     proof (cases "d \<in> box a b \<or> c \<in> box a b")
       case True
@@ -644,16 +590,11 @@
       define e where "e = (a + b) /2"
       case False
       then have "f d = f c"
-        using d c assms(2) by auto
-      then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
-        using c d
+        using d c fab by auto
+      with c d have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
         by force
       then show ?thesis
-        apply (rule_tac x=e in bexI)
-        unfolding e_def
-        using assms(1)
-        apply auto
-        done
+        by (rule_tac x=e in bexI) (auto simp: e_def \<open>a < b\<close>)
     qed
   qed
   then obtain x where x: "x \<in> {a <..< b}" "(\<forall>y\<in>{a <..< b}. f x \<le> f y) \<or> (\<forall>y\<in>{a <..< b}. f y \<le> f x)"
@@ -673,18 +614,18 @@
 lemma mvt:
   fixes f :: "real \<Rightarrow> real"
   assumes "a < b"
-    and "continuous_on {a..b} f"
-  assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)"
+    and contf: "continuous_on {a..b} f"
+    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)"
 proof -
   have "\<exists>x\<in>{a <..< b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
-  proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
+  proof (intro Rolle[OF \<open>a < b\<close>, of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
     fix x
-    assume x: "x \<in> {a <..< b}"
+    assume x: "a < x" "x < b"
     show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
         (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
-      by (intro derivative_intros assms(3)[rule_format,OF x])
-  qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps)
+      by (intro derivative_intros derf[OF x])
+  qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>)
   then obtain x where
     "x \<in> {a <..< b}"
     "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
@@ -697,50 +638,33 @@
 lemma mvt_simple:
   fixes f :: "real \<Rightarrow> real"
   assumes "a < b"
-    and "\<forall>x\<in>{a..b}. (f has_derivative f' x) (at x within {a..b})"
+    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
 proof (rule mvt)
   have "f differentiable_on {a..b}"
-    using assms(2) unfolding differentiable_on_def differentiable_def by fast
+    by (meson atLeastAtMost_iff derf differentiable_at_imp_differentiable_on differentiable_def)
   then show "continuous_on {a..b} f"
     by (rule differentiable_imp_continuous_on)
-  show "\<forall>x\<in>{a<..<b}. (f has_derivative f' x) (at x)"
-  proof
-    fix x
-    assume x: "x \<in> {a <..< b}"
-    show "(f has_derivative f' x) (at x)"
-      unfolding at_within_open[OF x open_greaterThanLessThan,symmetric]
-      apply (rule has_derivative_within_subset)
-      apply (rule assms(2)[rule_format])
-      using x
-      apply auto
-      done
-  qed
-qed (rule assms(1))
+  show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x
+    by (metis derf not_less order.asym that)
+qed (rule assms)
 
 lemma mvt_very_simple:
   fixes f :: "real \<Rightarrow> real"
   assumes "a \<le> b"
-    and "\<forall>x\<in>{a .. b}. (f has_derivative f' x) (at x within {a .. b})"
-  shows "\<exists>x\<in>{a .. b}. f b - f a = f' x (b - a)"
+    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
+  shows "\<exists>x\<in>{a..b}. f b - f a = f' x (b - a)"
 proof (cases "a = b")
   interpret bounded_linear "f' b"
     using assms(2) assms(1) by auto
   case True
   then show ?thesis
-    apply (rule_tac x=a in bexI)
-    using assms(2)[THEN bspec[where x=a]]
-    unfolding has_derivative_def
-    unfolding True
-    using zero
-    apply auto
-    done
+    by force
 next
   case False
   then show ?thesis
-    using mvt_simple[OF _ assms(2)]
-    using assms(1)
-    by auto
+    using mvt_simple[OF _ derf]
+    by (metis \<open>a \<le> b\<close> atLeastAtMost_iff dual_order.order_iff_strict greaterThanLessThan_iff)
 qed
 
 text \<open>A nice generalization (see Havin's proof of 5.19 from Rudin's book).\<close>
@@ -748,19 +672,16 @@
 lemma mvt_general:
   fixes f :: "real \<Rightarrow> 'a::real_inner"
   assumes "a < b"
-    and "continuous_on {a .. b} f"
-    and "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
+    and contf: "continuous_on {a..b} f"
+    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   shows "\<exists>x\<in>{a<..<b}. norm (f b - f a) \<le> norm (f' x (b - a))"
 proof -
   have "\<exists>x\<in>{a<..<b}. (f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)"
-    apply (rule mvt)
-    apply (rule assms(1))
-    apply (intro continuous_intros assms(2))
-    using assms(3)
-    apply (fast intro: has_derivative_inner_right)
+    apply (rule mvt [OF \<open>a < b\<close>])
+    apply (intro continuous_intros contf)
+    using derf apply (blast intro: has_derivative_inner_right)
     done
-  then obtain x where x:
-    "x \<in> {a<..<b}"
+  then obtain x where x: "x \<in> {a<..<b}"
     "(f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)" ..
   show ?thesis
   proof (cases "f a = f b")
@@ -779,21 +700,18 @@
   next
     case True
     then show ?thesis
-      using assms(1)
-      apply (rule_tac x="(a + b) /2" in bexI)
-      apply auto
-      done
+      using \<open>a < b\<close> by (rule_tac x="(a + b) /2" in bexI) auto
   qed
 qed
 
 
 subsection \<open>More general bound theorems\<close>
 
-lemma differentiable_bound_general:
+proposition differentiable_bound_general:
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   assumes "a < b"
-    and f_cont: "continuous_on {a .. b} f"
-    and phi_cont: "continuous_on {a .. b} \<phi>"
+    and f_cont: "continuous_on {a..b} f"
+    and phi_cont: "continuous_on {a..b} \<phi>"
     and f': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
     and phi': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<phi> has_vector_derivative \<phi>' x) (at x)"
     and bnd: "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> norm (f' x) \<le> \<phi>' x"
@@ -813,7 +731,7 @@
     with \<open>e > 0\<close> have "e2 > 0" by simp
     let ?le = "\<lambda>x1. norm (f x1 - f a) \<le> \<phi> x1 - \<phi> a + e * (x1 - a) + e"
     define A where "A = {x2. a \<le> x2 \<and> x2 \<le> b \<and> (\<forall>x1\<in>{a ..< x2}. ?le x1)}"
-    have A_subset: "A \<subseteq> {a .. b}" by (auto simp: A_def)
+    have A_subset: "A \<subseteq> {a..b}" by (auto simp: A_def)
     {
       fix x2
       assume a: "a \<le> x2" "x2 \<le> b" and le: "\<forall>x1\<in>{a..<x2}. ?le x1"
@@ -828,7 +746,7 @@
           "((\<lambda>x1. norm (f x1 - f a)) \<longlongrightarrow> norm (f x2 - f a)) (at x2 within {a <..<x2})"
           using a
           by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto
-            intro: tendsto_within_subset[where S="{a .. b}"])
+            intro: tendsto_within_subset[where S="{a..b}"])
         moreover
         have "eventually (\<lambda>x. x > a) (at x2 within {a <..<x2})"
           by (auto simp: eventually_at_filter)
@@ -860,85 +778,11 @@
       using y_all_le \<open>a \<le> y\<close> \<open>y \<le> b\<close>
       by (auto simp: A_def)
     hence "A = {a .. y}"
-      using A_subset
-      by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
+      using A_subset by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
     from le_cont[OF \<open>a \<le> y\<close> \<open>y \<le> b\<close> y_all_le] have le_y: "?le y" .
-    {
-      assume "a \<noteq> y" with \<open>a \<le> y\<close> have "a < y" by simp
-      have "y = b"
-      proof (rule ccontr)
-        assume "y \<noteq> b"
-        hence "y < b" using \<open>y \<le> b\<close> by simp
-        let ?F = "at y within {y..<b}"
-        from f' phi'
-        have "(f has_vector_derivative f' y) ?F"
-          and "(\<phi> has_vector_derivative \<phi>' y) ?F"
-          using \<open>a < y\<close> \<open>y < b\<close>
-          by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def
-            intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"])
-        hence "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>"
-            "\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>"
-          using \<open>e2 > 0\<close>
-          by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
-        moreover
-        have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b"
-          by (auto simp: eventually_at_filter)
-        ultimately
-        have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
-          (is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
-        proof eventually_elim
-          case (elim x1)
-          from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
-          have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
-            by (simp add: ac_simps)
-          also have "norm (f' y) \<le> \<phi>' y" using bnd \<open>a < y\<close> \<open>y < b\<close> by simp
-          also
-          from elim have "\<phi>' y * \<bar>x1 - y\<bar> \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar>"
-            by (simp add: ac_simps)
-          finally
-          have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
-            by (auto simp: mult_right_mono)
-          thus ?case by (simp add: e2_def)
-        qed
-        moreover have "?le' y" by simp
-        ultimately obtain S
-        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x"
-          unfolding eventually_at_topological
-          by metis
-        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
-          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
-        define d' where "d' = min ((y + b)/2) (y + (d/2))"
-        have "d' \<in> A"
-          unfolding A_def
-        proof safe
-          show "a \<le> d'" using \<open>a < y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def)
-          show "d' \<le> b" using \<open>y < b\<close> by (simp add: d'_def min_def)
-          fix x1
-          assume x1: "x1 \<in> {a..<d'}"
-          {
-            assume "x1 < y"
-            hence "?le x1"
-              using \<open>x1 \<in> {a..<d'}\<close> y_all_le by auto
-          } moreover {
-            assume "x1 \<ge> y"
-            hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1
-              by (auto simp: d'_def dist_real_def intro!: d)
-            have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
-              by (rule order_trans[OF _ norm_triangle_ineq]) simp
-            also note S(3)[OF x1']
-            also note le_y
-            finally have "?le x1"
-              using \<open>x1 \<ge> y\<close> by (auto simp: algebra_simps)
-          } ultimately show "?le x1" by arith
-        qed
-        hence "d' \<le> y"
-          unfolding y_def
-          by (rule cSup_upper) simp
-        thus False using \<open>d > 0\<close> \<open>y < b\<close>
-          by (simp add: d'_def min_def split: if_split_asm)
-      qed
-    } moreover {
-      assume "a = y"
+    have "y = b"
+    proof (cases "a = y")
+      case True
       with \<open>a < b\<close> have "y < b" by simp
       with \<open>a = y\<close> f_cont phi_cont \<open>e2 > 0\<close>
       have 1: "\<forall>\<^sub>F x in at y within {y..b}. dist (f x) (f y) < e2"
@@ -966,8 +810,7 @@
         finally show "?le x1" .
       qed
       from this[unfolded eventually_at_topological] \<open>?le y\<close>
-      obtain S
-      where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
+      obtain S where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
         by metis
       from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
         by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
@@ -987,81 +830,140 @@
       hence "d' \<le> y"
         unfolding y_def
         by (rule cSup_upper) simp
-      hence "y = b" using \<open>d > 0\<close> \<open>y < b\<close>
+      then show "y = b" using \<open>d > 0\<close> \<open>y < b\<close>
         by (simp add: d'_def)
-    } ultimately have "y = b"
-      by auto
+    next
+      case False
+      with \<open>a \<le> y\<close> have "a < y" by simp
+      show "y = b"
+      proof (rule ccontr)
+        assume "y \<noteq> b"
+        hence "y < b" using \<open>y \<le> b\<close> by simp
+        let ?F = "at y within {y..<b}"
+        from f' phi'
+        have "(f has_vector_derivative f' y) ?F"
+          and "(\<phi> has_vector_derivative \<phi>' y) ?F"
+          using \<open>a < y\<close> \<open>y < b\<close>
+          by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def
+            intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"])
+        hence "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>"
+            "\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>"
+          using \<open>e2 > 0\<close>
+          by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
+        moreover
+        have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b"
+          by (auto simp: eventually_at_filter)
+        ultimately
+        have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
+          (is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
+        proof eventually_elim
+          case (elim x1)
+          from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
+          have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
+            by (simp add: ac_simps)
+          also have "norm (f' y) \<le> \<phi>' y" using bnd \<open>a < y\<close> \<open>y < b\<close> by simp
+          also have "\<phi>' y * \<bar>x1 - y\<bar> \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar>"
+            using elim by (simp add: ac_simps)
+          finally
+          have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
+            by (auto simp: mult_right_mono)
+          thus ?case by (simp add: e2_def)
+        qed
+        moreover have "?le' y" by simp
+        ultimately obtain S
+        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x"
+          unfolding eventually_at_topological
+          by metis
+        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
+          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
+        define d' where "d' = min ((y + b)/2) (y + (d/2))"
+        have "d' \<in> A"
+          unfolding A_def
+        proof safe
+          show "a \<le> d'" using \<open>a < y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def)
+          show "d' \<le> b" using \<open>y < b\<close> by (simp add: d'_def min_def)
+          fix x1
+          assume x1: "x1 \<in> {a..<d'}"
+          show "?le x1"
+          proof (cases "x1 < y")
+            case True
+            then show ?thesis
+              using \<open>y \<in> A\<close> local.leI x1 by auto
+          next
+            case False
+            hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1
+              by (auto simp: d'_def dist_real_def intro!: d)
+            have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
+              by (rule order_trans[OF _ norm_triangle_ineq]) simp
+            also note S(3)[OF x1']
+            also note le_y
+            finally show "?le x1"
+              using False by (auto simp: algebra_simps)
+          qed
+        qed
+        hence "d' \<le> y"
+          unfolding y_def by (rule cSup_upper) simp
+        thus False using \<open>d > 0\<close> \<open>y < b\<close>
+          by (simp add: d'_def min_def split: if_split_asm)
+      qed
+    qed
     with le_y have "norm (f b - f a) \<le> \<phi> b - \<phi> a + e * (b - a + 1)"
       by (simp add: algebra_simps)
   } note * = this
-  {
+  show ?thesis
+  proof (rule field_le_epsilon)
     fix e::real assume "e > 0"
-    hence "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
+    then show "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
       using *[of "e / (b - a + 1)"] \<open>a < b\<close> by simp
-  } thus ?thesis
-    by (rule field_le_epsilon)
+  qed
 qed
 
 lemma differentiable_bound:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  assumes "convex s"
-    and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
-    and "\<forall>x\<in>s. onorm (f' x) \<le> B"
-    and x: "x \<in> s"
-    and y: "y \<in> s"
+  assumes "convex S"
+    and derf: "\<And>x. x\<in>S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
+    and B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x) \<le> B"
+    and x: "x \<in> S"
+    and y: "y \<in> S"
   shows "norm (f x - f y) \<le> B * norm (x - y)"
 proof -
   let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
   let ?\<phi> = "\<lambda>h. h * B * norm (x - y)"
-  have *: "\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
-    using assms(1)[unfolded convex_alt,rule_format,OF x y]
-    unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
-    by (auto simp add: algebra_simps)
-  have 0: "continuous_on (?p ` {0..1}) f"
-    using *
+  have *: "x + u *\<^sub>R (y - x) \<in> S" if "u \<in> {0..1}" for u
+  proof -
+    have "u *\<^sub>R y = u *\<^sub>R (y - x) + u *\<^sub>R x"
+      by (simp add: scale_right_diff_distrib)
+    then show "x + u *\<^sub>R (y - x) \<in> S"
+      using that \<open>convex S\<close> unfolding convex_alt by (metis (no_types) atLeastAtMost_iff linordered_field_class.sign_simps(2) pth_c(3) scaleR_collapse x y)
+  qed
+  have "\<And>z. z \<in> (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1} \<Longrightarrow>
+          (f has_derivative f' z) (at z within (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1})"
+    by (auto intro: * has_derivative_within_subset [OF derf])
+  then have "continuous_on (?p ` {0..1}) f"
     unfolding continuous_on_eq_continuous_within
-    apply -
-    apply rule
-    apply (rule differentiable_imp_continuous_within)
-    unfolding differentiable_def
-    apply (rule_tac x="f' xa" in exI)
-    apply (rule has_derivative_within_subset)
-    apply (rule assms(2)[rule_format])
-    apply auto
-    done
-  from * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
-    by (intro continuous_intros 0)+
+    by (meson has_derivative_continuous)
+  with * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
+    by (intro continuous_intros)+
   {
     fix u::real assume u: "u \<in>{0 <..< 1}"
     let ?u = "?p u"
     interpret linear "(f' ?u)"
-      using u by (auto intro!: has_derivative_linear assms(2)[rule_format] *)
+      using u by (auto intro!: has_derivative_linear derf *)
     have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
-      apply (rule diff_chain_within)
-      apply (rule derivative_intros)+
-      apply (rule has_derivative_within_subset)
-      apply (rule assms(2)[rule_format])
-      using u *
-      apply auto
-      done
+      by (intro derivative_intros has_derivative_within_subset [OF derf]) (use u * in auto)
     hence "((f \<circ> ?p) has_vector_derivative f' ?u (y - x)) (at u)"
       by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan]
         scaleR has_vector_derivative_def o_def)
   } note 2 = this
-  {
-    have "continuous_on {0..1} ?\<phi>"
-      by (rule continuous_intros)+
-  } note 3 = this
-  {
-    fix u::real assume u: "u \<in>{0 <..< 1}"
-    have "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)"
-      by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
-  } note 4 = this
+  have 3: "continuous_on {0..1} ?\<phi>"
+    by (rule continuous_intros)+
+  have 4: "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)" for u
+    by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
   {
     fix u::real assume u: "u \<in>{0 <..< 1}"
     let ?u = "?p u"
     interpret bounded_linear "(f' ?u)"
-      using u by (auto intro!: has_derivative_bounded_linear assms(2)[rule_format] *)
+      using u by (auto intro!: has_derivative_bounded_linear derf *)
     have "norm (f' ?u (y - x)) \<le> onorm (f' ?u) * norm (y - x)"
       by (rule onorm) (rule bounded_linear)
     also have "onorm (f' ?u) \<le> B"
@@ -1083,7 +985,7 @@
   fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R a \<in> G"
   assumes f': "\<And>x. x \<in> G \<Longrightarrow> (f has_derivative f' x) (at x within G)"
-  assumes B: "\<forall>x\<in>{0..1}. onorm (f' (x0 + x *\<^sub>R a)) \<le> B"
+  assumes B: "\<And>x. x \<in> {0..1} \<Longrightarrow> onorm (f' (x0 + x *\<^sub>R a)) \<le> B"
   shows "norm (f (x0 + a) - f x0) \<le> norm a * B"
 proof -
   let ?G = "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}"
@@ -1095,14 +997,14 @@
   ultimately show ?thesis
     using has_derivative_subset[OF f' \<open>?G \<subseteq> G\<close>] B
       differentiable_bound[of "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}" f f' B "x0 + a" x0]
-    by (auto simp: ac_simps)
+    by (force simp: ac_simps)
 qed
 
 lemma differentiable_bound_linearization:
   fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
+  assumes S: "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
   assumes f'[derivative_intros]: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
-  assumes B: "\<forall>x\<in>S. onorm (f' x - f' x0) \<le> B"
+  assumes B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x - f' x0) \<le> B"
   assumes "x0 \<in> S"
   shows "norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B"
 proof -
@@ -1111,9 +1013,9 @@
     unfolding g_def using assms
     by (auto intro!: derivative_eq_intros
       bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f'])
-  from B have B: "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B"
-     using assms by (auto simp: fun_diff_def)
-  from differentiable_bound_segment[OF assms(1) g B] \<open>x0 \<in> S\<close>
+  from B have "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B"
+    using assms by (auto simp: fun_diff_def)
+  with differentiable_bound_segment[OF S g] \<open>x0 \<in> S\<close>
   show ?thesis
     by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
 qed
@@ -1122,7 +1024,7 @@
   fixes f::"real \<Rightarrow> 'b::real_normed_vector"
   assumes f': "\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)"
   assumes "closed_segment a b \<subseteq> S"
-  assumes B: "\<forall>x\<in>S. norm (f' x - f' x0) \<le> B"
+  assumes B: "\<And>x. x \<in> S \<Longrightarrow> norm (f' x - f' x0) \<le> B"
   assumes "x0 \<in> S"
   shows "norm (f b - f a - (b - a) *\<^sub>R f' x0) \<le> norm (b - a) * B"
   using assms
@@ -1346,20 +1248,14 @@
     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 gf: "\<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"
   shows "(g has_derivative g') (at (f x))"
 proof -
-  {
-    fix y
-    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>] ..
-  } note * = this
+  have *: "\<And>y. y \<in> interior (f ` S) \<Longrightarrow> f (g y) = y"
+    by (metis gf image_iff interior_subset subsetCE)
   show ?thesis
     apply (rule has_derivative_inverse_basic_x[OF assms(6-8), where T = "interior (f ` S)"])
     apply (rule continuous_on_interior[OF _ fx])
@@ -1386,8 +1282,8 @@
   show ?thesis
     unfolding *
     apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
-    apply (rule continuous_intros assms)+
-    using assms(4-6)
+    apply (intro continuous_intros)
+    using assms
     apply auto
     done
 qed
@@ -1411,34 +1307,28 @@
 lemma sussmann_open_mapping:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
   assumes "open S"
-    and "continuous_on S f"
+    and contf: "continuous_on S f"
     and "x \<in> S"
-    and "(f has_derivative f') (at x)"
+    and derf: "(f has_derivative f') (at x)"
     and "bounded_linear g'" "f' \<circ> g' = id"
     and "T \<subseteq> S"
-    and "x \<in> interior T"
+    and x: "x \<in> interior T"
   shows "f x \<in> interior (f ` T)"
 proof -
   interpret f': bounded_linear f'
-    using assms
-    unfolding has_derivative_def
-    by auto
+    using assms unfolding has_derivative_def by auto
   interpret g': bounded_linear g'
-    using assms
-    by auto
+    using assms by auto
   obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
     using bounded_linear.pos_bounded[OF assms(5)] by blast
   hence *: "1 / (2 * B) > 0" by auto
   obtain e0 where e0:
       "0 < e0"
       "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
-    using assms(4)
-    unfolding has_derivative_at_alt
+    using derf unfolding has_derivative_at_alt
     using * by blast
   obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
-    using assms(8)
-    unfolding mem_interior_cball
-    by blast
+    using mem_interior_cball x 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
@@ -1449,83 +1339,59 @@
       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"
-        unfolding g'.diff[symmetric]
-        using B
-        by auto
+        by (metis B(2) g'.diff)
       also have "\<dots> \<le> e * B"
-        using as(1)[unfolded mem_cball dist_norm]
-        using B
-        by auto
+        by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1))
       also have "\<dots> \<le> e1"
-        using e
-        unfolding less_divide_eq
-        using B
-        by auto
+        using B(1) e(3) pos_less_divide_eq by fastforce
       finally have "z \<in> cball x e1"
-        unfolding mem_cball
         by force
       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
+    proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f])
+      show "continuous_on ((\<lambda>y. x + (g' y - g' (f x))) ` cball (f x) e) f"
+        by (rule continuous_on_subset[OF contf]) (use z in blast)
+      show "continuous_on (cball (f x) e) (\<lambda>y. x + (g' y - g' (f x)))"
+        by (intro continuous_intros linear_continuous_on[OF \<open>bounded_linear g'\<close>])
+    qed
   next
     fix y z
-    assume as: "y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e"
+    assume y: "y \<in> cball (f x) (e / 2)" and z: "z \<in> cball (f x) e"
     have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
       using B by auto
     also have "\<dots> \<le> e * B"
-      apply (rule mult_right_mono)
-      using as(2)[unfolded mem_cball dist_norm] and B
-      unfolding norm_minus_commute
-       apply auto
-      done
+      by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1)
     also have "\<dots> < e0"
-      using e and B
-      unfolding less_divide_eq
-      by auto
+      using B(1) e(2) pos_less_divide_eq by blast
     finally have *: "norm (x + g' (z - f x) - x) < e0"
       by auto
     have **: "f x + f' (x + g' (z - f x) - x) = z"
       using assms(6)[unfolded o_def id_def,THEN cong]
       by auto
     have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
-        norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
+          norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
       using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
       by (auto simp add: algebra_simps)
     also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
       using e0(2)[rule_format, OF *]
       by (simp only: algebra_simps **) auto
     also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
-      using as(1)[unfolded mem_cball dist_norm]
-      by auto
+      using y by (auto simp: dist_norm)
     also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
-      using * and B
-      by (auto simp add: field_simps)
+      using * B by (auto simp add: field_simps)
     also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
       by auto
     also have "\<dots> \<le> e/2 + e/2"
-      apply (rule add_right_mono)
-      using as(2)[unfolded mem_cball dist_norm]
-      unfolding norm_minus_commute
-      apply auto
-      done
+      using B(1) \<open>norm (z - f x) * B \<le> e * B\<close> by auto
     finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
-      unfolding mem_cball dist_norm
-      by auto
+      by (auto simp: dist_norm)
   qed (use e that in auto) 
   show ?thesis
     unfolding mem_interior
-    apply (rule_tac x="e/2" in exI)
-    apply rule
-    apply (rule divide_pos_pos)
-    prefer 3
-  proof
+  proof (intro exI conjI subsetI)
     fix y
     assume "y \<in> ball (f x) (e / 2)"
     then have *: "y \<in> cball (f x) (e / 2)"
@@ -1536,23 +1402,14 @@
       using B
       by (auto simp add: field_simps)
     also have "\<dots> \<le> e * B"
-      apply (rule mult_right_mono)
-      using z(1)
-      unfolding mem_cball dist_norm norm_minus_commute
-      using B
-      apply auto
-      done
+      by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1))
     also have "\<dots> \<le> e1"
       using e B unfolding less_divide_eq by auto
     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
+      by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq)
     then show "y \<in> f ` T"
       using z by auto
-  qed (insert e, auto)
+  qed (use e in auto)
 qed
 
 text \<open>Hence the following eccentric variant of the inverse function theorem.
@@ -1562,30 +1419,25 @@
 
 lemma has_derivative_inverse_strong:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "open s"
-    and "x \<in> s"
-    and "continuous_on s f"
-    and "\<forall>x\<in>s. g (f x) = x"
-    and "(f has_derivative f') (at x)"
-    and "f' \<circ> g' = id"
+  assumes "open S"
+    and "x \<in> S"
+    and contf: "continuous_on S f"
+    and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+    and derf: "(f has_derivative f') (at x)"
+    and id: "f' \<circ> g' = id"
   shows "(g has_derivative g') (at (f x))"
 proof -
   have linf: "bounded_linear f'"
-    using assms(5) unfolding has_derivative_def by auto
+    using derf unfolding has_derivative_def by auto
   then have ling: "bounded_linear g'"
     unfolding linear_conv_bounded_linear[symmetric]
-    apply -
-    apply (rule right_inverse_linear)
-    using assms(6)
-    apply auto
-    done
+    using id right_inverse_linear by blast
   moreover have "g' \<circ> f' = id"
-    using assms(6) linf ling
+    using id linf ling
     unfolding linear_conv_bounded_linear[symmetric]
     using linear_inverse_left
     by auto
-  moreover have *:"\<forall>t\<subseteq>s. x \<in> interior t \<longrightarrow> f x \<in> interior (f ` t)"
-    apply clarify
+  moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
     apply (rule sussmann_open_mapping)
     apply (rule assms ling)+
     apply auto
@@ -1595,44 +1447,30 @@
   proof (rule, rule)
     fix e :: real
     assume "e > 0"
-    then have "f x \<in> interior (f ` (ball x e \<inter> s))"
-      using *[rule_format,of "ball x e \<inter> s"] \<open>x \<in> s\<close>
+    then have "f x \<in> interior (f ` (ball x e \<inter> S))"
+      using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
       by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
-    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> s)"
+    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
       unfolding mem_interior by blast
     show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
-      apply (rule_tac x=d in exI)
-      apply rule
-      apply (rule d(1))
-      apply rule
-      apply rule
-    proof -
+    proof (intro exI allI impI conjI)
       fix y
       assume "0 < dist y (f x) \<and> dist y (f x) < d"
-      then have "g y \<in> g ` f ` (ball x e \<inter> s)"
-        using d(2)[unfolded subset_eq,THEN bspec[where x=y]]
-        by (auto simp add: dist_commute)
-      then have "g y \<in> ball x e \<inter> s"
-        using assms(4) by auto
+      then have "g y \<in> g ` f ` (ball x e \<inter> S)"
+        by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
       then show "dist (g y) (g (f x)) < e"
-        using assms(4)[rule_format,OF \<open>x \<in> s\<close>]
-        by (auto simp add: dist_commute)
-    qed
+        using gf[OF \<open>x \<in> S\<close>]
+        by (simp add: assms(4) dist_commute image_iff)
+    qed (use d in auto)
   qed
-  moreover have "f x \<in> interior (f ` s)"
+  moreover have "f x \<in> interior (f ` S)"
     apply (rule sussmann_open_mapping)
     apply (rule assms ling)+
-    using interior_open[OF assms(1)] and \<open>x \<in> s\<close>
+    using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
     apply auto
     done
-  moreover have "f (g y) = y" if "y \<in> interior (f ` s)" for y
-  proof -
-    from that have "y \<in> f ` s"
-      using interior_subset by auto
-    then obtain z where "z \<in> s" "y = f z" unfolding image_iff ..
-    then show ?thesis
-      using assms(4) by auto
-  qed
+  moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
+    by (metis gf imageE interiorE set_mp that)
   ultimately show ?thesis using assms
     by (metis has_derivative_inverse_basic_x open_interior)
 qed
@@ -1641,10 +1479,10 @@
 
 lemma has_derivative_inverse_strong_x:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
-  assumes "open s"
-    and "g y \<in> s"
-    and "continuous_on s f"
-    and "\<forall>x\<in>s. g (f x) = x"
+  assumes "open S"
+    and "g y \<in> S"
+    and "continuous_on S f"
+    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
     and "(f has_derivative f') (at (g y))"
     and "f' \<circ> g' = id"
     and "f (g y) = y"
@@ -1657,21 +1495,18 @@
 
 lemma has_derivative_inverse_on:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "open s"
-    and "\<forall>x\<in>s. (f has_derivative f'(x)) (at x)"
-    and "\<forall>x\<in>s. g (f x) = x"
+  assumes "open S"
+    and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
+    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
     and "f' x \<circ> g' x = id"
-    and "x \<in> s"
+    and "x \<in> S"
   shows "(g has_derivative g'(x)) (at (f x))"
-  apply (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
-  apply (rule assms)+
-  unfolding continuous_on_eq_continuous_at[OF assms(1)]
-  apply rule
-  apply (rule differentiable_imp_continuous_within)
-  unfolding differentiable_def
-  using assms
-  apply auto
-  done
+proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
+  show "continuous_on S f"
+  unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
+  using derf has_derivative_continuous by blast
+qed (use assms in auto)
+
 
 text \<open>Invertible derivative continous at a point implies local
 injectivity. It's only for this we need continuity of the derivative,
@@ -1681,13 +1516,13 @@
 
 proposition has_derivative_locally_injective:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "a \<in> s"
-      and "open s"
+  assumes "a \<in> S"
+      and "open S"
       and bling: "bounded_linear g'"
       and "g' \<circ> f' a = id"
-      and derf: "\<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)"
+  obtains r where "r > 0" "ball a r \<subseteq> S" "inj_on f (ball a r)"
 proof -
   interpret bounded_linear g'
     using assms by auto
@@ -1704,21 +1539,17 @@
       "0 < d1"
       "\<And>x. dist a x < d1 \<Longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < k"
     using assms(6) * by blast
-  from \<open>open s\<close> obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s"
-    using \<open>a\<in>s\<close> ..
-  obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s"
-    using assms(2,1) ..
-  obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> s"
-    using assms(2)
-    unfolding open_contains_ball
-    using \<open>a\<in>s\<close> by blast
+  from \<open>open S\<close> obtain d2 where "d2 > 0" "ball a d2 \<subseteq> S"
+    using \<open>a\<in>S\<close> ..
+  obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> S"
+    using \<open>0 < d2\<close> \<open>ball a d2 \<subseteq> S\<close> by blast
   obtain d where d: "0 < d" "d < d1" "d < d2"
     using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
   show ?thesis
   proof
     show "0 < d" by (fact d)
-    show "ball a d \<subseteq> s"
-      using \<open>d < d2\<close> \<open>ball a d2 \<subseteq> s\<close> by auto
+    show "ball a d \<subseteq> S"
+      using \<open>d < d2\<close> \<open>ball a d2 \<subseteq> S\<close> by auto
     show "inj_on f (ball a d)"
     unfolding inj_on_def
     proof (intro strip)
@@ -1726,55 +1557,36 @@
       assume as: "x \<in> ball a d" "y \<in> ball a d" "f x = f y"
       define ph where [abs_def]: "ph w = w - g' (f w - f x)" for w
       have ph':"ph = g' \<circ> (\<lambda>w. f' a w - (f w - f x))"
-        unfolding ph_def o_def
-        unfolding diff
-        using f'g'
-        by (auto simp: algebra_simps)
+        unfolding ph_def o_def  by (simp add: diff f'g')
       have "norm (ph x - ph y) \<le> (1 / 2) * norm (x - y)"
-        apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
-        apply (rule_tac[!] ballI)
-      proof -
+      proof (rule differentiable_bound[OF convex_ball _ _ as(1-2)])
         fix u
         assume u: "u \<in> ball a d"
-        then have "u \<in> s"
+        then have "u \<in> S"
           using d d2 by auto
         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
+          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' * 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)+
+          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)
-          using assms(5) \<open>u \<in> s\<close> \<open>a \<in> s\<close>
-          apply auto
-          done
-        have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)"
-          unfolding *
-          apply (rule onorm_compose)
-          apply (rule assms(3) **)+
-          done
+          using \<open>u \<in> S\<close> blin bounded_linear_sub derf by auto
+        then have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)"
+          by (simp add: "*" bounded_linear_axioms onorm_compose)
         also have "\<dots> \<le> onorm g' * k"
           apply (rule mult_left_mono)
           using d1(2)[of u]
-          using onorm_neg[where f="\<lambda>x. f' u x - f' a x"]
-          using d and u and onorm_pos_le[OF assms(3)]
-          apply (auto simp: algebra_simps)
+          using onorm_neg[where f="\<lambda>x. f' u x - f' a x"] d u onorm_pos_le[OF bling] apply (auto simp: algebra_simps)
           done
         also have "\<dots> \<le> 1 / 2"
           unfolding k_def by auto
         finally show "onorm (\<lambda>v. v - g' (f' u v)) \<le> 1 / 2" .
       qed
       moreover have "norm (ph y - ph x) = norm (y - x)"
-        apply (rule arg_cong[where f=norm])
-        unfolding ph_def
-        using diff
-        unfolding as
-        apply auto
-        done
+        by (simp add: as(3) ph_def)
       ultimately show "x = y"
         unfolding norm_minus_commute by auto
     qed
@@ -1786,32 +1598,28 @@
 
 lemma has_derivative_sequence_lipschitz_lemma:
   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>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
+  assumes "convex S"
+    and derf: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
+    and nle: "\<And>n x h. \<lbrakk>n\<ge>N; x \<in> S\<rbrakk> \<Longrightarrow> norm (f' n x h - g' x h) \<le> e * norm h"
     and "0 \<le> e"
-  shows "\<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> 2 * e * norm (x - y)"
-proof rule+
+  shows "\<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> 2 * e * norm (x - y)"
+proof clarify
   fix m n x y
-  assume as: "N \<le> m" "N \<le> n" "x \<in> s" "y \<in> s"
+  assume as: "N \<le> m" "N \<le> n" "x \<in> S" "y \<in> S"
   show "norm ((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm (x - y)"
-    apply (rule differentiable_bound[where f'="\<lambda>x h. f' m x h - f' n x h", OF assms(1) _ _ as(3-4)])
-    apply (rule_tac[!] ballI)
-  proof -
+  proof (rule differentiable_bound[where f'="\<lambda>x h. f' m x h - f' n x h", OF \<open>convex S\<close> _ _ as(3-4)])
     fix x
-    assume "x \<in> s"
-    show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
-      by (rule derivative_intros assms(2)[rule_format] \<open>x\<in>s\<close>)+
+    assume "x \<in> S"
+    show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within S)"
+      by (rule derivative_intros derf \<open>x\<in>S\<close>)+
     show "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e"
     proof (rule onorm_bound)
       fix h
       have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
         using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"]
-        unfolding norm_minus_commute
-        by (auto simp add: algebra_simps)
+        by (auto simp add: algebra_simps norm_minus_commute)
       also have "\<dots> \<le> e * norm h + e * norm h"
-        using assms(3)[rule_format,OF \<open>N \<le> m\<close> \<open>x \<in> s\<close>, of h]
-        using assms(3)[rule_format,OF \<open>N \<le> n\<close> \<open>x \<in> s\<close>, of h]
+        using nle[OF \<open>N \<le> m\<close> \<open>x \<in> S\<close>, of h] nle[OF \<open>N \<le> n\<close> \<open>x \<in> S\<close>, of h]
         by (auto simp add: field_simps)
       finally show "norm (f' m x h - f' n x h) \<le> 2 * e * norm h"
         by auto
@@ -1823,18 +1631,20 @@
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   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 nle: "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<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 -
-  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
+  have *: "2 * (e/2) = e"
+    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> (e/2) * norm h"
+    using nle \<open>e > 0\<close>
+    unfolding eventually_sequentially
+    by (metis less_divide_eq_numeral1(1) mult_zero_left)
   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 *])
+    apply (rule has_derivative_sequence_lipschitz_lemma[where e="e/2", unfolded *])
     using assms \<open>e > 0\<close>
     apply auto
     done
@@ -1843,60 +1653,51 @@
 lemma has_derivative_sequence:
   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 "\<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 derf: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
+    and nle: "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<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)"
+    and lim: "((\<lambda>n. f n x0) \<longlongrightarrow> l) sequentially"
+  shows "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) \<longlonglongrightarrow> g x \<and> (g has_derivative g'(x)) (at x within S)"
 proof -
   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"
-    apply (rule bchoice)
-    unfolding convergent_eq_Cauchy
-  proof
+  proof (intro ballI bchoice)
     fix x
     assume "x \<in> S"
-    show "Cauchy (\<lambda>n. f n x)"
+    show "\<exists>y. (\<lambda>n. f n x) \<longlonglongrightarrow> y"
+    unfolding convergent_eq_Cauchy
     proof (cases "x = x0")
       case True
-      then show ?thesis
-        using LIMSEQ_imp_Cauchy[OF assms(5)] by auto
+      then show "Cauchy (\<lambda>n. f n x)"
+        using LIMSEQ_imp_Cauchy[OF lim] by auto
     next
       case False
-      show ?thesis
+      show "Cauchy (\<lambda>n. f n x)"
         unfolding Cauchy_def
       proof (intro allI impI)
         fix e :: real
         assume "e > 0"
         hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto
         obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x0) (f n x0) < e / 2"
-          using LIMSEQ_imp_Cauchy[OF assms(5)]
-          unfolding Cauchy_def
-          using *(1) by blast
+          using LIMSEQ_imp_Cauchy[OF lim] * unfolding Cauchy_def 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>
-              e / 2 / norm (x - x0) * norm (xa - y)"
+            \<forall>u\<in>S. \<forall>y\<in>S. norm (f m u - f n u - (f m y - f n y)) \<le>
+              e / 2 / norm (x - x0) * norm (u - 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"
         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>
-              norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
+          have "dist (f m x) (f n x) \<le> norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
             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
-            by auto
+            using N \<open>x\<in>S\<close> \<open>x0\<in>S\<close> as False by fastforce
           also have "\<dots> < e / 2 + e / 2"
-            apply (rule add_strict_right_mono)
-            using as and M[rule_format]
-            unfolding dist_norm
-            apply auto
-            done
+            by (rule add_strict_right_mono) (use as M in \<open>auto simp: dist_norm\<close>)
           finally show "dist (f m x) (f n x) < e"
             by auto
         qed
@@ -1904,16 +1705,13 @@
     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)"
-  proof (rule, rule)
-    fix e :: real
-    assume *: "e > 0"
+  have lem2: "\<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)" if "e > 0" for e
+  proof -
     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)"
-      using lem1 * by blast
+      using lem1 \<open>e > 0\<close> 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)"
-      apply (rule_tac x=N in exI)
-    proof rule+
+    proof (intro exI ballI allI impI)
       fix n x y
       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"
@@ -1924,8 +1722,7 @@
         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)"
-          using N[rule_format, of n m x y] and as
-          by (auto simp add: algebra_simps)
+          using N as by (auto simp add: algebra_simps)
       qed
       ultimately show "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
         by (simp add: tendsto_upperbound)
@@ -1933,31 +1730,28 @@
   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)"
     unfolding has_derivative_within_alt2
-  proof (intro ballI conjI)
+  proof (intro ballI conjI allI impI)
     fix x
     assume "x \<in> S"
-    then show "((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
+    then show "(\<lambda>n. f n x) \<longlonglongrightarrow> g x"
       by (simp add: g)
-    have lem3: "\<forall>u. ((\<lambda>n. f' n x u) \<longlongrightarrow> g' x u) sequentially"
+    have tog': "(\<lambda>n. f' n x u) \<longlonglongrightarrow> g' x u" for u
       unfolding filterlim_def le_nhds_metric_le eventually_filtermap dist_norm
     proof (intro allI impI)
-      fix u
       fix e :: real
       assume "e > 0"
       show "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e) sequentially"
       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>
-          by (fast elim: eventually_mono)
+          using nle \<open>0 < e\<close> \<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)
+          using \<open>u = 0\<close> \<open>0 < e\<close> by (auto elim: eventually_mono)
       next
         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>
-          by (fast elim: eventually_mono)
+          using nle \<open>x \<in> S\<close> by (fast elim: eventually_mono)
         then show ?thesis
           using \<open>u \<noteq> 0\<close> by simp
       qed
@@ -1968,23 +1762,20 @@
       fix c :: real
       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])
+        apply (rule tendsto_unique[OF trivial_limit_sequentially tog'])
         unfolding lin[THEN bounded_linear.linear, THEN linear_cmul]
-        apply (intro tendsto_intros)
-        apply (rule lem3[rule_format])
+        apply (intro tendsto_intros tog')
         done
       show "g' x (y + z) = g' x y + g' x z"
-        apply (rule tendsto_unique[OF trivial_limit_sequentially])
-        apply (rule lem3[rule_format])
+        apply (rule tendsto_unique[OF trivial_limit_sequentially tog'])
         unfolding lin[THEN bounded_linear.linear, THEN linear_add]
         apply (rule tendsto_add)
-        apply (rule lem3[rule_format])+
+        apply (rule tog')+
         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 nle \<open>x \<in> S\<close> unfolding eventually_sequentially by (fast intro: zero_less_one)
       have "bounded_linear (f' N x)"
-        using assms(2) \<open>x \<in> S\<close> by fast
+        using derf \<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" ..
       {
@@ -2000,20 +1791,19 @@
       }
       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)"
-    proof (rule, rule)
-      fix e :: real
-      assume "e > 0"
-      then have *: "e / 3 > 0"
-        by auto
+    show "eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within S)"
+      if "e > 0" for e
+    proof -
+      have *: "e / 3 > 0"
+        using that 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"
-        using assms(3) * by blast
+        using nle * unfolding eventually_sequentially 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[rule_format]: "\<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
+        using derf[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)"
@@ -2022,7 +1812,7 @@
         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[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)"]
@@ -2045,7 +1835,8 @@
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
   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"
+    and no: "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially.
+       \<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
@@ -2058,7 +1849,7 @@
     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
+      apply auto
     done
 qed auto
 
@@ -2087,14 +1878,14 @@
     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"
+    show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S.  \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
+        unfolding eventually_sequentially
     proof (intro exI allI ballI impI)
       fix n x h
       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)
+        using n apply (auto simp add: field_simps)
         done
       show "norm (f' n x h - g' x h) \<le> e * norm h"
         by (meson "*" mult_right_mono norm_ge_zero order.trans x f')
@@ -2109,7 +1900,7 @@
   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 "\<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 "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<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)"
@@ -2130,7 +1921,9 @@
   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 "\<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
+  show "\<forall>\<^sub>F n in sequentially.
+       \<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
+    unfolding eventually_sequentially
   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
@@ -2217,17 +2010,17 @@
   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"
-    proof clarsimp
-      fix e :: real assume "0 < e"
-      with islimpt_approachable_real[of x S] not_bot
+  proof (rule frechet_derivative_unique_within, simp_all)
+    show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> S" if "0 < e"  for e
+    proof -
+      from that
       obtain x' where "x' \<in> S" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
+        using islimpt_approachable_real[of x S] not_bot
         by (auto simp add: trivial_limit_within)
-      then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> S"
-        by (intro exI[of _ "x' - x"]) auto
+      then show ?thesis
+        using eq_iff_diff_eq_0 by fastforce
     qed
-  qed (insert f' f'', auto simp: has_vector_derivative_def)
+  qed (use f' f'' in \<open>auto simp: has_vector_derivative_def\<close>)
   then show ?thesis
     unfolding fun_eq_iff by (metis scaleR_one)
 qed
@@ -2416,59 +2209,59 @@
 
 lemma vector_derivative_within_closed_interval:
   fixes f::"real \<Rightarrow> 'a::euclidean_space"
-  assumes "a < b" and "x \<in> {a .. b}"
-  assumes "(f has_vector_derivative f') (at x within {a .. b})"
-  shows "vector_derivative f (at x within {a .. b}) = f'"
+  assumes "a < b" and "x \<in> {a..b}"
+  assumes "(f has_vector_derivative f') (at x within {a..b})"
+  shows "vector_derivative f (at x within {a..b}) = f'"
   using assms vector_derivative_within_cbox
   by fastforce
 
 lemma has_vector_derivative_within_subset:
-  "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
+  "(f has_vector_derivative f') (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f has_vector_derivative f') (at x within T)"
   by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
 
 lemma has_vector_derivative_at_within:
-  "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
+  "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within S)"
   unfolding has_vector_derivative_def
   by (rule has_derivative_at_withinI)
 
 lemma has_vector_derivative_weaken:
-  fixes x D and f g s t
-  assumes f: "(f has_vector_derivative D) (at x within t)"
-    and "x \<in> s" "s \<subseteq> t"
-    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
-  shows "(g has_vector_derivative D) (at x within s)"
+  fixes x D and f g S T
+  assumes f: "(f has_vector_derivative D) (at x within T)"
+    and "x \<in> S" "S \<subseteq> T"
+    and "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
+  shows "(g has_vector_derivative D) (at x within S)"
 proof -
-  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
+  have "(f has_vector_derivative D) (at x within S) \<longleftrightarrow> (g has_vector_derivative D) (at x within S)"
     unfolding has_vector_derivative_def has_derivative_iff_norm
     using assms by (intro conj_cong Lim_cong_within refl) auto
   then show ?thesis
-    using has_vector_derivative_within_subset[OF f \<open>s \<subseteq> t\<close>] by simp
+    using has_vector_derivative_within_subset[OF f \<open>S \<subseteq> T\<close>] by simp
 qed
 
 lemma has_vector_derivative_transform_within:
-  assumes "(f has_vector_derivative f') (at x within s)"
+  assumes "(f has_vector_derivative f') (at x within S)"
     and "0 < d"
-    and "x \<in> s"
-    and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
-    shows "(g has_vector_derivative f') (at x within s)"
+    and "x \<in> S"
+    and "\<And>x'. \<lbrakk>x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
+    shows "(g has_vector_derivative f') (at x within S)"
   using assms
   unfolding has_vector_derivative_def
   by (rule has_derivative_transform_within)
 
 lemma has_vector_derivative_transform_within_open:
   assumes "(f has_vector_derivative f') (at x)"
-    and "open s"
-    and "x \<in> s"
-    and "\<And>y. y\<in>s \<Longrightarrow> f y = g y"
+    and "open S"
+    and "x \<in> S"
+    and "\<And>y. y\<in>S \<Longrightarrow> f y = g y"
   shows "(g has_vector_derivative f') (at x)"
   using assms
   unfolding has_vector_derivative_def
   by (rule has_derivative_transform_within_open)
 
 lemma has_vector_derivative_transform:
-  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
-  assumes f': "(f has_vector_derivative f') (at x within s)"
-  shows "(g has_vector_derivative f') (at x within s)"
+  assumes "x \<in> S" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+  assumes f': "(f has_vector_derivative f') (at x within S)"
+  shows "(g has_vector_derivative f') (at x within S)"
   using assms
   unfolding has_vector_derivative_def
   by (rule has_derivative_transform)
@@ -2477,23 +2270,13 @@
   assumes "(f has_vector_derivative f') (at x)"
     and "(g has_vector_derivative g') (at (f x))"
   shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)"
-  using assms(2)
-  unfolding has_vector_derivative_def
-  apply -
-  apply (drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
-  apply (simp only: o_def real_scaleR_def scaleR_scaleR)
-  done
+  using assms has_vector_derivative_at_within has_vector_derivative_def vector_derivative_diff_chain_within by blast
 
 lemma vector_diff_chain_within:
   assumes "(f has_vector_derivative f') (at x within s)"
     and "(g has_vector_derivative g') (at (f x) within f ` s)"
   shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)"
-  using assms(2)
-  unfolding has_vector_derivative_def
-  apply -
-  apply (drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
-  apply (simp only: o_def real_scaleR_def scaleR_scaleR)
-  done
+  using assms has_vector_derivative_def vector_derivative_diff_chain_within by blast
 
 lemma vector_derivative_const_at [simp]: "vector_derivative (\<lambda>x. c) (at a) = 0"
   by (simp add: vector_derivative_at)
@@ -2518,11 +2301,11 @@
  by (auto simp: o_def mult.commute has_vector_derivative_def)
 
 lemma vector_derivative_chain_within: 
-  assumes "at x within s \<noteq> bot" "f differentiable (at x within s)" 
-    "(g has_derivative g') (at (f x) within f ` s)" 
-  shows "vector_derivative (g \<circ> f) (at x within s) =
-        g' (vector_derivative f (at x within s)) "
-  apply (rule vector_derivative_within [OF \<open>at x within s \<noteq> bot\<close>])
+  assumes "at x within S \<noteq> bot" "f differentiable (at x within S)" 
+    "(g has_derivative g') (at (f x) within f ` S)" 
+  shows "vector_derivative (g \<circ> f) (at x within S) =
+        g' (vector_derivative f (at x within S)) "
+  apply (rule vector_derivative_within [OF \<open>at x within S \<noteq> bot\<close>])
   apply (rule vector_derivative_diff_chain_within)
   using assms(2-3) vector_derivative_works
   by auto
@@ -2543,26 +2326,22 @@
 by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
 
 lemma field_differentiable_imp_continuous_at:
-    "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
+    "f field_differentiable (at x within S) \<Longrightarrow> continuous (at x within S) f"
   by (metis DERIV_continuous field_differentiable_def)
 
 lemma field_differentiable_within_subset:
-    "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
-     \<Longrightarrow> f field_differentiable (at x within t)"
+    "\<lbrakk>f field_differentiable (at x within S); T \<subseteq> S\<rbrakk> \<Longrightarrow> f field_differentiable (at x within T)"
   by (metis DERIV_subset field_differentiable_def)
 
 lemma field_differentiable_at_within:
     "\<lbrakk>f field_differentiable (at x)\<rbrakk>
-     \<Longrightarrow> f field_differentiable (at x within s)"
+     \<Longrightarrow> f field_differentiable (at x within S)"
   unfolding field_differentiable_def
   by (metis DERIV_subset top_greatest)
 
 lemma field_differentiable_linear [simp,derivative_intros]: "(( * ) c) field_differentiable F"
-proof -
-  show ?thesis
-    unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
-    by (force intro: has_derivative_mult_right)
-qed
+  unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
+  by (force intro: has_derivative_mult_right)
 
 lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
   unfolding field_differentiable_def has_field_derivative_def
@@ -2602,45 +2381,45 @@
   by (metis field_differentiable_diff)
 
 lemma field_differentiable_inverse [derivative_intros]:
-  assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
-  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
+  assumes "f field_differentiable (at a within S)" "f a \<noteq> 0"
+  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within S)"
   using assms unfolding field_differentiable_def
   by (metis DERIV_inverse_fun)
 
 lemma field_differentiable_mult [derivative_intros]:
-  assumes "f field_differentiable (at a within s)"
-          "g field_differentiable (at a within s)"
-    shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
+  assumes "f field_differentiable (at a within S)"
+          "g field_differentiable (at a within S)"
+    shows "(\<lambda>z. f z * g z) field_differentiable (at a within S)"
   using assms unfolding field_differentiable_def
-  by (metis DERIV_mult [of f _ a s g])
+  by (metis DERIV_mult [of f _ a S g])
 
 lemma field_differentiable_divide [derivative_intros]:
-  assumes "f field_differentiable (at a within s)"
-          "g field_differentiable (at a within s)"
+  assumes "f field_differentiable (at a within S)"
+          "g field_differentiable (at a within S)"
           "g a \<noteq> 0"
-    shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
+    shows "(\<lambda>z. f z / g z) field_differentiable (at a within S)"
   using assms unfolding field_differentiable_def
-  by (metis DERIV_divide [of f _ a s g])
+  by (metis DERIV_divide [of f _ a S g])
 
 lemma field_differentiable_power [derivative_intros]:
-  assumes "f field_differentiable (at a within s)"
-    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
+  assumes "f field_differentiable (at a within S)"
+    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within S)"
   using assms unfolding field_differentiable_def
   by (metis DERIV_power)
 
 lemma field_differentiable_transform_within:
   "0 < d \<Longrightarrow>
-        x \<in> s \<Longrightarrow>
-        (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
-        f field_differentiable (at x within s)
-        \<Longrightarrow> g field_differentiable (at x within s)"
+        x \<in> S \<Longrightarrow>
+        (\<And>x'. x' \<in> S \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
+        f field_differentiable (at x within S)
+        \<Longrightarrow> g field_differentiable (at x within S)"
   unfolding field_differentiable_def has_field_derivative_def
   by (blast intro: has_derivative_transform_within)
 
 lemma field_differentiable_compose_within:
-  assumes "f field_differentiable (at a within s)"
-          "g field_differentiable (at (f a) within f`s)"
-    shows "(g o f) field_differentiable (at a within s)"
+  assumes "f field_differentiable (at a within S)"
+          "g field_differentiable (at (f a) within f`S)"
+    shows "(g o f) field_differentiable (at a within S)"
   using assms unfolding field_differentiable_def
   by (metis DERIV_image_chain)
 
@@ -2650,7 +2429,7 @@
 by (metis field_differentiable_at_within field_differentiable_compose_within)
 
 lemma field_differentiable_within_open:
-     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
+     "\<lbrakk>a \<in> S; open S\<rbrakk> \<Longrightarrow> f field_differentiable at a within S \<longleftrightarrow>
                           f field_differentiable at a"
   unfolding field_differentiable_def
   by (metis at_within_open)
@@ -2692,9 +2471,7 @@
     unfolding *
     by (rule tendsto_norm_zero_cancel) (auto intro!: tendsto_eq_intros)
 
-  moreover
-
-  have "\<forall>\<^sub>F x in at t within T. x \<noteq> t"
+  moreover have "\<forall>\<^sub>F x in at t within T. x \<noteq> t"
     by (simp add: eventually_at_filter)
   then have "\<forall>\<^sub>F x in at t within T. ((x - t) / \<bar>x - t\<bar>) *\<^sub>R ((\<Sum>n. ?e n x) - A) =
     (exp ((x - t) *\<^sub>R A) - 1 - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t)"
@@ -2721,9 +2498,7 @@
       by (simp add: divide_simps)
   qed
 
-  ultimately
-
-  have "((\<lambda>y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0) (at t within T)"
+  ultimately have "((\<lambda>y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0) (at t within T)"
     by (rule Lim_transform_eventually[rotated])
   from tendsto_mult_right_zero[OF this, where c="exp (t *\<^sub>R A)"]
   show "((\<lambda>y. (exp (y *\<^sub>R A) - exp (t *\<^sub>R A) - (y - t) *\<^sub>R (exp (t *\<^sub>R A) * A)) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0)
@@ -2756,7 +2531,7 @@
   also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_Int_closure_subset) auto
   finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
   moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
-    unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
+    unfolding has_field_derivative_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
   moreover from eventually_at_right_real[OF xc]
     have "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at_right c)"
   proof eventually_elim
@@ -2778,7 +2553,7 @@
   also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_Int_closure_subset) auto
   finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
   moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
-    unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
+    unfolding has_field_derivative_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
   moreover from eventually_at_left_real[OF xc]
     have "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at_left c)"
   proof eventually_elim
@@ -2816,8 +2591,7 @@
 
 lemma eventually_at_Pair_within_TimesI2:
   fixes x::"'a::metric_space"
-  assumes "\<forall>\<^sub>F y' in at y within Y. P y'"
-  assumes "P y"
+  assumes "\<forall>\<^sub>F y' in at y within Y. P y'" "P y"
   shows "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'"
 proof -
   from assms[unfolded eventually_at_topological]
@@ -2907,12 +2681,12 @@
       have "\<dots> \<subseteq> ball y d \<inter> Y"
         using \<open>y \<in> Y\<close> \<open>0 < d\<close> dy y'
         by (intro \<open>convex ?S\<close>[unfolded convex_contains_segment, rule_format, of y y'])
-          (auto simp: dist_commute mem_ball)
+          (auto simp: dist_commute)
       finally have "y + t *\<^sub>R (y' - y) \<in> ?S" .
     } note seg = this
 
-    have "\<forall>x\<in>ball y d \<inter> Y. onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
-      by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: mem_ball dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
+    have "\<And>x. x \<in> ball y d \<inter> Y \<Longrightarrow> onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
+      by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
     with seg has_derivative_within_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
     show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
       by (rule differentiable_bound_linearization[where S="?S"])
@@ -2923,10 +2697,10 @@
   from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
   have "\<forall>\<^sub>F x' in at x within X. ?le x'"
     by eventually_elim
-       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps fx.zero split: if_split_asm)
+       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
   then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
     by (rule eventually_at_Pair_within_TimesI1)
-       (simp add: blinfun.bilinear_simps fx.zero)
+       (simp add: blinfun.bilinear_simps)
   moreover have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm ((x', y') - (x, y)) \<noteq> 0"
     unfolding norm_eq_zero right_minus_eq
     by (auto simp: eventually_at intro!: zero_less_one)
@@ -2996,11 +2770,11 @@
 subsection \<open>Differentiable case distinction\<close>
 
 lemma has_derivative_within_If_eq:
-  "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within s) =
+  "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within S) =
     (bounded_linear f' \<and>
      ((\<lambda>y.(if P y then (f y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)
            else (g y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)))
-      \<longlongrightarrow> 0) (at x within s))"
+      \<longlongrightarrow> 0) (at x within S))"
   (is "_ = (_ \<and> (?if \<longlongrightarrow> 0) _)")
 proof -
   have "(\<lambda>y. (1 / norm (y - x)) *\<^sub>R
@@ -3011,41 +2785,41 @@
 qed
 
 lemma has_derivative_If_within_closures:
-  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
-    (f has_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
-  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
-    (g has_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
-  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
-  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
-  assumes x_in: "x \<in> s \<union> t"
-  shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative
-      (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
+  assumes f': "x \<in> S \<union> (closure S \<inter> closure T) \<Longrightarrow>
+    (f has_derivative f' x) (at x within S \<union> (closure S \<inter> closure T))"
+  assumes g': "x \<in> T \<union> (closure S \<inter> closure T) \<Longrightarrow>
+    (g has_derivative g' x) (at x within T \<union> (closure S \<inter> closure T))"
+  assumes connect: "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f x = g x"
+  assumes connect': "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f' x = g' x"
+  assumes x_in: "x \<in> S \<union> T"
+  shows "((\<lambda>x. if x \<in> S then f x else g x) has_derivative
+      (if x \<in> S then f' x else g' x)) (at x within (S \<union> T))"
 proof -
-  from f' x_in interpret f': bounded_linear "if x \<in> s then f' x else (\<lambda>x. 0)"
+  from f' x_in interpret f': bounded_linear "if x \<in> S then f' x else (\<lambda>x. 0)"
     by (auto simp add: has_derivative_within)
-  from g' interpret g': bounded_linear "if x \<in> t then g' x else (\<lambda>x. 0)"
+  from g' interpret g': bounded_linear "if x \<in> T then g' x else (\<lambda>x. 0)"
     by (auto simp add: has_derivative_within)
-  have bl: "bounded_linear (if x \<in> s then f' x else g' x)"
+  have bl: "bounded_linear (if x \<in> S then f' x else g' x)"
     using f'.scaleR f'.bounded f'.add g'.scaleR g'.bounded g'.add x_in
     by (unfold_locales; force)
   show ?thesis
-    using f' g' closure_subset[of t] closure_subset[of s]
+    using f' g' closure_subset[of T] closure_subset[of S]
     unfolding has_derivative_within_If_eq
     by (intro conjI bl tendsto_If_within_closures x_in)
       (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp)
 qed
 
 lemma has_vector_derivative_If_within_closures:
-  assumes x_in: "x \<in> s \<union> t"
-  assumes "u = s \<union> t"
-  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
-    (f has_vector_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
-  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
-    (g has_vector_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
-  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
-  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
-  shows "((\<lambda>x. if x \<in> s then f x else g x) has_vector_derivative
-    (if x \<in> s then f' x else g' x)) (at x within u)"
+  assumes x_in: "x \<in> S \<union> T"
+  assumes "u = S \<union> T"
+  assumes f': "x \<in> S \<union> (closure S \<inter> closure T) \<Longrightarrow>
+    (f has_vector_derivative f' x) (at x within S \<union> (closure S \<inter> closure T))"
+  assumes g': "x \<in> T \<union> (closure S \<inter> closure T) \<Longrightarrow>
+    (g has_vector_derivative g' x) (at x within T \<union> (closure S \<inter> closure T))"
+  assumes connect: "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f x = g x"
+  assumes connect': "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f' x = g' x"
+  shows "((\<lambda>x. if x \<in> S then f x else g x) has_vector_derivative
+    (if x \<in> S then f' x else g' x)) (at x within u)"
   unfolding has_vector_derivative_def assms
   using x_in
   apply (intro has_derivative_If_within_closures[where
diff -r 88dd06301dd3 -r 0764ee22a4d1 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun May 20 18:37:34 2018 +0100
@@ -5089,9 +5089,9 @@
             using B' [of a b] B' [of c d] norm_triangle_half_r by blast
         qed
       qed (use \<open>B > 0\<close> in auto)}
-  then show ?thesis
-    by force
-qed
+    then show ?thesis
+      by force
+  qed
   finally show ?thesis .
 qed
 
@@ -6496,7 +6496,7 @@
           unfolding has_vector_derivative_def[symmetric]
           using that \<open>x \<in> X0\<close>
           by (intro has_derivative_within_subset[OF fx]) auto
-        have "\<forall>x \<in> X0 \<inter> U. onorm (blinfun_apply (fx x t) - (fx x0 t)) \<le> e"
+        have "\<And>x. x \<in> X0 \<inter> U \<Longrightarrow> onorm (blinfun_apply (fx x t) - (fx x0 t)) \<le> e"
           using fx_bound t
           by (auto simp add: norm_blinfun_def fun_diff_def blinfun.bilinear_simps[symmetric])
         from differentiable_bound_linearization[OF seg deriv this] X0
diff -r 88dd06301dd3 -r 0764ee22a4d1 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun May 20 18:37:34 2018 +0100
@@ -250,8 +250,8 @@
 lemma homeomorphic_closed_intervals_real:
   fixes a::real and b and c::real and d
   assumes "a<b" and "c<d"
-    shows "{a..b} homeomorphic {c..d}"
-by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt)
+  shows "{a..b} homeomorphic {c..d}"
+  using assms by (auto intro: homeomorphic_convex_compact)
 
 no_notation
   eucl_less (infix "<e" 50)