diff -r 340738057c8c -r a6479cb85944 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Feb 23 15:47:39 2016 +0000
@@ -1697,15 +1697,15 @@
 also continuous. So if we know for some other reason that the inverse
 function exists, it's OK.\<close>
 
-lemma has_derivative_locally_injective:
+proposition has_derivative_locally_injective:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes "a \<in> s"
-    and "open s"
-    and "bounded_linear g'"
-    and "g' \<circ> f' a = id"
-    and "\<forall>x\<in>s. (f has_derivative f' x) (at x)"
-    and "\<forall>e>0. \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < e"
-  obtains t where "a \<in> t" "open t" "\<forall>x\<in>t. \<forall>x'\<in>t. f x' = f x \<longrightarrow> x' = x"
+      and "open s"
+      and "bounded_linear g'"
+      and "g' \<circ> f' a = id"
+      and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x)"
+      and "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < e"
+  obtains r where "r > 0" "ball a r \<subseteq> s" "inj_on f (ball a r)"
 proof -
   interpret bounded_linear g'
     using assms by auto
@@ -1738,9 +1738,11 @@
     using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
   show ?thesis
   proof
-    show "a \<in> ball a d"
-      using d by auto
-    show "\<forall>x\<in>ball a d. \<forall>x'\<in>ball a d. f x' = f x \<longrightarrow> x' = x"
+    show "0 < d" by (fact d)
+    show "ball a d \<subseteq> s"
+      using \<open>d < d2\<close> \<open>ball a d2 \<subseteq> s\<close> by auto
+    show "inj_on f (ball a d)"
+    unfolding inj_on_def
     proof (intro strip)
       fix x y
       assume as: "x \<in> ball a d" "y \<in> ball a d" "f x = f y"
@@ -1749,7 +1751,7 @@
         unfolding ph_def o_def
         unfolding diff
         using f'g'
-        by (auto simp add: algebra_simps)
+        by (auto simp: algebra_simps)
       have "norm (ph x - ph y) \<le> (1 / 2) * norm (x - y)"
         apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
         apply (rule_tac[!] ballI)
@@ -1788,7 +1790,7 @@
           using d1(2)[of u]
           using onorm_neg[where f="\<lambda>x. f' u x - f' a x"]
           using d and u and onorm_pos_le[OF assms(3)]
-          apply (auto simp add: algebra_simps)
+          apply (auto simp: algebra_simps)
           done
         also have "\<dots> \<le> 1 / 2"
           unfolding k_def by auto
@@ -1804,7 +1806,7 @@
       ultimately show "x = y"
         unfolding norm_minus_commute by auto
     qed
-  qed auto
+  qed
 qed