src/HOL/Transcendental.thy

       then obtain n where "x = ?s n" and "n \<in> {..<?N}"
         using image_iff[THEN iffD1] by blast
       from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF \<open>0 < ?r\<close>, unfolded real_norm_def]
       obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)"
         by auto
-      have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound)
+      have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound simp del: real_of_nat_Suc)
       thus "0 < x" unfolding \<open>x = ?s n\<close> .
     qed
   qed auto
 
   def S \<equiv> "min (min (x0 - a) (b - x0)) S'"

     qed auto
     also have "\<dots> = of_nat (card {..<?N}) * ?r"
       by (rule setsum_constant)
     also have "\<dots> = real ?N * ?r"
       unfolding real_eq_of_nat by auto
-    also have "\<dots> = r/3" by auto
+    also have "\<dots> = r/3" by (auto simp del: real_of_nat_Suc)
     finally have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
 
     from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
     have "\<bar>(suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0)\<bar> =
         \<bar>\<Sum>n. ?diff n x - f' x0 n\<bar>"

           fix n
           have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)"
             by (rule mult_left_mono) auto
           show "norm (f n * x^n) \<le> norm (f n * real (Suc n) * x^n)"
             unfolding real_norm_def abs_mult
-            by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
+            using le mult_right_mono by fastforce
         qed (rule powser_insidea[OF converges[OF \<open>R' \<in> {-R <..< R}\<close>] \<open>norm x < norm R'\<close>])
         from this[THEN summable_mult2[where c=x], unfolded mult.assoc, unfolded mult.commute]
         show "summable (?f x)" by auto
       }
       show "summable (?f' x0)"

         by (rule LIM_less_bound)
       hence "?diff 1 n \<le> ?a 1 n" by auto
     }
     have "?a 1 ----> 0"
       unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
-      by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
+      by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat simp del: real_of_nat_Suc)
     have "?diff 1 ----> 0"
     proof (rule LIMSEQ_I)
       fix r :: real
       assume "0 < r"
       obtain N :: nat where N_I: "\<And>n. N \<le> n \<Longrightarrow> ?a 1 n < r"