reduce imports of Derivative, inverse function theorem as application of Brouwer draft
authorimmler
Wed, 28 Aug 2019 00:08:14 +0200
changeset 70809 ffdb0de54d53
parent 70808 191bb458b95c
reduce imports of Derivative, inverse function theorem as application of Brouwer
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -19,6 +19,7 @@
     Path_Connected
     Homeomorphism
     Continuous_Extension
+    Derivative
 begin
 
 subsection \<open>Retractions\<close>
@@ -4936,4 +4937,249 @@
   shows "connected(-S)"
   using assms path_connected_complement_homeomorphic_interval path_connected_imp_connected by blast
 
+subsubsection \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
+
+lemma brouwer_surjective:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "compact T"
+    and "convex T"
+    and "T \<noteq> {}"
+    and "continuous_on T f"
+    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
+    and "x \<in> S"
+  shows "\<exists>y\<in>T. f y = x"
+proof -
+  have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
+    by (auto simp add: algebra_simps)
+  show ?thesis
+    unfolding *
+    apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
+    apply (intro continuous_intros)
+    using assms
+    apply auto
+    done
+qed
+
+lemma brouwer_surjective_cball:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "continuous_on (cball a e) f"
+    and "e > 0"
+    and "x \<in> S"
+    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
+  shows "\<exists>y\<in>cball a e. f y = x"
+  apply (rule brouwer_surjective)
+  apply (rule compact_cball convex_cball)+
+  unfolding cball_eq_empty
+  using assms
+  apply auto
+  done
+
+subsubsection \<open>Inverse function theorem\<close>
+
+text \<open>See Sussmann: "Multidifferential calculus", Theorem 2.1.1\<close>
+
+lemma sussmann_open_mapping:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+  assumes "open S"
+    and contf: "continuous_on S f"
+    and "x \<in> S"
+    and derf: "(f has_derivative f') (at x)"
+    and "bounded_linear g'" "f' \<circ> g' = id"
+    and "T \<subseteq> S"
+    and x: "x \<in> interior T"
+  shows "f x \<in> interior (f ` T)"
+proof -
+  interpret f': bounded_linear f'
+    using assms unfolding has_derivative_def by auto
+  interpret g': bounded_linear g'
+    using assms by auto
+  obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
+    using bounded_linear.pos_bounded[OF assms(5)] by blast
+  hence *: "1 / (2 * B) > 0" by auto
+  obtain e0 where e0:
+      "0 < e0"
+      "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
+    using derf unfolding has_derivative_at_alt
+    using * by blast
+  obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
+    using mem_interior_cball x by blast
+  have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
+  obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
+    using field_lbound_gt_zero[OF *] by blast
+  have lem: "\<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" if "z\<in>cball (f x) (e / 2)" for z
+  proof (rule brouwer_surjective_cball)
+    have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
+    proof-
+      have "dist x z = norm (g' (f x) - g' y)"
+        unfolding as(2) and dist_norm by auto
+      also have "\<dots> \<le> norm (f x - y) * B"
+        by (metis B(2) g'.diff)
+      also have "\<dots> \<le> e * B"
+        by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1))
+      also have "\<dots> \<le> e1"
+        using B(1) e(3) pos_less_divide_eq by fastforce
+      finally have "z \<in> cball x e1"
+        by force
+      then show "z \<in> S"
+        using e1 assms(7) by auto
+    qed
+    show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
+      unfolding g'.diff
+    proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f])
+      show "continuous_on ((\<lambda>y. x + (g' y - g' (f x))) ` cball (f x) e) f"
+        by (rule continuous_on_subset[OF contf]) (use z in blast)
+      show "continuous_on (cball (f x) e) (\<lambda>y. x + (g' y - g' (f x)))"
+        by (intro continuous_intros linear_continuous_on[OF \<open>bounded_linear g'\<close>])
+    qed
+  next
+    fix y z
+    assume y: "y \<in> cball (f x) (e / 2)" and z: "z \<in> cball (f x) e"
+    have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
+      using B by auto
+    also have "\<dots> \<le> e * B"
+      by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1)
+    also have "\<dots> < e0"
+      using B(1) e(2) pos_less_divide_eq by blast
+    finally have *: "norm (x + g' (z - f x) - x) < e0"
+      by auto
+    have **: "f x + f' (x + g' (z - f x) - x) = z"
+      using assms(6)[unfolded o_def id_def,THEN cong]
+      by auto
+    have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
+          norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
+      using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
+      by (auto simp add: algebra_simps)
+    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
+      using e0(2)[rule_format, OF *]
+      by (simp only: algebra_simps **) auto
+    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
+      using y by (auto simp: dist_norm)
+    also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
+      using * B by (auto simp add: field_simps)
+    also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
+      by auto
+    also have "\<dots> \<le> e/2 + e/2"
+      using B(1) \<open>norm (z - f x) * B \<le> e * B\<close> by auto
+    finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
+      by (auto simp: dist_norm)
+  qed (use e that in auto) 
+  show ?thesis
+    unfolding mem_interior
+  proof (intro exI conjI subsetI)
+    fix y
+    assume "y \<in> ball (f x) (e / 2)"
+    then have *: "y \<in> cball (f x) (e / 2)"
+      by auto
+    obtain z where z: "z \<in> cball (f x) e" "f (x + g' (z - f x)) = y"
+      using lem * by blast
+    then have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
+      using B
+      by (auto simp add: field_simps)
+    also have "\<dots> \<le> e * B"
+      by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1))
+    also have "\<dots> \<le> e1"
+      using e B unfolding less_divide_eq by auto
+    finally have "x + g'(z - f x) \<in> T"
+      by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq)
+    then show "y \<in> f ` T"
+      using z by auto
+  qed (use e in auto)
+qed
+
+text \<open>Hence the following eccentric variant of the inverse function theorem.
+  This has no continuity assumptions, but we do need the inverse function.
+  We could put \<open>f' \<circ> g = I\<close> but this happens to fit with the minimal linear
+  algebra theory I've set up so far.\<close>
+
+lemma has_derivative_inverse_strong:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "open S"
+    and "x \<in> S"
+    and contf: "continuous_on S f"
+    and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+    and derf: "(f has_derivative f') (at x)"
+    and id: "f' \<circ> g' = id"
+  shows "(g has_derivative g') (at (f x))"
+proof -
+  have linf: "bounded_linear f'"
+    using derf unfolding has_derivative_def by auto
+  then have ling: "bounded_linear g'"
+    unfolding linear_conv_bounded_linear[symmetric]
+    using id right_inverse_linear by blast
+  moreover have "g' \<circ> f' = id"
+    using id linf ling
+    unfolding linear_conv_bounded_linear[symmetric]
+    using linear_inverse_left
+    by auto
+  moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
+    apply (rule sussmann_open_mapping)
+    apply (rule assms ling)+
+    apply auto
+    done
+  have "continuous (at (f x)) g"
+    unfolding continuous_at Lim_at
+  proof (rule, rule)
+    fix e :: real
+    assume "e > 0"
+    then have "f x \<in> interior (f ` (ball x e \<inter> S))"
+      using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
+      by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
+    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
+      unfolding mem_interior by blast
+    show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
+    proof (intro exI allI impI conjI)
+      fix y
+      assume "0 < dist y (f x) \<and> dist y (f x) < d"
+      then have "g y \<in> g ` f ` (ball x e \<inter> S)"
+        by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
+      then show "dist (g y) (g (f x)) < e"
+        using gf[OF \<open>x \<in> S\<close>]
+        by (simp add: assms(4) dist_commute image_iff)
+    qed (use d in auto)
+  qed
+  moreover have "f x \<in> interior (f ` S)"
+    apply (rule sussmann_open_mapping)
+    apply (rule assms ling)+
+    using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
+    apply auto
+    done
+  moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
+    by (metis gf imageE interiorE subsetD that)
+  ultimately show ?thesis using assms
+    by (metis has_derivative_inverse_basic_x open_interior)
+qed
+
+text \<open>A rewrite based on the other domain.\<close>
+
+lemma has_derivative_inverse_strong_x:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+  assumes "open S"
+    and "g y \<in> S"
+    and "continuous_on S f"
+    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+    and "(f has_derivative f') (at (g y))"
+    and "f' \<circ> g' = id"
+    and "f (g y) = y"
+  shows "(g has_derivative g') (at y)"
+  using has_derivative_inverse_strong[OF assms(1-6)]
+  unfolding assms(7)
+  by simp
+
+text \<open>On a region.\<close>
+
+theorem has_derivative_inverse_on:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "open S"
+    and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
+    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+    and "f' x \<circ> g' x = id"
+    and "x \<in> S"
+  shows "(g has_derivative g'(x)) (at (f x))"
+proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
+  show "continuous_on S f"
+  unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
+  using derf has_derivative_continuous by blast
+qed (use assms in auto)
+
+
 end
