# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1531688330 -3600
# Node ID 87d1bff264df0c7edeb73f3df4dd7f641cfd73c0
# Parent  ec8c7c9459e0a761447281ab9dd1a6932aa6e0c5
de-applying and meta-quantifying

diff -r ec8c7c9459e0 -r 87d1bff264df src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Sun Jul 15 18:22:31 2018 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy	Sun Jul 15 21:58:50 2018 +0100
@@ -863,10 +863,10 @@
   have lle[simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
   have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
   have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
-  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI allI impI)
-    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
+  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI)
+    show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
       by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
-    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> 0 \<le> g' u"
+    show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> 0 \<le> g' u"
       by (meson assms(5) dual_order.trans le_ereal_le less_imp_le order_refl that)
   qed
   have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
@@ -960,10 +960,10 @@
   have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
   have uleu[simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
   have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
-  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI allI impI)
-    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
+  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI)
+    show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
       by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
-    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> 0 \<le> g' u"
+    show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> 0 \<le> g' u"
       by (meson g'_nonneg less_ereal.simps(1) less_trans not_less that)
   qed
   have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
diff -r ec8c7c9459e0 -r 87d1bff264df src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sun Jul 15 18:22:31 2018 +0100
+++ b/src/HOL/Deriv.thy	Sun Jul 15 21:58:50 2018 +0100
@@ -1372,8 +1372,8 @@
 theorem MVT:
   fixes a b :: real
   assumes lt: "a < b"
-    and con: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
-    and dif [rule_format]: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)"
+    and con:  "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" 
+    and dif: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)"
   shows "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l"
 proof -
   let ?F = "\<lambda>x. f x - ((f b - f a) / (b - a)) * x"
@@ -1384,7 +1384,7 @@
     fix x :: real
     assume x: "a < x" "x < b"
     obtain l where der: "DERIV f x :> l"
-      using differentiableD [OF dif [OF conjI [OF x]]] ..
+      using differentiableD [OF dif] x by blast 
     show "?F differentiable (at x)"
       by (rule differentiableI [where D = "l - (f b - f a) / (b - a)"],
           blast intro: DERIV_diff DERIV_cmult_Id der)
@@ -1413,9 +1413,9 @@
            (f has_real_derivative l) (at z) \<and>
            f b - f a = (b - a) * l"
   proof (rule MVT [OF \<open>a < b\<close>])
-    show "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
+    show  "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" 
       using assms by (blast intro: DERIV_isCont)
-    show "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable at x"
+    show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)"
       using assms by (force dest: order_less_imp_le simp add: real_differentiable_def)
   qed
   with assms show ?thesis
@@ -1441,34 +1441,21 @@
 
 lemma DERIV_isconst_end:
   fixes f :: "real \<Rightarrow> real"
-  shows "a < b \<Longrightarrow>
-    \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
-    \<forall>x. a < x \<and> x < b \<longrightarrow> DERIV f x :> 0 \<Longrightarrow> f b = f a"
-  apply (drule (1) MVT)
-   apply (blast intro: differentiableI)
-  apply (auto dest!: DERIV_unique simp add: diff_eq_eq)
-  done
-
-lemma DERIV_isconst1:
-  fixes f :: "real \<Rightarrow> real"
-  shows "a < b \<Longrightarrow>
-    \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
-    \<forall>x. a < x \<and> x < b \<longrightarrow> DERIV f x :> 0 \<Longrightarrow>
-    \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x = f a"
-  apply safe
-  apply (drule_tac x = a in order_le_imp_less_or_eq)
-  apply safe
-  apply (drule_tac b = x in DERIV_isconst_end)
-    apply auto
-  done
+  assumes "a < b" and contf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" 
+    and 0: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> DERIV f x :> 0"
+  shows "f b = f a"
+  using  MVT [OF \<open>a < b\<close>] "0" DERIV_unique contf real_differentiable_def by fastforce
 
 lemma DERIV_isconst2:
   fixes f :: "real \<Rightarrow> real"
