src/HOL/Limits.thy

 unfolding Bfun_def
 proof (intro exI conjI allI)
   show "0 < max K 1" by simp
 next
   show "eventually (\<lambda>x. norm (f x) \<le> max K 1) F"
-    using K by (rule eventually_elim1, simp)
+    using K by (rule eventually_mono, simp)
 qed
 
 lemma BfunE:
   assumes "Bfun f F"
   obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F"

 proof -
   from a have "0 < norm a" by simp
   with f have "eventually (\<lambda>x. dist (f x) a < norm a) F"
     by (rule tendstoD)
   then have "eventually (\<lambda>x. f x \<noteq> 0) F"
-    unfolding dist_norm by (auto elim!: eventually_elim1)
+    unfolding dist_norm by (auto elim!: eventually_mono)
   with a have "eventually (\<lambda>x. inverse (f x) - inverse a =
     - (inverse (f x) * (f x - a) * inverse a)) F"
-    by (auto elim!: eventually_elim1 simp: inverse_diff_inverse)
+    by (auto elim!: eventually_mono simp: inverse_diff_inverse)
   moreover have "Zfun (\<lambda>x. - (inverse (f x) * (f x - a) * inverse a)) F"
     by (intro Zfun_minus Zfun_mult_left
       bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]
       Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff])
   ultimately show ?thesis

 proof safe
   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 \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
-    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
+    by (auto elim!: eventually_mono simp: inverse_eq_divide field_simps)
 qed
 
 lemma tendsto_inverse_0:
   fixes x :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
   shows "(inverse ---> (0::'a)) at_infinity"

      (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
 
 lemma filterlim_inverse_at_top:
   "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
   by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
-     (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
+     (simp add: filterlim_def eventually_filtermap eventually_mono at_within_def le_principal)
 
 lemma filterlim_inverse_at_bot_neg:
   "LIM x (at_left (0::real)). inverse x :> at_bot"
   by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
 

   shows "LIM x F. (f x * g x :: real) :> at_top"
   unfolding filterlim_at_top_gt[where c=0]
 proof safe
   fix Z :: real assume "0 < Z"
   from f \<open>0 < c\<close> have "eventually (\<lambda>x. c / 2 < f x) F"
-    by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1
+    by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_mono
              simp: dist_real_def abs_real_def split: split_if_asm)
   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 \<le> f x * g x) F"
   proof eventually_elim

   shows "LIM x F. (f x + g x :: real) :> at_top"
   unfolding filterlim_at_top_gt[where c=0]
 proof safe
   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)
+    by (auto dest!: tendstoD[where e=1] elim!: eventually_mono simp: dist_real_def)
   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 \<le> f x + g x) F"
     by eventually_elim simp
 qed