# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1598538228 -3600
# Node ID bb29e4eb938de847b76521bca7d017b0c190c2d8
# Parent  0f38c96a0a743c52ce3b494a6da0fea307927b94
but not the [cong] rule

diff -r 0f38c96a0a74 -r bb29e4eb938d src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Aug 27 12:14:46 2020 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Aug 27 15:23:48 2020 +0100
@@ -4008,11 +4008,15 @@
 proof -
   have **: "((\<lambda>x. ereal (inverse x)) \<longlongrightarrow> ereal 0) at_infinity"
     by (intro tendsto_intros tendsto_inverse_0)
-
-  show ?thesis
-    by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def)
-       (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity
-             intro!: filterlim_mono_eventually[OF **])
+  then have "((\<lambda>x. if x = 0 then \<infinity> else ereal (inverse x)) \<longlongrightarrow> 0) at_top"
+  proof (rule filterlim_mono_eventually)
+    show "nhds (ereal 0) \<le> nhds 0"
+      by (simp add: zero_ereal_def)
+    show "(at_top::real filter) \<le> at_infinity"
+      by (simp add: at_top_le_at_infinity)
+  qed auto
+  then show ?thesis
+    unfolding at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def by auto
 qed
 
 lemma inverse_ereal_tendsto_pos:
diff -r 0f38c96a0a74 -r bb29e4eb938d src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Aug 27 12:14:46 2020 +0100
+++ b/src/HOL/Limits.thy	Thu Aug 27 15:23:48 2020 +0100
@@ -2178,7 +2178,7 @@
 
 text \<open>A congruence rule allowing us to transform limits assuming not at point.\<close>
 
-lemma Lim_cong_within [cong]:
+lemma Lim_cong_within:
   assumes "a = b"
     and "x = y"
     and "S = T"
diff -r 0f38c96a0a74 -r bb29e4eb938d src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Aug 27 12:14:46 2020 +0100
+++ b/src/HOL/Transcendental.thy	Thu Aug 27 15:23:48 2020 +0100
@@ -1003,7 +1003,7 @@
   have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> a 0) (at 0)"
     by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm)
   show ?thesis
-    using "*" by auto
+    using "*" by (auto cong: Lim_cong_within)
 qed