src/HOL/Library/Extended_Real.thy

--- a/src/HOL/Library/Extended_Real.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -3856,7 +3856,7 @@
   assumes "eventually (\<lambda>x. f x \<ge> 0) F"
   shows   "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse c) F"
   by (cases "F = bot")
-     (auto intro!: tendsto_le_const[of F] assms
+     (auto intro!: tendsto_lowerbound assms
                    continuous_on_tendsto_compose[OF continuous_on_inverse_ereal])