src/HOL/Library/Liminf_Limsup.thy

 qed
 
 lemma Liminf_eq:
   assumes "eventually (\<lambda>x. f x = g x) F"
   shows "Liminf F f = Liminf F g"
-  by (intro antisym Liminf_mono eventually_mono'[OF assms]) auto
+  by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
 
 lemma Limsup_mono:
   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
   shows "Limsup F f \<le> Limsup F g"
   unfolding Limsup_def

 qed
 
 lemma Limsup_eq:
   assumes "eventually (\<lambda>x. f x = g x) net"
   shows "Limsup net f = Limsup net g"
-  by (intro antisym Limsup_mono eventually_mono'[OF assms]) auto
+  by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
 
 lemma Liminf_le_Limsup:
   assumes ntriv: "\<not> trivial_limit F"
   shows "Liminf F f \<le> Limsup F f"
   unfolding Limsup_def Liminf_def

   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
 proof -
   have "eventually (\<lambda>x. y < X x) F"
     if "eventually P F" "y < INFIMUM (Collect P) X" for y P
-    using that by (auto elim!: eventually_elim1 dest: less_INF_D)
+    using that by (auto elim!: eventually_mono dest: less_INF_D)
   moreover
   have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
     if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
   proof (cases "\<exists>z. y < z \<and> z < C")
     case True

     proof (rule classical)
       assume "\<not> f0 \<le> y"
       then have "eventually (\<lambda>x. y < f x) F"
         using lim[THEN topological_tendstoD, of "{y <..}"] by auto
       then have "eventually (\<lambda>x. f0 \<le> f x) F"
-        using discrete by (auto elim!: eventually_elim1)
+        using discrete by (auto elim!: eventually_mono)
       then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
         by (rule upper)
       moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
         by (intro INF_greatest) simp
       ultimately show "f0 \<le> y" by simp

     proof (rule classical)
       assume "\<not> y \<le> f0"
       then have "eventually (\<lambda>x. f x < y) F"
         using lim[THEN topological_tendstoD, of "{..< y}"] by auto
       then have "eventually (\<lambda>x. f x \<le> f0) F"
-        using False by (auto elim!: eventually_elim1 simp: not_less)
+        using False by (auto elim!: eventually_mono simp: not_less)
       then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
         by (rule lower)
       moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
         by (intro SUP_least) simp
       ultimately show "y \<le> f0" by simp

   fix a assume "f0 < a"
   with assms have "Limsup F f < a" by simp
   then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
     unfolding Limsup_def INF_less_iff by auto
   then show "eventually (\<lambda>x. f x < a) F"
-    by (auto elim!: eventually_elim1 dest: SUP_lessD)
+    by (auto elim!: eventually_mono dest: SUP_lessD)
 next
   fix a assume "a < f0"
   with assms have "a < Liminf F f" by simp
   then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
     unfolding Liminf_def less_SUP_iff by auto
   then show "eventually (\<lambda>x. a < f x) F"
-    by (auto elim!: eventually_elim1 dest: less_INF_D)
+    by (auto elim!: eventually_mono dest: less_INF_D)
 qed
 
 lemma tendsto_iff_Liminf_eq_Limsup:
   fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
   shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"