src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Sep 30 16:36:42 2015 +0100
@@ -6597,8 +6597,7 @@
         then have "\<exists>N::nat. inverse (real (N + 1)) < e"
           using real_arch_inv[of e]
           apply (auto simp add: Suc_pred')
-          apply (rule_tac x="n - 1" in exI)
-          apply auto
+          apply (metis Suc_pred' real_of_nat_Suc)
           done
         then obtain N :: nat where "inverse (real (N + 1)) < e"
           by auto