-  shows "a < b \<Longrightarrow>
-    \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
-    \<forall>x. a < x \<and> x < b \<longrightarrow> DERIV f x :> 0 \<Longrightarrow>
-    a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> f x = f a"
-  by (blast dest: DERIV_isconst1)
+  assumes "a < b" "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> DERIV f x :> 0"
+    and "a \<le> x" "x \<le> b"
+shows "f x = f a"
+proof (cases "x=a")
+  case False
+  show ?thesis
+    by (rule DERIV_isconst_end [where f=f]) (use False assms in auto)
+qed auto
 
 lemma DERIV_isconst3:
   fixes a b x y :: real
@@ -1482,17 +1469,15 @@
   let ?a = "min x y"
   let ?b = "max x y"
 
-  have "\<forall>z. ?a \<le> z \<and> z \<le> ?b \<longrightarrow> DERIV f z :> 0"
-  proof (rule allI, rule impI)
-    fix z :: real
-    assume "?a \<le> z \<and> z \<le> ?b"
-    then have "a < z" and "z < b"
-      using \<open>x \<in> {a <..< b}\<close> and \<open>y \<in> {a <..< b}\<close> by auto
+  have "DERIV f z :> 0" if "?a \<le> z" "z \<le> ?b" for z
+  proof -
+    have "a < z" and "z < b"
+      using that \<open>x \<in> {a <..< b}\<close> and \<open>y \<in> {a <..< b}\<close> by auto
     then have "z \<in> {a<..<b}" by auto
     then show "DERIV f z :> 0" by (rule derivable)
   qed
-  then have isCont: "\<forall>z. ?a \<le> z \<and> z \<le> ?b \<longrightarrow> isCont f z"
-    and DERIV: "\<forall>z. ?a < z \<and> z < ?b \<longrightarrow> DERIV f z :> 0"
+  then have isCont: "\<And>z. \<lbrakk>?a \<le> z; z \<le> ?b\<rbrakk> \<Longrightarrow> isCont f z"
+    and DERIV: "\<And>z. \<lbrakk>?a < z; z < ?b\<rbrakk> \<Longrightarrow> DERIV f z :> 0"
     using DERIV_isCont by auto
 
   have "?a < ?b" using \<open>x \<noteq> y\<close> by auto
@@ -1509,20 +1494,24 @@
 
 lemma DERIV_const_ratio_const:
   fixes f :: "real \<Rightarrow> real"
-  shows "a \<noteq> b \<Longrightarrow> \<forall>x. DERIV f x :> k \<Longrightarrow> f b - f a = (b - a) * k"
-  apply (rule linorder_cases [of a b])
-    apply auto
-   apply (drule_tac [!] f = f in MVT)
-       apply (auto dest: DERIV_isCont DERIV_unique simp: real_differentiable_def)
-  apply (auto dest: DERIV_unique simp: ring_distribs)
-  done
+  assumes "a \<noteq> b" and df: "\<And>x. DERIV f x :> k"
+  shows "f b - f a = (b - a) * k"
+proof (cases a b rule: linorder_cases)
+  case less
+  show ?thesis
+    using MVT [OF less] df by (auto dest: DERIV_isCont DERIV_unique simp: real_differentiable_def)
+next
+  case greater
+  show ?thesis
+    using MVT [OF greater] df
+    by (fastforce dest: DERIV_continuous DERIV_unique simp: real_differentiable_def algebra_simps)
+qed auto
 
 lemma DERIV_const_ratio_const2:
   fixes f :: "real \<Rightarrow> real"
-  shows "a \<noteq> b \<Longrightarrow> \<forall>x. DERIV f x :> k \<Longrightarrow> (f b - f a) / (b - a) = k"
-  apply (rule_tac c1 = "b-a" in mult_right_cancel [THEN iffD1])
-   apply (auto dest!: DERIV_const_ratio_const simp add: mult.assoc)
-  done
+  assumes "a \<noteq> b" and df: "\<And>x. DERIV f x :> k"
+  shows "(f b - f a) / (b - a) = k"
+  using DERIV_const_ratio_const [OF assms] \<open>a \<noteq> b\<close> by auto
 
 lemma real_average_minus_first [simp]: "(a + b) / 2 - a = (b - a) / 2"
   for a b :: real
@@ -1538,7 +1527,7 @@
   fixes v :: "real \<Rightarrow> real"
     and a b :: real
   assumes neq: "a \<noteq> b"
-    and der: "\<forall>x. DERIV v x :> k"
+    and der: "\<And>x. DERIV v x :> k"
   shows "v ((a + b) / 2) = (v a + v b) / 2"
 proof (cases rule: linorder_cases [of a b])
   case equal
@@ -1598,7 +1587,7 @@
   fixes a b :: real
     and f :: "real \<Rightarrow> real"
   assumes "a \<le> b"
-    and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y \<ge> 0)"
+    and "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y \<ge> 0"
   shows "f a \<le> f b"
 proof (rule ccontr, cases "a = b")
   assume "\<not> ?thesis" and "a = b"
@@ -1606,13 +1595,11 @@
 next
   assume *: "\<not> ?thesis"
   assume "a \<noteq> b"
+  with \<open>a \<le> b\<close> have "a < b"
+    by linarith
   with assms have "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l"
-    apply -
-    apply (rule MVT)
-      apply auto
-     apply (metis DERIV_isCont)
-    apply (metis differentiableI less_le)
-    done
+    by (metis (no_types) not_le not_less_iff_gr_or_eq  
+                         MVT [OF \<open>a < b\<close>, of f] DERIV_isCont [of f] differentiableI)
   then obtain l z where lz: "a < z" "z < b" "DERIV f z :> l" and **: "f b - f a = (b - a) * l"
     by auto
   with * have "a < b" "f b < f a" by auto
@@ -1626,16 +1613,16 @@
   fixes a b :: real
     and f :: "real \<Rightarrow> real"
   assumes "a < b"
-    and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y < 0)"
+    and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0"
     and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
   shows "f a > f b"
 proof -
   have "(\<lambda>x. -f x) a < (\<lambda>x. -f x) b"
-    apply (rule DERIV_pos_imp_increasing_open [of a b "\<lambda>x. -f x"])
-    using assms
-      apply auto
-    apply (metis field_differentiable_minus neg_0_less_iff_less)
-    done
+  proof (rule DERIV_pos_imp_increasing_open [of a b])
+    show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> \<exists>y. ((\<lambda>x. - f x) has_real_derivative y) (at x) \<and> 0 < y"
+      using assms
+      by simp (metis field_differentiable_minus neg_0_less_iff_less)
+  qed (use assms in auto)
   then show ?thesis
     by simp
 qed
@@ -1644,7 +1631,7 @@
   fixes a b :: real
     and f :: "real \<Rightarrow> real"
   assumes "a < b"
-    and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y < 0)"
+    and "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0"
   shows "f a > f b"
   by (metis DERIV_neg_imp_decreasing_open [of a b f] assms DERIV_continuous less_imp_le)
 
@@ -1652,15 +1639,11 @@
   fixes a b :: real
     and f :: "real \<Rightarrow> real"
   assumes "a \<le> b"
-    and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y \<le> 0)"
+    and "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y \<le> 0"
   shows "f a \<ge> f b"
 proof -
   have "(\<lambda>x. -f x) a \<le> (\<lambda>x. -f x) b"
-    apply (rule DERIV_nonneg_imp_nondecreasing [of a b "\<lambda>x. -f x"])
-    using assms
-     apply auto
-    apply (metis DERIV_minus neg_0_le_iff_le)
-    done
+    using DERIV_nonneg_imp_nondecreasing [of a b "\<lambda>x. -f x"] assms DERIV_minus by fastforce
   then show ?thesis
     by simp
 qed
