diff -r 91da58bb560d -r c2128ab11f61 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Thu Oct 19 17:16:01 2017 +0100
@@ -2318,9 +2318,9 @@
 proof (clarsimp simp add: continuous_openin_preimage_eq)
   fix T :: "'a set"
   assume "open T"
-  have eq: "{x. x \<in> f ` S \<and> g x \<in> T} = f ` (S \<inter> T)"
+  have eq: "f ` S \<inter> g -` T = f ` (S \<inter> T)"
     by (auto simp: gf)
-  show "openin (subtopology euclidean (f ` S)) {x \<in> f ` S. g x \<in> T}"
+  show "openin (subtopology euclidean (f ` S)) (f ` S \<inter> g -` T)"
     apply (subst eq)
     apply (rule open_openin_trans)
       apply (rule invariance_of_domain_gen)
@@ -3173,7 +3173,7 @@
   have zn2: "(\<lambda>z::complex. z^n) ` (- {0}) = - {0}"
     using assms by (auto simp: image_def elim: exists_complex_root_nonzero [where n = n])
   have zn3: "\<exists>T. z^n \<in> T \<and> open T \<and> 0 \<notin> T \<and>
-               (\<exists>v. \<Union>v = {x. x \<noteq> 0 \<and> x^n \<in> T} \<and>
+               (\<exists>v. \<Union>v = -{0} \<inter> (\<lambda>z. z ^ n) -` T \<and>
                     (\<forall>u\<in>v. open u \<and> 0 \<notin> u) \<and>
                     pairwise disjnt v \<and>
                     (\<forall>u\<in>v. Ex (homeomorphism u T (\<lambda>z. z^n))))"
@@ -3216,8 +3216,6 @@
       by (intro continuous_intros)
     have noncon: "\<not> (\<lambda>w::complex. w^n) constant_on UNIV"
       by (metis UNIV_I assms constant_on_def power_one zero_neq_one zero_power)
-    have open_imball: "open ((\<lambda>w. w^n) ` ball z d)"
-      by (rule invariance_of_domain [OF cont open_ball inj])
     have im_eq: "(\<lambda>w. w^n) ` ball z' d = (\<lambda>w. w^n) ` ball z d"
                 if z': "z'^n = z^n" for z'
     proof -
@@ -3262,6 +3260,7 @@
       qed
       then show ?thesis by blast
     qed
+
     have ex_ball: "\<exists>B. (\<exists>z'. B = ball z' d \<and> z'^n = z^n) \<and> x \<in> B"
                   if "x \<noteq> 0" and eq: "x^n = w^n" and dzw: "dist z w < d" for x w
     proof -
@@ -3286,50 +3285,63 @@
         apply (simp add: dist_norm)
         done
     qed
-    have ball1: "\<Union>{ball z' d |z'. z'^n = z^n} = {x. x \<noteq> 0 \<and> x^n \<in> (\<lambda>w. w^n) ` ball z d}"
-      apply (rule equalityI)
-       prefer 2 apply (force simp: ex_ball, clarsimp)
-      apply (subst im_eq [symmetric], assumption)
-      using assms
-      apply (force simp: dist_norm d_def min_mult_distrib_right dest: power_eq_imp_eq_norm)
-      done
-    have ball2: "pairwise disjnt {ball z' d |z'. z'^n = z^n}"
-    proof (clarsimp simp add: pairwise_def disjnt_iff)
-      fix \<xi> \<zeta> x
-      assume "\<xi>^n = z^n" "\<zeta>^n = z^n" "ball \<xi> d \<noteq> ball \<zeta> d"
-         and "dist \<xi> x < d" "dist \<zeta> x < d"
-      then have "dist \<xi> \<zeta> < d+d"
-        using dist_triangle_less_add by blast
-      then have "cmod (\<xi> - \<zeta>) < 2*d"
-        by (simp add: dist_norm)
-      also have "... \<le> e * cmod z"
-        using mult_right_mono \<open>0 < e\<close> that by (auto simp: d_def)
-      finally have "cmod (\<xi> - \<zeta>) < e * cmod z" .
-      with e have "\<xi> = \<zeta>"
-        by (metis \<open>\<xi>^n = z^n\<close> \<open>\<zeta>^n = z^n\<close> assms power_eq_imp_eq_norm)
-      then show "False"
-        using \<open>ball \<xi> d \<noteq> ball \<zeta> d\<close> by blast
+
+    show ?thesis
+    proof (rule exI, intro conjI)
+      show "z ^ n \<in> (\<lambda>w. w ^ n) ` ball z d"
+        using \<open>d > 0\<close> by simp
+      show "open ((\<lambda>w. w ^ n) ` ball z d)"
+        by (rule invariance_of_domain [OF cont open_ball inj])
+      show "0 \<notin> (\<lambda>w. w ^ n) ` ball z d"
+        using \<open>z \<noteq> 0\<close> assms by (force simp: d_def)
+      show "\<exists>v. \<Union>v = - {0} \<inter> (\<lambda>z. z ^ n) -` (\<lambda>w. w ^ n) ` ball z d \<and>
+                (\<forall>u\<in>v. open u \<and> 0 \<notin> u) \<and>
+                disjoint v \<and>
+                (\<forall>u\<in>v. Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n)))"
+      proof (rule exI, intro ballI conjI)
+        show "\<Union>{ball z' d |z'. z'^n = z^n} = - {0} \<inter> (\<lambda>z. z ^ n) -` (\<lambda>w. w ^ n) ` ball z d" (is "?l = ?r")
+        proof 
+          show "?l \<subseteq> ?r"
+            apply auto
+             apply (simp add: assms d_def power_eq_imp_eq_norm that)
+            by (metis im_eq image_eqI mem_ball)
+          show "?r \<subseteq> ?l"
+            by auto (meson ex_ball)
+        qed
+        show "\<And>u. u \<in> {ball z' d |z'. z' ^ n = z ^ n} \<Longrightarrow> 0 \<notin> u"
+          by (force simp add: assms d_def power_eq_imp_eq_norm that)
+
+        show "disjoint {ball z' d |z'. z' ^ n = z ^ n}"
+        proof (clarsimp simp add: pairwise_def disjnt_iff)
+          fix \<xi> \<zeta> x
+          assume "\<xi>^n = z^n" "\<zeta>^n = z^n" "ball \<xi> d \<noteq> ball \<zeta> d"
+            and "dist \<xi> x < d" "dist \<zeta> x < d"
+          then have "dist \<xi> \<zeta> < d+d"
+            using dist_triangle_less_add by blast
+          then have "cmod (\<xi> - \<zeta>) < 2*d"
+            by (simp add: dist_norm)
+          also have "... \<le> e * cmod z"
+            using mult_right_mono \<open>0 < e\<close> that by (auto simp: d_def)
+          finally have "cmod (\<xi> - \<zeta>) < e * cmod z" .
+          with e have "\<xi> = \<zeta>"
+            by (metis \<open>\<xi>^n = z^n\<close> \<open>\<zeta>^n = z^n\<close> assms power_eq_imp_eq_norm)
+          then show "False"
+            using \<open>ball \<xi> d \<noteq> ball \<zeta> d\<close> by blast
+        qed
+        show "Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n))"
+          if "u \<in> {ball z' d |z'. z' ^ n = z ^ n}" for u
+        proof (rule invariance_of_domain_homeomorphism [of "u" "\<lambda>z. z^n"])
+          show "open u"
+            using that by auto
+          show "continuous_on u (\<lambda>z. z ^ n)"
+            by (intro continuous_intros)
+          show "inj_on (\<lambda>z. z ^ n) u"
+            using that by (auto simp: iff_x_eq_y inj_on_def)
+          show "\<And>g. homeomorphism u ((\<lambda>z. z ^ n) ` u) (\<lambda>z. z ^ n) g \<Longrightarrow> Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n))"
+            using im_eq that by clarify metis
+        qed auto
+      qed auto
     qed
