src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

 lemma Lim_at_infinity:
   "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
   by (auto simp add: tendsto_iff eventually_at_infinity)
 
 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
-  by (rule topological_tendstoI, auto elim: eventually_mono')
+  by (rule topological_tendstoI, auto elim: eventually_mono)
 
 text\<open>The expected monotonicity property.\<close>
 
 lemma Lim_Un:
   assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"

     then show "?rhs"
       unfolding eventually_at_topological by auto
   next
     assume "?rhs"
     then show "?lhs"
-      by (auto elim: eventually_elim1 simp: eventually_at_filter)
+      by (auto elim: eventually_mono simp: eventually_at_filter)
   }
 qed
 
 lemma at_within_interior:
   "x \<in> interior S \<Longrightarrow> at x within S = at x"

   proof (rule topological_tendstoI)
     fix S
     assume "open S" "x \<in> S"
     from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
     show "eventually (\<lambda>x. f x \<in> S) sequentially"
-      by (auto elim!: eventually_elim1)
+      by (auto elim!: eventually_mono)
   qed
   ultimately show ?rhs by fast
 next
   assume ?rhs
   then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x"

   assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g ---> 0) net"
   shows "(f ---> 0) net"
   using assms(2)
 proof (rule metric_tendsto_imp_tendsto)
   show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net"
-    using assms(1) by (rule eventually_elim1) (simp add: dist_norm)
+    using assms(1) by (rule eventually_mono) (simp add: dist_norm)
 qed
 
 lemma Lim_transform_bound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     and g :: "'a \<Rightarrow> 'c::real_normed_vector"

     assume "y \<in> closure S"
     then obtain f where f: "\<forall>n. f n \<in> S"  "(f ---> y) sequentially"
       unfolding closure_sequential by auto
     have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
     then have "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"
-      by (rule eventually_mono, simp add: f(1))
+      by (simp add: f(1))
     have "dist x y \<le> a"
       apply (rule Lim_dist_ubound [of sequentially f])
       apply (rule trivial_limit_sequentially)
       apply (rule f(2))
       apply fact

   def Z \<equiv> "closure ` {A. eventually (\<lambda>x. x \<in> A) F}"
   then have "\<forall>z\<in>Z. closed z"
     by auto
   moreover
   have ev_Z: "\<And>z. z \<in> Z \<Longrightarrow> eventually (\<lambda>x. x \<in> z) F"
-    unfolding Z_def by (auto elim: eventually_elim1 intro: set_mp[OF closure_subset])
+    unfolding Z_def by (auto elim: eventually_mono intro: set_mp[OF closure_subset])
   have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
   proof (intro allI impI)
     fix B assume "finite B" "B \<subseteq> Z"
     with \<open>finite B\<close> ev_Z F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
       by (auto simp: eventually_ball_finite_distrib eventually_conj_iff)

         done
       finally have "dist (f (r n)) l < e"
         by auto
     }
     ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
-      by (rule eventually_elim1)
+      by (rule eventually_mono)
   }
   then have *: "((f \<circ> r) ---> l) sequentially"
     unfolding o_def tendsto_iff by simp
   with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
     by auto

   then obtain T where T_def: "open T" "x0 \<in> T" "\<forall>x\<in>T. f x \<in> S"
      using assms continuous_at_open by metis
   then have "eventually (\<lambda>n. x n \<in> T) sequentially"
     using assms T_def by (auto simp: tendsto_def)
   then show "eventually (\<lambda>n. (f \<circ> x) n \<in> S) sequentially"
-    using T_def by (auto elim!: eventually_elim1)
+    using T_def by (auto elim!: eventually_mono)
 qed
 
 lemma continuous_on_open:
   "continuous_on s f \<longleftrightarrow>
     (\<forall>t. openin (subtopology euclidean (f ` s)) t \<longrightarrow>

     using assms(1) by (simp add: continuous_within)
   then have "eventually (\<lambda>y. f y \<in> U) (at x within s)"
     using \<open>open U\<close> and \<open>f x \<in> U\<close>
     unfolding tendsto_def by fast
   then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
-    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono')
+    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)
   then show ?thesis
     using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute zero_less_dist_iff eventually_at)
 qed
 
 lemma continuous_at_avoid: