add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2

--- a/src/HOL/Deriv.thy	Tue Dec 04 16:20:24 2012 +0100
+++ b/src/HOL/Deriv.thy	Tue Dec 04 18:00:31 2012 +0100
@@ -1783,7 +1783,7 @@
 
   moreover
   have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)"
-    using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top)
+    using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top_dense)
 
   moreover
   have inv_g: "((\<lambda>x. inverse (g x)) ---> 0) (at_right 0)"

--- a/src/HOL/Limits.thy	Tue Dec 04 16:20:24 2012 +0100
+++ b/src/HOL/Limits.thy	Tue Dec 04 18:00:31 2012 +0100
@@ -298,6 +298,10 @@
   then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
 qed auto
 
+lemma eventually_ge_at_top:
+  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
+  unfolding eventually_at_top_linorder by auto
+
 lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)"
   unfolding eventually_at_top_linorder
 proof safe
@@ -308,6 +312,10 @@
   ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
 qed
 
+lemma eventually_gt_at_top:
+  "eventually (\<lambda>x. (c::_::dense_linorder) < x) at_top"
+  unfolding eventually_at_top_dense by auto
+
 definition at_bot :: "('a::order) filter"
   where "at_bot = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<le>k. P n)"
 
@@ -322,6 +330,10 @@
   then show "\<exists>k. \<forall>n\<le>k. P n \<and> Q n" ..
 qed auto
 
+lemma eventually_le_at_bot:
+  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
+  unfolding eventually_at_bot_linorder by auto
+
 lemma eventually_at_bot_dense:
   fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
   unfolding eventually_at_bot_linorder
@@ -333,6 +345,10 @@
   ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])
 qed
 
+lemma eventually_gt_at_bot:
+  "eventually (\<lambda>x. x < (c::_::dense_linorder)) at_bot"
+  unfolding eventually_at_bot_dense by auto
+
 subsection {* Sequentially *}
 
 abbreviation sequentially :: "nat filter"
@@ -1193,36 +1209,115 @@
 subsection {* Limits to @{const at_top} and @{const at_bot} *}
 
 lemma filterlim_at_top:
+  fixes f :: "'a \<Rightarrow> ('b::linorder)"
+  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
+  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
+
+lemma filterlim_at_top_dense:
   fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
   shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
-  by (auto simp: filterlim_iff eventually_at_top_dense elim!: eventually_elim1)
+  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
+            filterlim_at_top[of f F] filterlim_iff[of f at_top F])
 
-lemma filterlim_at_top_gt:
-  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
-  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z < f x) F)"
+lemma filterlim_at_top_ge:
+  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
+  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
   unfolding filterlim_at_top
 proof safe
-  fix Z assume *: "\<forall>Z>c. eventually (\<lambda>x. Z < f x) F"
-  from gt_ex[of "max Z c"] guess x ..
-  with *[THEN spec, of x] show "eventually (\<lambda>x. Z < f x) F"
+  fix Z assume *: "\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F"
+  with *[THEN spec, of "max Z c"] show "eventually (\<lambda>x. Z \<le> f x) F"
     by (auto elim!: eventually_elim1)
 qed simp
 
+lemma filterlim_at_top_at_top:
+  fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
+  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
+  assumes Q: "eventually Q at_top"
+  assumes P: "eventually P at_top"
+  shows "filterlim f at_top at_top"
+proof -
+  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
+    unfolding eventually_at_top_linorder by auto
+  show ?thesis
+  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
+    fix z assume "x \<le> z"
+    with x have "P z" by auto
+    have "eventually (\<lambda>x. g z \<le> x) at_top"
+      by (rule eventually_ge_at_top)
+    with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
+      by eventually_elim (metis mono bij `P z`)
+  qed
+qed
+
+lemma filterlim_at_top_gt:
+  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
+  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
+  by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
+
 lemma filterlim_at_bot: 
-  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
-  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
-  by (auto simp: filterlim_iff eventually_at_bot_dense elim!: eventually_elim1)
+  fixes f :: "'a \<Rightarrow> ('b::linorder)"
+  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
+  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
+
+lemma filterlim_at_bot_le:
+  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
+  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
+  unfolding filterlim_at_bot
+proof safe
+  fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
+  with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
+    by (auto elim!: eventually_elim1)
+qed simp
 
 lemma filterlim_at_bot_lt:
   fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