-    have ball3: "Ex (homeomorphism (ball z' d) ((\<lambda>w. w^n) ` ball z d) (\<lambda>z. z^n))"
-            if zeq: "z'^n = z^n" for z'
-    proof -
-      have inj: "inj_on (\<lambda>z. z ^ n) (ball z' d)"
-        by (meson iff_x_eq_y inj_onI zeq)
-      show ?thesis
-        apply (rule invariance_of_domain_homeomorphism [of "ball z' d" "\<lambda>z. z^n"])
-          apply (rule open_ball continuous_intros order_refl inj)+
-        apply (force simp: im_eq [OF zeq])
-        done
-    qed
-    show ?thesis
-      apply (rule_tac x = "(\<lambda>w. w^n) ` (ball z d)" in exI)
-      apply (intro conjI open_imball)
-        using \<open>d > 0\<close> apply simp
-       using \<open>z \<noteq> 0\<close> assms apply (force simp: d_def)
-      apply (rule_tac x="{ ball z' d |z'. z'^n = z^n}" in exI)
-      apply (intro conjI ball1 ball2)
-       apply (force simp: assms d_def power_eq_imp_eq_norm that, clarify)
-      by (metis ball3)
   qed
   show ?thesis
     using assms
@@ -3353,7 +3365,7 @@
   show "range exp = - {0::complex}"
     by auto (metis exp_Ln range_eqI)
   show "\<exists>T. z \<in> T \<and> openin (subtopology euclidean (- {0})) T \<and>