@@ -1672,11 +1655,9 @@
   shows "flim < f b"
 proof -
   have "\<exists>N. \<forall>n\<le>N. f n \<le> f (b - 1)"
-    apply (rule_tac x="b - 2" in exI)
-    apply (force intro: order.strict_implies_order DERIV_pos_imp_increasing [where f=f] assms)
-    done
+    by (rule_tac x="b - 2" in exI) (force intro: order.strict_implies_order DERIV_pos_imp_increasing assms)
   then have "flim \<le> f (b - 1)"
-     by (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder tendsto_upperbound [OF lim])
+     by (auto simp: eventually_at_bot_linorder tendsto_upperbound [OF lim])
   also have "\<dots> < f b"
     by (force intro: DERIV_pos_imp_increasing [where f=f] assms)
   finally show ?thesis .
@@ -1684,7 +1665,7 @@
 
 lemma DERIV_neg_imp_decreasing_at_top:
   fixes f :: "real \<Rightarrow> real"
-  assumes der: "\<And>x. x \<ge> b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y < 0)"
+  assumes der: "\<And>x. x \<ge> b \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0"
     and lim: "(f \<longlongrightarrow> flim) at_top"
   shows "flim < f b"
   apply (rule DERIV_pos_imp_increasing_at_bot [where f = "\<lambda>i. f (-i)" and b = "-b", simplified])
@@ -1755,9 +1736,9 @@
   have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l"
   proof (rule MVT)
     from assms show "a < b" by simp
-    show "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
+    show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont ?h x"
       using fc gc by simp
-    show "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable (at x)"
+    show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> ?h differentiable (at x)"
       using fd gd by simp
   qed
   then obtain l where l: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
@@ -1822,15 +1803,20 @@
 
 lemma isCont_If_ge:
   fixes a :: "'a :: linorder_topology"
-  shows "continuous (at_left a) g \<Longrightarrow> (f \<longlongrightarrow> g a) (at_right a) \<Longrightarrow>
-    isCont (\<lambda>x. if x \<le> a then g x else f x) a"
-  unfolding isCont_def continuous_within
-  apply (intro filterlim_split_at)
-   apply (subst filterlim_cong[OF refl refl, where g=g])
-    apply (simp_all add: eventually_at_filter less_le)
-  apply (subst filterlim_cong[OF refl refl, where g=f])
-   apply (simp_all add: eventually_at_filter less_le)
-  done
+  assumes "continuous (at_left a) g" and f: "(f \<longlongrightarrow> g a) (at_right a)"
+  shows "isCont (\<lambda>x. if x \<le> a then g x else f x) a" (is "isCont ?gf a")
+proof -
+  have g: "(g \<longlongrightarrow> g a) (at_left a)"
+    using assms continuous_within by blast
+  show ?thesis
+    unfolding isCont_def continuous_within
+  proof (intro filterlim_split_at; simp)
+    show "(?gf \<longlongrightarrow> g a) (at_left a)"
+      by (subst filterlim_cong[OF refl refl, where g=g]) (simp_all add: eventually_at_filter less_le g)
+    show "(?gf \<longlongrightarrow> g a) (at_right a)"
+      by (subst filterlim_cong[OF refl refl, where g=f]) (simp_all add: eventually_at_filter less_le f)
+  qed
+qed
 
 lemma lhopital_right_0:
   fixes f0 g0 :: "real \<Rightarrow> real"
@@ -2089,19 +2075,11 @@
   show "eventually (\<lambda>x. DERIV ?G x  :> ?D g' x) ?R"
     unfolding eventually_at_right_to_top
     using Dg eventually_ge_at_top[where c=1]