-  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z > f x) F)"
-  unfolding filterlim_at_bot
-proof safe
-  fix Z assume *: "\<forall>Z<c. eventually (\<lambda>x. Z > f x) F"
-  from lt_ex[of "min Z c"] guess x ..
-  with *[THEN spec, of x] show "eventually (\<lambda>x. Z > f x) F"
-    by (auto elim!: eventually_elim1)
-qed simp
+  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
+  by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
+
+lemma filterlim_at_bot_at_right:
+  fixes f :: "real \<Rightarrow> 'b::linorder"
+  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
+  assumes Q: "eventually Q (at_right a)" and bound: "\<And>b. Q b \<Longrightarrow> a < b"
+  assumes P: "eventually P at_bot"
+  shows "filterlim f at_bot (at_right a)"
+proof -
+  from P obtain x where x: "\<And>y. y \<le> x \<Longrightarrow> P y"
+    unfolding eventually_at_bot_linorder by auto
+  show ?thesis
+  proof (intro filterlim_at_bot_le[THEN iffD2] allI impI)
+    fix z assume "z \<le> x"
+    with x have "P z" by auto
+    have "eventually (\<lambda>x. x \<le> g z) (at_right a)"
+      using bound[OF bij(2)[OF `P z`]]
+      by (auto simp add: eventually_within_less dist_real_def intro!:  exI[of _ "g z - a"])
+    with Q show "eventually (\<lambda>x. f x \<le> z) (at_right a)"
+      by eventually_elim (metis bij `P z` mono)
+  qed
+qed
+
+lemma filterlim_at_top_at_left:
+  fixes f :: "real \<Rightarrow> 'b::linorder"
+  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
+  assumes Q: "eventually Q (at_left a)" and bound: "\<And>b. Q b \<Longrightarrow> b < a"
+  assumes P: "eventually P at_top"
+  shows "filterlim f at_top (at_left a)"
+proof -
+  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
+    unfolding eventually_at_top_linorder by auto
+  show ?thesis
+  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
+    fix z assume "x \<le> z"
+    with x have "P z" by auto
+    have "eventually (\<lambda>x. g z \<le> x) (at_left a)"
+      using bound[OF bij(2)[OF `P z`]]
+      by (auto simp add: eventually_within_less dist_real_def intro!:  exI[of _ "a - g z"])
+    with Q show "eventually (\<lambda>x. z \<le> f x) (at_left a)"
+      by eventually_elim (metis bij `P z` mono)
+  qed
+qed
 
 lemma filterlim_at_infinity:
   fixes f :: "_ \<Rightarrow> 'a\<Colon>real_normed_vector"
@@ -1257,7 +1352,7 @@
   fix Z :: real assume [arith]: "0 < Z"
   then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
     by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
-  then show "eventually (\<lambda>x. x \<in> {0<..} \<longrightarrow> Z < inverse x) (nhds 0)"
+  then show "eventually (\<lambda>x. x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
     by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
 qed
 
@@ -1273,7 +1368,7 @@
   fix Z :: real assume [arith]: "Z < 0"
   have "eventually (\<lambda>x. inverse Z < x) (nhds 0)"
     by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
-  then show "eventually (\<lambda>x. x \<in> {..< 0} \<longrightarrow> inverse x < Z) (nhds 0)"
+  then show "eventually (\<lambda>x. x \<in> {..< 0} \<longrightarrow> inverse x \<le> Z) (nhds 0)"
     by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
 qed
 
@@ -1282,19 +1377,34 @@
   by (intro filterlim_compose[OF filterlim_inverse_at_bot_neg])
      (simp add: filterlim_def eventually_filtermap le_within_iff)
 
+lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
+  unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder
+  by (metis le_minus_iff minus_minus)
+
+lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)"
+  unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident)
+
+lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)"
+  unfolding filterlim_def at_top_mirror filtermap_filtermap ..
+
+lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \<longleftrightarrow> (LIM x at_top. f (-x::real) :> F)"
+  unfolding filterlim_def at_bot_mirror filtermap_filtermap ..
+
 lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
   unfolding filterlim_at_top eventually_at_bot_dense
-  by (blast intro: less_minus_iff[THEN iffD1])
-
-lemma filterlim_uminus_at_top: "LIM x F. f x :> at_bot \<Longrightarrow> LIM x F. - (f x) :: real :> at_top"
-  by (rule filterlim_compose[OF filterlim_uminus_at_top_at_bot])
+  by (metis leI minus_less_iff order_less_asym)
 
 lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
   unfolding filterlim_at_bot eventually_at_top_dense