--- a/src/HOL/Analysis/Derivative.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -6,7 +6,11 @@
 section \<open>Derivative\<close>
 
 theory Derivative
-imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
+  imports
+    Path_Connected
+    Operator_Norm
+    Uniform_Limit
+    Bounded_Linear_Function
 begin
 
 declare bounded_linear_inner_left [intro]
@@ -1203,251 +1207,6 @@
 qed
 
 
-subsection \<open>Inverse function theorem\<close>
-
-text \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
-
-lemma brouwer_surjective:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "compact T"
-    and "convex T"
-    and "T \<noteq> {}"
-    and "continuous_on T f"
-    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
-    and "x \<in> S"
-  shows "\<exists>y\<in>T. f y = x"
-proof -
-  have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
-    by (auto simp add: algebra_simps)
-  show ?thesis
-    unfolding *
-    apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
-    apply (intro continuous_intros)
-    using assms
-    apply auto
-    done
-qed
-
-lemma brouwer_surjective_cball:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "continuous_on (cball a e) f"
-    and "e > 0"
-    and "x \<in> S"
-    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
-  shows "\<exists>y\<in>cball a e. f y = x"
-  apply (rule brouwer_surjective)
-  apply (rule compact_cball convex_cball)+
-  unfolding cball_eq_empty
-  using assms
-  apply auto
-  done
-
-text \<open>See Sussmann: "Multidifferential calculus", Theorem 2.1.1\<close>
-
-lemma sussmann_open_mapping:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
-  assumes "open S"
-    and contf: "continuous_on S f"
-    and "x \<in> S"
-    and derf: "(f has_derivative f') (at x)"
-    and "bounded_linear g'" "f' \<circ> g' = id"
-    and "T \<subseteq> S"
-    and x: "x \<in> interior T"
-  shows "f x \<in> interior (f ` T)"
-proof -
-  interpret f': bounded_linear f'
-    using assms unfolding has_derivative_def by auto
-  interpret g': bounded_linear g'
-    using assms by auto
-  obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
-    using bounded_linear.pos_bounded[OF assms(5)] by blast
-  hence *: "1 / (2 * B) > 0" by auto
-  obtain e0 where e0:
-      "0 < e0"
-      "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
-    using derf unfolding has_derivative_at_alt
-    using * by blast
-  obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
-    using mem_interior_cball x by blast
-  have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
-  obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
-    using field_lbound_gt_zero[OF *] by blast
-  have lem: "\<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" if "z\<in>cball (f x) (e / 2)" for z
-  proof (rule brouwer_surjective_cball)
-    have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
-    proof-
-      have "dist x z = norm (g' (f x) - g' y)"
-        unfolding as(2) and dist_norm by auto
-      also have "\<dots> \<le> norm (f x - y) * B"
-        by (metis B(2) g'.diff)
-      also have "\<dots> \<le> e * B"
-        by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1))
-      also have "\<dots> \<le> e1"
-        using B(1) e(3) pos_less_divide_eq by fastforce
-      finally have "z \<in> cball x e1"
-        by force
-      then show "z \<in> S"
-        using e1 assms(7) by auto
-    qed
-    show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
-      unfolding g'.diff
-    proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f])
-      show "continuous_on ((\<lambda>y. x + (g' y - g' (f x))) ` cball (f x) e) f"
-        by (rule continuous_on_subset[OF contf]) (use z in blast)
-      show "continuous_on (cball (f x) e) (\<lambda>y. x + (g' y - g' (f x)))"
-        by (intro continuous_intros linear_continuous_on[OF \<open>bounded_linear g'\<close>])
-    qed
-  next
-    fix y z
-    assume y: "y \<in> cball (f x) (e / 2)" and z: "z \<in> cball (f x) e"
-    have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
-      using B by auto
-    also have "\<dots> \<le> e * B"
-      by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1)
-    also have "\<dots> < e0"
-      using B(1) e(2) pos_less_divide_eq by blast
-    finally have *: "norm (x + g' (z - f x) - x) < e0"
-      by auto
-    have **: "f x + f' (x + g' (z - f x) - x) = z"
-      using assms(6)[unfolded o_def id_def,THEN cong]
-      by auto
-    have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
-          norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
-      using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
-      by (auto simp add: algebra_simps)
-    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
-      using e0(2)[rule_format, OF *]
-      by (simp only: algebra_simps **) auto
-    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
-      using y by (auto simp: dist_norm)
-    also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
-      using * B by (auto simp add: field_simps)
-    also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
-      by auto
-    also have "\<dots> \<le> e/2 + e/2"
-      using B(1) \<open>norm (z - f x) * B \<le> e * B\<close> by auto
-    finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
-      by (auto simp: dist_norm)
-  qed (use e that in auto) 
-  show ?thesis
-    unfolding mem_interior
-  proof (intro exI conjI subsetI)
-    fix y
-    assume "y \<in> ball (f x) (e / 2)"
-    then have *: "y \<in> cball (f x) (e / 2)"
-      by auto
-    obtain z where z: "z \<in> cball (f x) e" "f (x + g' (z - f x)) = y"
-      using lem * by blast
-    then have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
-      using B
-      by (auto simp add: field_simps)
-    also have "\<dots> \<le> e * B"
-      by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1))
-    also have "\<dots> \<le> e1"
-      using e B unfolding less_divide_eq by auto
-    finally have "x + g'(z - f x) \<in> T"
-      by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq)
-    then show "y \<in> f ` T"
-      using z by auto
-  qed (use e in auto)
-qed
-
-text \<open>Hence the following eccentric variant of the inverse function theorem.
-  This has no continuity assumptions, but we do need the inverse function.
-  We could put \<open>f' \<circ> g = I\<close> but this happens to fit with the minimal linear
-  algebra theory I've set up so far.\<close>
-
-lemma has_derivative_inverse_strong:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "open S"
-    and "x \<in> S"
-    and contf: "continuous_on S f"
-    and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
-    and derf: "(f has_derivative f') (at x)"
-    and id: "f' \<circ> g' = id"
-  shows "(g has_derivative g') (at (f x))"
-proof -
-  have linf: "bounded_linear f'"
-    using derf unfolding has_derivative_def by auto
-  then have ling: "bounded_linear g'"
-    unfolding linear_conv_bounded_linear[symmetric]
-    using id right_inverse_linear by blast
-  moreover have "g' \<circ> f' = id"
-    using id linf ling
-    unfolding linear_conv_bounded_linear[symmetric]
-    using linear_inverse_left
-    by auto
-  moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
-    apply (rule sussmann_open_mapping)
-    apply (rule assms ling)+
-    apply auto
-    done
-  have "continuous (at (f x)) g"
-    unfolding continuous_at Lim_at
-  proof (rule, rule)
-    fix e :: real
-    assume "e > 0"
-    then have "f x \<in> interior (f ` (ball x e \<inter> S))"
-      using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
-      by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
-    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
-      unfolding mem_interior by blast
-    show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
-    proof (intro exI allI impI conjI)
-      fix y
-      assume "0 < dist y (f x) \<and> dist y (f x) < d"
-      then have "g y \<in> g ` f ` (ball x e \<inter> S)"
-        by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
-      then show "dist (g y) (g (f x)) < e"
-        using gf[OF \<open>x \<in> S\<close>]
-        by (simp add: assms(4) dist_commute image_iff)
-    qed (use d in auto)
-  qed
-  moreover have "f x \<in> interior (f ` S)"
-    apply (rule sussmann_open_mapping)
-    apply (rule assms ling)+
-    using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
-    apply auto
-    done
-  moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
-    by (metis gf imageE interiorE subsetD that)
-  ultimately show ?thesis using assms
-    by (metis has_derivative_inverse_basic_x open_interior)
-qed
-
-text \<open>A rewrite based on the other domain.\<close>
-
-lemma has_derivative_inverse_strong_x:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
-  assumes "open S"
-    and "g y \<in> S"
-    and "continuous_on S f"
-    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
-    and "(f has_derivative f') (at (g y))"
-    and "f' \<circ> g' = id"
-    and "f (g y) = y"
-  shows "(g has_derivative g') (at y)"
-  using has_derivative_inverse_strong[OF assms(1-6)]
-  unfolding assms(7)
-  by simp
-
-text \<open>On a region.\<close>
-
-theorem has_derivative_inverse_on:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "open S"
-    and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
-    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
-    and "f' x \<circ> g' x = id"
-    and "x \<in> S"
-  shows "(g has_derivative g'(x)) (at (f x))"
-proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
-  show "continuous_on S f"
-  unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
-  using derf has_derivative_continuous by blast
-qed (use assms in auto)
-
-
 text \<open>Invertible derivative continuous at a point implies local
 injectivity. It's only for this we need continuity of the derivative,
 except of course if we want the fact that the inverse derivative is