-             (\<exists>v. \<Union>v = {z. exp z \<in> T} \<and> (\<forall>u\<in>v. open u) \<and> disjoint v \<and>
+             (\<exists>v. \<Union>v = exp -` T \<and> (\<forall>u\<in>v. open u) \<and> disjoint v \<and>
                   (\<forall>u\<in>v. \<exists>q. homeomorphism u T exp q))"
         if "z \<in> - {0::complex}" for z
   proof -
@@ -3374,8 +3386,8 @@
         using pi_ge_two by (simp add: ball_subset_ball_iff)
       ultimately show "openin (subtopology euclidean (- {0})) (exp ` ball (Ln z) 1)"
         by (auto simp: openin_open_eq invariance_of_domain continuous_on_exp [OF continuous_on_id])
-      show "\<Union>\<V> = {w. exp w \<in> exp ` ball (Ln z) 1}"
-        by (auto simp: \<V>_def Complex_Transcendental.exp_eq image_iff)
+      show "\<Union>\<V> = exp -` exp ` ball (Ln z) 1"
+        by (force simp: \<V>_def Complex_Transcendental.exp_eq image_iff)
       show "\<forall>V\<in>\<V>. open V"
         by (auto simp: \<V>_def inj_on_def continuous_intros invariance_of_domain)
       have xy: "2 \<le> cmod (2 * of_int x * of_real pi * \<i> - 2 * of_int y * of_real pi * \<i>)"
@@ -4314,7 +4326,7 @@
     qed
   next
     case False
-    obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+    have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
     proof (rule continuous_discrete_range_constant [OF ST])
       show "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
         apply (intro continuous_intros)
@@ -4338,7 +4350,9 @@
         then show ?thesis
           by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
       qed
-    qed blast
+    qed 
+    then obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+      by (auto simp: constant_on_def)
     with False have "exp a = 1"
       by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
     with a show ?thesis
@@ -4382,7 +4396,7 @@
     qed
   next
     case False
-    obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+    have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
     proof (rule continuous_discrete_range_constant [OF ST])
       show "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
         apply (intro continuous_intros)
@@ -4406,7 +4420,9 @@
         then show ?thesis
           by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
       qed
-    qed blast
+    qed
+    then obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+      by (auto simp: constant_on_def)
     with False have "exp a = 1"
       by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
     with a show ?thesis
@@ -4441,7 +4457,7 @@
     using fim by auto
   then obtain f' where f': "\<And>y. y \<in> T \<longrightarrow> f' y \<in> S \<and> f (f' y) = y"
     by metis
-  have *: "\<exists>a. \<forall>x \<in> {x. x \<in> S \<and> f x = y}. h x - h(f' y) = a" if "y \<in> T" for y
+  have *: "(\<lambda>x. h x - h(f' y)) constant_on {x. x \<in> S \<and> f x = y}" if "y \<in> T" for y
   proof (rule continuous_discrete_range_constant [OF conn [OF that], of "\<lambda>x. h x - h (f' y)"], simp_all add: algebra_simps)
     show "continuous_on {x \<in> S. f x = y} (\<lambda>x. h x - h (f' y))"
       by (intro continuous_intros continuous_on_subset [OF conth]) auto
@@ -4462,13 +4478,12 @@
     qed
   qed 
   have "h x = h (f' (f x))" if "x \<in> S" for x
-    using * [of "f x"] fim that apply clarsimp
-    by (metis f' imageI right_minus_eq)
+    using * [of "f x"] fim that unfolding constant_on_def by clarsimp (metis f' imageI right_minus_eq)
   moreover have "\<And>x. x \<in> T \<Longrightarrow> \<exists>u. u \<in> S \<and> x = f u \<and> h (f' x) = h u"
     using f' by fastforce
   ultimately
   have eq: "((\<lambda>x. (x, (h \<circ> f') x)) ` T) =
-            {p. \<exists>x. x \<in> S \<and> (x, p) \<in> {z \<in> S \<times> UNIV. snd z - ((f \<circ> fst) z, (h \<circ> fst) z) \<in> {0}}}"
+            {p. \<exists>x. x \<in> S \<and> (x, p) \<in> (S \<times> UNIV) \<inter> ((\<lambda>z. snd z - ((f \<circ> fst) z, (h \<circ> fst) z)) -` {0})}"
     using fim by (auto simp: image_iff)
   show "\<exists>h. continuous_on T h \<and> (\<forall>x\<in>T. g x = exp (h x))"
   proof (intro exI conjI)
@@ -4513,9 +4528,10 @@
     proof (rule compact_continuous_image)
       show "continuous_on {x \<in> S. f x = y} h"
         by (rule continuous_on_subset [OF conth]) auto
-      have "compact {x \<in> S. f x \<in> {y}}"
+      have "compact (S \<inter> f -` {y})"
         by (rule proper_map_from_compact [OF contf _ \<open>compact S\<close>, of T]) (simp_all add: fim that)
-      then show "compact {x \<in> S. f x = y}" by simp
+      then show "compact {x \<in> S. f x = y}" 
+        by (auto simp: vimage_def Int_def)
     qed
     have 2: "h ` {x \<in> S. f x = y} \<noteq> {}"
       using fim that by auto