-  by (blast intro: minus_less_iff[THEN iffD1])
+  by (metis leI less_minus_iff order_less_asym)
 
-lemma filterlim_uminus_at_bot: "LIM x F. f x :> at_top \<Longrightarrow> LIM x F. - (f x) :: real :> at_bot"
-  by (rule filterlim_compose[OF filterlim_uminus_at_bot_at_top])
+lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_bot)"
+  using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F]
+  using filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
+  by auto
+
+lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_top)"
+  unfolding filterlim_uminus_at_top by simp
 
 lemma tendsto_inverse_0:
   fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra"
@@ -1362,14 +1472,14 @@
   from f `0 < c` have "eventually (\<lambda>x. c / 2 < f x) F"
     by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1
              simp: dist_real_def abs_real_def split: split_if_asm)
-  moreover from g have "eventually (\<lambda>x. (Z / c * 2) < g x) F"
+  moreover from g have "eventually (\<lambda>x. (Z / c * 2) \<le> g x) F"
     unfolding filterlim_at_top by auto
-  ultimately show "eventually (\<lambda>x. Z < f x * g x) F"
+  ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F"
   proof eventually_elim
-    fix x assume "c / 2 < f x" "Z / c * 2 < g x"
-    with `0 < Z` `0 < c` have "c / 2 * (Z / c * 2) < f x * g x"
-      by (intro mult_strict_mono) (auto simp: zero_le_divide_iff)
-    with `0 < c` show "Z < f x * g x"
+    fix x assume "c / 2 < f x" "Z / c * 2 \<le> g x"
+    with `0 < Z` `0 < c` have "c / 2 * (Z / c * 2) \<le> f x * g x"
+      by (intro mult_mono) (auto simp: zero_le_divide_iff)
+    with `0 < c` show "Z \<le> f x * g x"
        by simp
   qed
 qed
@@ -1381,16 +1491,16 @@
   unfolding filterlim_at_top_gt[where c=0]
 proof safe
   fix Z :: real assume "0 < Z"
-  from f have "eventually (\<lambda>x. 1 < f x) F"
+  from f have "eventually (\<lambda>x. 1 \<le> f x) F"
     unfolding filterlim_at_top by auto
-  moreover from g have "eventually (\<lambda>x. Z < g x) F"
+  moreover from g have "eventually (\<lambda>x. Z \<le> g x) F"
     unfolding filterlim_at_top by auto
-  ultimately show "eventually (\<lambda>x. Z < f x * g x) F"
+  ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F"
   proof eventually_elim
-    fix x assume "1 < f x" "Z < g x"
-    with `0 < Z` have "1 * Z < f x * g x"
-      by (intro mult_strict_mono) (auto simp: zero_le_divide_iff)
-    then show "Z < f x * g x"
+    fix x assume "1 \<le> f x" "Z \<le> g x"
+    with `0 < Z` have "1 * Z \<le> f x * g x"
+      by (intro mult_mono) (auto simp: zero_le_divide_iff)
+    then show "Z \<le> f x * g x"
        by simp
   qed
 qed
@@ -1404,9 +1514,9 @@
   fix Z :: real assume "0 < Z"
   from f have "eventually (\<lambda>x. c - 1 < f x) F"
     by (auto dest!: tendstoD[where e=1] elim!: eventually_elim1 simp: dist_real_def)
-  moreover from g have "eventually (\<lambda>x. Z - (c - 1) < g x) F"
+  moreover from g have "eventually (\<lambda>x. Z - (c - 1) \<le> g x) F"
     unfolding filterlim_at_top by auto
-  ultimately show "eventually (\<lambda>x. Z < f x + g x) F"
+  ultimately show "eventually (\<lambda>x. Z \<le> f x + g x) F"
     by eventually_elim simp
 qed
 
@@ -1417,11 +1527,11 @@
   unfolding filterlim_at_top_gt[where c=0]
 proof safe
   fix Z :: real assume "0 < Z"
-  from f have "eventually (\<lambda>x. 0 < f x) F"
+  from f have "eventually (\<lambda>x. 0 \<le> f x) F"
     unfolding filterlim_at_top by auto
-  moreover from g have "eventually (\<lambda>x. Z < g x) F"
+  moreover from g have "eventually (\<lambda>x. Z \<le> g x) F"
     unfolding filterlim_at_top by auto
