src/HOL/Deriv.thy

 
 subsection \<open>Composition\<close>
 
 lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \<Longrightarrow> (f ---> y) (at x within s) \<longleftrightarrow> (f ---> y) (inf (nhds x) (principal s))"
   unfolding tendsto_def eventually_inf_principal eventually_at_filter
-  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
+  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
 
 lemma has_derivative_in_compose:
   assumes f: "(f has_derivative f') (at x within s)"
   assumes g: "(g has_derivative g') (at (f x) within (f`s))"
   shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"

 proof (rule filterlim_cong)
   assume *: "eventually (\<lambda>x. f x = g x) (nhds x)"
   moreover from * have "f x = g x" by (auto simp: eventually_nhds)
   moreover assume "x = y" "u = v"
   ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
-    by (auto simp: eventually_at_filter elim: eventually_elim1)
+    by (auto simp: eventually_at_filter elim: eventually_mono)
 qed simp_all
 
 lemma DERIV_shift:
   "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
   by (simp add: DERIV_def field_simps)

   then have "((\<lambda>x. norm (\<zeta> x)) ---> 0) (at_right 0)"
     by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"]) auto
   then have "(\<zeta> ---> 0) (at_right 0)"
     by (rule tendsto_norm_zero_cancel)
   with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
-    by (auto elim!: eventually_elim1 simp: filterlim_at)
+    by (auto elim!: eventually_mono simp: filterlim_at)
   from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) ---> x) (at_right 0)"
     by (rule_tac filterlim_compose[of _ _ _ \<zeta>])
   ultimately have "((\<lambda>t. f t / g t) ---> x) (at_right 0)" (is ?P)
     by (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
-       (auto elim: eventually_elim1)
+       (auto elim: eventually_mono)
   also have "?P \<longleftrightarrow> ?thesis"
     by (rule filterlim_cong) (auto simp: f_def g_def eventually_at_filter)
   finally show ?thesis .
 qed
 

     "eventually (\<lambda>t. t < a) (at_right 0)" "eventually (\<lambda>t::real. 0 < t) (at_right 0)"
     unfolding eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def)
 
   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_dense)
+    using g_0 by (auto elim: eventually_mono simp: filterlim_at_top_dense)
 
   moreover
   have inv_g: "((\<lambda>x. inverse (g x)) ---> 0) (at_right 0)"
     using tendsto_inverse_0 filterlim_mono[OF g_0 at_top_le_at_infinity order_refl]
     by (rule filterlim_compose)

     by (intro tendsto_intros)
   then have "((\<lambda>x. norm (1 - g a / g x)) ---> 1) (at_right 0)"
     by (simp add: inverse_eq_divide)
   from this[unfolded tendsto_iff, rule_format, of 1]
   have "eventually (\<lambda>x. norm (1 - g a / g x) < 2) (at_right 0)"
-    by (auto elim!: eventually_elim1 simp: dist_real_def)
+    by (auto elim!: eventually_mono simp: dist_real_def)
 
   moreover
   from inv_g have "((\<lambda>t. norm ((f a - x * g a) * inverse (g t))) ---> norm ((f a - x * g a) * 0)) (at_right 0)"
     by (intro tendsto_intros)
   then have "((\<lambda>t. norm (f a - x * g a) / norm (g t)) ---> 0) (at_right 0)"