src/HOL/Deriv.thy

     and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0"
     and f: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV f x :> (f' x)"
     and g: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV g x :> (g' x)"
     unfolding eventually_within eventually_at by (auto simp: dist_real_def)
 
-  { fix x assume x: "0 \<le> x" "x < a"
-    from `0 \<le> x` have "isCont f x"
-      unfolding le_less
-    proof
-      assume "0 = x" with `isCont f 0` show "isCont f x" by simp
-    next
-      assume "0 < x" with f x show ?thesis by (auto intro!: DERIV_isCont)
-    qed }
-  note isCont_f = this
-
-  { fix x assume x: "0 \<le> x" "x < a"
-    from `0 \<le> x` have "isCont g x"
-      unfolding le_less
-    proof
-      assume "0 = x" with `isCont g 0` show "isCont g x" by simp
-    next
-      assume "0 < x" with g x show ?thesis by (auto intro!: DERIV_isCont)
-    qed }
-  note isCont_g = this
-
   have "\<exists>\<zeta>. \<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)"
   proof (rule bchoice, rule)
     fix x assume "x \<in> {0 <..< a}"
     then have x[arith]: "0 < x" "x < a" by auto
     with g'_neq_0 g_neq_0 `g 0 = 0` have g': "\<And>x. 0 < x \<Longrightarrow> x < a  \<Longrightarrow> 0 \<noteq> g' x" "g 0 \<noteq> g x"
       by auto
-
-    have "\<exists>c. 0 < c \<and> c < x \<and> (f x - f 0) * g' c = (g x - g 0) * f' c"
-      using isCont_f isCont_g f g `x < a` by (intro GMVT') auto
+    have "\<And>x. 0 \<le> x \<Longrightarrow> x < a \<Longrightarrow> isCont f x"
+      using `isCont f 0` f by (auto intro: DERIV_isCont simp: le_less)
+    moreover have "\<And>x. 0 \<le> x \<Longrightarrow> x < a \<Longrightarrow> isCont g x"
+      using `isCont g 0` g by (auto intro: DERIV_isCont simp: le_less)
+    ultimately have "\<exists>c. 0 < c \<and> c < x \<and> (f x - f 0) * g' c = (g x - g 0) * f' c"
+      using f g `x < a` by (intro GMVT') auto
     then guess c ..
     moreover
     with g'(1)[of c] g'(2) have "(f x - f 0)  / (g x - g 0) = f' c / g' c"
       by (simp add: field_simps)
     ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y"

   with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
     by (auto elim!: eventually_elim1 simp: filterlim_within filterlim_at)
   from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) ---> x) (at_right 0)"
     by (rule_tac filterlim_compose[of _ _ _ \<zeta>])
   ultimately show "((\<lambda>t. f t / g t) ---> x) (at_right 0)"
-    apply (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
-    apply (erule_tac eventually_elim1)
-    apply simp_all
-    done
+    by (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
+       (auto elim: eventually_elim1)
 qed
 
 lemma lhopital_right_0_at_top:
   fixes f g :: "real \<Rightarrow> real"
   assumes g_0: "LIM x at_right 0. g x :> at_top"

     and g0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV g x :> (g' x)"
     and Df: "\<And>t. 0 < t \<Longrightarrow> t < a \<Longrightarrow> dist (f' t / g' t) x < e / 4"
     unfolding eventually_within_le by (auto simp: dist_real_def)
 
   from Df have
-    "eventually (\<lambda>t. t < a) (at_right 0)"
-    "eventually (\<lambda>t::real. 0 < t) (at_right 0)"
+    "eventually (\<lambda>t. t < a) (at_right 0)" "eventually (\<lambda>t::real. 0 < t) (at_right 0)"
     unfolding eventually_within eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def)
+
   moreover
-
-  have "eventually (\<lambda>t. 0 < g t) (at_right 0)"
-    using g_0[unfolded filterlim_at_top, rule_format, of "1"] by eventually_elim auto
-
-  moreover
-
-  have "eventually (\<lambda>t. g a < g t) (at_right 0)"
-    using g_0[unfolded filterlim_at_top, rule_format, of "g a + 1"] by eventually_elim auto
+  have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)"
+    using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top)
+
   moreover
   have inv_g: "((\<lambda>x. inverse (g x)) ---> 0) (at_right 0)"
     using tendsto_inverse_0 filterlim_mono[OF g_0 at_top_le_at_infinity order_refl]
     by (rule filterlim_compose)
   then have "((\<lambda>x. norm (1 - g a * inverse (g x))) ---> norm (1 - g a * 0)) (at_right 0)"