-  ultimately show "eventually (\<lambda>x. Z < f x + g x) F"
+  ultimately show "eventually (\<lambda>x. Z \<le> f x + g x) F"
     by eventually_elim simp
 qed
 

--- a/src/HOL/Log.thy	Tue Dec 04 16:20:24 2012 +0100
+++ b/src/HOL/Log.thy	Tue Dec 04 18:00:31 2012 +0100
@@ -364,7 +364,8 @@
 proof (rule tendstoI)
   fix e :: real assume "0 < e"
   def Z \<equiv> "e powr (1 / s)"
-  from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: filterlim_at_top)
+  from assms have "eventually (\<lambda>x. Z < f x) F"
+    by (simp add: filterlim_at_top_dense)
   moreover
   from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
     by (auto simp: Z_def intro!: powr_less_mono2_neg)

--- a/src/HOL/Transcendental.thy	Tue Dec 04 16:20:24 2012 +0100
+++ b/src/HOL/Transcendental.thy	Tue Dec 04 18:00:31 2012 +0100
@@ -1328,39 +1328,16 @@
 qed
 
 lemma exp_at_top: "LIM x at_top. exp x :: real :> at_top"
-proof -
-  { fix r n :: real assume "r < n"
-    also have "n < 1 + n" by simp
-    also have "1 + n \<le> exp n" by (rule exp_ge_add_one_self)
-    finally have "r < exp n" . }
-  then show ?thesis
-    by (auto simp: eventually_at_top_dense filterlim_at_top)
-qed
+  by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
+     (auto intro: eventually_gt_at_top)
 
 lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
-  unfolding filterlim_at_bot
-proof safe
-  fix r :: real
-  { fix x :: real assume "0 < x" "x < exp r"
-    then have "ln x < ln (exp r)"
-      by (subst ln_less_cancel_iff) auto
-    then have "ln x < r" by simp }
-  then show "eventually (\<lambda>x. ln x < r) (at_right 0)"
-    by (auto simp add: dist_real_def eventually_within eventually_at intro!: exI[of _ "exp r"])
-qed
+  by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
+     (auto simp: eventually_within)
 
 lemma ln_at_top: "LIM x at_top. ln x :> at_top"
-  unfolding filterlim_at_top
-proof safe
-  fix r :: real
-  { fix x assume "exp r < x"
-    with exp_gt_zero[of r] have "ln (exp r) < ln x"
-      by (subst ln_less_cancel_iff) (auto simp del: exp_gt_zero)
-    then have "r < ln x"
-      by simp }
-  then show "eventually (\<lambda>x. r < ln x) at_top"
-    by (auto simp add: eventually_at_top_dense)
-qed
+  by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
+     (auto intro: eventually_gt_at_top)
 
 subsection {* Sine and Cosine *}
 
@@ -2481,6 +2458,39 @@
   DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
 
+lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
+  by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
+     (auto simp: le_less eventually_within_less dist_real_def simp del: less_divide_eq_numeral1
+           intro!: tan_monotone exI[of _ "pi/2"])
+
+lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
+  by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
+     (auto simp: le_less eventually_within_less dist_real_def simp del: less_divide_eq_numeral1
+           intro!: tan_monotone exI[of _ "pi/2"])
+
+lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
+proof (rule tendstoI)
+  fix e :: real assume "0 < e"
+  def y \<equiv> "pi/2 - min (pi/2) e"
+  then have y: "0 \<le> y" "y < pi/2" "pi/2 \<le> e + y"
+    using `0 < e` by auto
+
+  show "eventually (\<lambda>x. dist (arctan x) (pi / 2) < e) at_top"
+  proof (intro eventually_at_top_dense[THEN iffD2] exI allI impI)
+    fix x assume "tan y < x"
+    then have "arctan (tan y) < arctan x"
+      by (simp add: arctan_less_iff)
+    with y have "y < arctan x"
+      by (subst (asm) arctan_tan) simp_all
+    with arctan_ubound[of x, arith] y `0 < e`
+    show "dist (arctan x) (pi / 2) < e"
+      by (simp add: dist_real_def)
+  qed
+qed
+
+lemma tendsto_arctan_at_bot: "(arctan ---> - (pi/2)) at_bot"
+  unfolding filterlim_at_bot_mirror arctan_minus by (intro tendsto_minus tendsto_arctan_at_top)
+
 subsection {* More Theorems about Sin and Cos *}
 
 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"