-    apply eventually_elim
-    apply (rule DERIV_cong)
-     apply (rule DERIV_chain'[where f=inverse])
-      apply (auto intro!:  DERIV_inverse)
-    done
+    by eventually_elim (rule derivative_eq_intros DERIV_chain'[where f=inverse] | simp)+
   show "eventually (\<lambda>x. DERIV ?F x  :> ?D f' x) ?R"
     unfolding eventually_at_right_to_top
     using Df eventually_ge_at_top[where c=1]
-    apply eventually_elim
-    apply (rule DERIV_cong)
-     apply (rule DERIV_chain'[where f=inverse])
-      apply (auto intro!:  DERIV_inverse)
-    done
+    by eventually_elim (rule derivative_eq_intros DERIV_chain'[where f=inverse] | simp)+
   show "eventually (\<lambda>x. ?D g' x \<noteq> 0) ?R"
     unfolding eventually_at_right_to_top
     using g' eventually_ge_at_top[where c=1]
diff -r ec8c7c9459e0 -r 87d1bff264df src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Jul 15 18:22:31 2018 +0100
+++ b/src/HOL/Transcendental.thy	Sun Jul 15 21:58:50 2018 +0100
@@ -2236,7 +2236,7 @@
     assume "1 < x"
     from dense[OF this] obtain a where "1 < a" "a < x" by blast
     from \<open>a < x\<close> have "?l x < ?l a"
-    proof (rule DERIV_neg_imp_decreasing, safe)
+    proof (rule DERIV_neg_imp_decreasing)
       fix y
       assume "a \<le> y" "y \<le> x"
       with \<open>1 < a\<close> have "1 / y - 1 < 0" "0 < y"
@@ -2367,10 +2367,8 @@
   shows "x \<le> (exp x - inverse(exp x)) / 2"
 proof -
   have *: "exp a - inverse(exp a) - 2*a \<le> exp b - inverse(exp b) - 2*b" if "a \<le> b" for a b::real
-    apply (rule DERIV_nonneg_imp_nondecreasing [OF that])
     using exp_plus_inverse_exp
-    apply (intro exI allI impI conjI derivative_eq_intros | force)+
-    done
+    by (fastforce intro: derivative_eq_intros DERIV_nonneg_imp_nondecreasing [OF that])
   show ?thesis
     using*[OF assms] by simp
 qed
@@ -2559,9 +2557,7 @@
   by (simp add: log_def)
 
 lemma log_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a (inverse x) = - log a x"
-  apply (rule add_left_cancel [THEN iffD1, where a1 = "log a x"])
-  apply (simp add: log_mult [symmetric])
-  done
+  using ln_inverse log_def by auto
 
 lemma log_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a (x/y) = log a x - log a y"
   by (simp add: log_mult divide_inverse log_inverse)
@@ -3134,10 +3130,7 @@
     show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
       unfolding eventually_at_right[OF zero_less_one]
       using False
-      apply (intro exI[of _ "1 / \<bar>x\<bar>"])
-      apply (auto simp: field_simps powr_def abs_if)
-      apply (metis add_less_same_cancel1 mult_less_0_iff not_less_iff_gr_or_eq zero_less_one)
-      done
+      by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def abs_if add_nonneg_eq_0_iff)
   qed (simp_all add: at_eq_sup_left_right)
 qed
 
@@ -5758,9 +5751,9 @@
         qed
         then have DERIV_in_rball: "\<forall>y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda>x. suminf (?c x) - arctan x) y :> 0"
           using \<open>-r < a\<close> \<open>b < r\<close> by auto
-        then show "\<forall>y. a < y \<and> y < b \<longrightarrow> DERIV (\<lambda>x. suminf (?c x) - arctan x) y :> 0"
+        then show "\<And>y. \<lbrakk>a < y; y < b\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. suminf (?c x) - arctan x) y :> 0"
           using \<open>\<bar>x\<bar> < r\<close> by auto
-        show "\<forall>y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda>x. suminf (?c x) - arctan x) y"
+        show "\<And>y. \<lbrakk>a \<le> y; y \<le> b\<rbrakk> \<Longrightarrow>  isCont (\<lambda>x. suminf (?c x) - arctan x) y"
           using DERIV_in_rball DERIV_isCont by auto
       qed
     qed