--- 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:
--- 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"
--- 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