src/HOL/Analysis/Homeomorphism.thy

 
 theory Homeomorphism
 imports Homotopy
 begin
 
-lemma%unimportant homeomorphic_spheres':
+lemma homeomorphic_spheres':
   fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space"
   assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)"
   shows "(sphere a \<delta>) homeomorphic (sphere b \<delta>)"
 proof -
   obtain f :: "'a\<Rightarrow>'b" and g where "linear f" "linear g"

     apply (force intro: continuous_intros
                   continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg)
     done
 qed
 
-lemma%unimportant homeomorphic_spheres_gen:
+lemma homeomorphic_spheres_gen:
     fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space"
   assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)"
   shows "(sphere a r homeomorphic sphere b s)"
   apply (rule homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres'])
   using assms  apply auto
   done
 
 subsection%important \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
 
-proposition%important ray_to_rel_frontier:
+proposition ray_to_rel_frontier:
   fixes a :: "'a::real_inner"
   assumes "bounded S"
       and a: "a \<in> rel_interior S"
       and aff: "(a + l) \<in> affine hull S"
       and "l \<noteq> 0"
   obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S"
            "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
-proof%unimportant -
+proof -
   have aaff: "a \<in> affine hull S"
     by (meson a hull_subset rel_interior_subset rev_subsetD)
   let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
   obtain B where "B > 0" and B: "S \<subseteq> ball a B"
     using bounded_subset_ballD [OF \<open>bounded S\<close>] by blast

     by (simp add: rel_frontier_def)
   show ?thesis
     by (rule that [OF \<open>0 < d\<close> infront inint])
 qed
 
-corollary%important ray_to_frontier:
+corollary ray_to_frontier:
   fixes a :: "'a::euclidean_space"
   assumes "bounded S"
       and a: "a \<in> interior S"
       and "l \<noteq> 0"
   obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S"
            "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S"
-proof%unimportant -
+proof -
   have "interior S = rel_interior S"
     using a rel_interior_nonempty_interior by auto
   then have "a \<in> rel_interior S"
     using a by simp
   then show ?thesis

      using a affine_hull_nonempty_interior apply blast
     by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
 qed
 
 
-lemma%unimportant segment_to_rel_frontier_aux:
+lemma segment_to_rel_frontier_aux:
   fixes x :: "'a::euclidean_space"
   assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y"
   obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
                    "open_segment x z \<subseteq> rel_interior S"
 proof -

       apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> x])
       using df rel_frontier_def by auto
   qed
 qed
 
-lemma%unimportant segment_to_rel_frontier:
+lemma segment_to_rel_frontier:
   fixes x :: "'a::euclidean_space"
   assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
       and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
   obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
                   "open_segment x z \<subseteq> rel_interior S"

   case False
   then show ?thesis
     using segment_to_rel_frontier_aux [OF S x y] that by blast
 qed
 
-proposition%important rel_frontier_not_sing:
+proposition rel_frontier_not_sing:
   fixes a :: "'a::euclidean_space"
   assumes "bounded S"
     shows "rel_frontier S \<noteq> {a}"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True  then show ?thesis  by simp
 next
   case False
   then obtain z where "z \<in> S"
     by blast

       qed
     qed
   qed
 qed
 
-proposition%important
+proposition (*FIXME needs name *)
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and 0: "0 \<in> rel_interior S"
       and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment 0 x \<subseteq> rel_interior S"
     shows starlike_compact_projective1_0:
             "S - rel_interior S homeomorphic sphere 0 1 \<inter> affine hull S"
             (is "?SMINUS homeomorphic ?SPHER")
       and starlike_compact_projective2_0:
             "S homeomorphic cball 0 1 \<inter> affine hull S"
             (is "S homeomorphic ?CBALL")
-proof%unimportant -
+proof -
   have starI: "(u *\<^sub>R x) \<in> rel_interior S" if "x \<in> S" "0 \<le> u" "u < 1" for x u
   proof (cases "x=0 \<or> u=0")
     case True with 0 show ?thesis by force
   next
     case False with that show ?thesis

     apply (subst homeomorphic_sym)
     apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball])
     done
 qed
 
-corollary%important
+corollary (* FIXME needs name *)
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and a: "a \<in> rel_interior S"
       and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
     shows starlike_compact_projective1:
             "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S"
       and starlike_compact_projective2:
             "S homeomorphic cball a 1 \<inter> affine hull S"
-proof%unimportant -
+proof -
   have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation)
   have 2: "0 \<in> rel_interior ((+) (-a) ` S)"
     using a rel_interior_translation [of "- a" S] by (simp cong: image_cong_simp)
   have 3: "open_segment 0 x \<subseteq> rel_interior ((+) (-a) ` S)" if "x \<in> ((+) (-a) ` S)" for x
   proof -

   also have "... homeomorphic cball a 1 \<inter> affine hull S"
     using homeomorphic_translation homeomorphic_sym by blast
   finally show "S homeomorphic cball a 1 \<inter> affine hull S" .
 qed
 
-corollary%important starlike_compact_projective_special:
+corollary starlike_compact_projective_special:
   assumes "compact S"
     and cb01: "cball (0::'a::euclidean_space) 1 \<subseteq> S"
     and scale: "\<And>x u. \<lbrakk>x \<in> S; 0 \<le> u; u < 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x \<in> S - frontier S"
   shows "S homeomorphic (cball (0::'a::euclidean_space) 1)"
-proof%unimportant -
+proof -
   have "ball 0 1 \<subseteq> interior S"
     using cb01 interior_cball interior_mono by blast
   then have 0: "0 \<in> rel_interior S"
     by (meson centre_in_ball subsetD interior_subset_rel_interior le_numeral_extra(2) not_le)
   have [simp]: "affine hull S = UNIV"

   qed
   show ?thesis
     using starlike_compact_projective2_0 [OF \<open>compact S\<close> 0 star] by simp
 qed
 
-lemma%important homeomorphic_convex_lemma:
+lemma homeomorphic_convex_lemma:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "convex S" "compact S" "convex T" "compact T"
       and affeq: "aff_dim S = aff_dim T"
     shows "(S - rel_interior S) homeomorphic (T - rel_interior T) \<and>
            S homeomorphic T"
-proof%unimportant (cases "rel_interior S = {} \<or> rel_interior T = {}")
+proof (cases "rel_interior S = {} \<or> rel_interior T = {}")
   case True
     then show ?thesis
       by (metis Diff_empty affeq \<open>convex S\<close> \<open>convex T\<close> aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty)
 next
   case False

   finally have 2: "S - rel_interior S homeomorphic T - rel_interior T" .
   show ?thesis
     using 1 2 by blast
 qed
 
-lemma%unimportant homeomorphic_convex_compact_sets:
+lemma homeomorphic_convex_compact_sets:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "convex S" "compact S" "convex T" "compact T"
       and affeq: "aff_dim S = aff_dim T"
     shows "S homeomorphic T"
 using homeomorphic_convex_lemma [OF assms] assms
 by (auto simp: rel_frontier_def)
 
-lemma%unimportant homeomorphic_rel_frontiers_convex_bounded_sets:
+lemma homeomorphic_rel_frontiers_convex_bounded_sets:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes "convex S" "bounded S" "convex T" "bounded T"
       and affeq: "aff_dim S = aff_dim T"
     shows  "rel_frontier S homeomorphic rel_frontier T"
 using assms homeomorphic_convex_lemma [of "closure S" "closure T"]

 
 subsection%important\<open>Homeomorphisms between punctured spheres and affine sets\<close>
 text\<open>Including the famous stereoscopic projection of the 3-D sphere to the complex plane\<close>
 
 text\<open>The special case with centre 0 and radius 1\<close>
-lemma%unimportant homeomorphic_punctured_affine_sphere_affine_01:
+lemma homeomorphic_punctured_affine_sphere_affine_01:
   assumes "b \<in> sphere 0 1" "affine T" "0 \<in> T" "b \<in> T" "affine p"
       and affT: "aff_dim T = aff_dim p + 1"
     shows "(sphere 0 1 \<inter> T) - {b} homeomorphic p"
 proof -
   have [simp]: "norm b = 1" "b\<bullet>b = 1"

     apply (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF \<open>affine T\<close>] affT)
     done
   finally show ?thesis .
 qed
 
-theorem%important homeomorphic_punctured_affine_sphere_affine:
+theorem homeomorphic_punctured_affine_sphere_affine:
   fixes a :: "'a :: euclidean_space"
   assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p"
       and aff: "aff_dim T = aff_dim p + 1"
     shows "(sphere a r \<inter> T) - {b} homeomorphic p"
-proof%unimportant -
+proof -
   have "a \<noteq> b" using assms by auto
   then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))"
     by (simp add: inj_on_def)
   have "((sphere a r \<inter> T) - {b}) homeomorphic
         (+) (-a) ` ((sphere a r \<inter> T) - {b})"

          apply (auto simp: dist_norm norm_minus_commute affine_scaling inj)
     done
   finally show ?thesis .
 qed
 
-corollary%important homeomorphic_punctured_sphere_affine:
+corollary homeomorphic_punctured_sphere_affine:
   fixes a :: "'a :: euclidean_space"
   assumes "0 < r" and b: "b \<in> sphere a r"
       and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
     shows "(sphere a r - {b}) homeomorphic T"
   using%unimportant homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by%unimportant auto
 
-corollary%important homeomorphic_punctured_sphere_hyperplane:
+corollary homeomorphic_punctured_sphere_hyperplane:
   fixes a :: "'a :: euclidean_space"
   assumes "0 < r" and b: "b \<in> sphere a r"
       and "c \<noteq> 0"
     shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}"
 apply (rule homeomorphic_punctured_sphere_affine)
 using assms
 apply (auto simp: affine_hyperplane of_nat_diff)
 done
 
-proposition%important homeomorphic_punctured_sphere_affine_gen:
+proposition homeomorphic_punctured_sphere_affine_gen:
   fixes a :: "'a :: euclidean_space"
   assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S"
       and "affine T" and affS: "aff_dim S = aff_dim T + 1"
     shows "rel_frontier S - {a} homeomorphic T"
-proof%unimportant -
+proof -
   obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S"
     using choose_affine_subset [OF affine_UNIV aff_dim_geq]
     by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex)
   have "S \<noteq> {}" using assms by auto
   then obtain z where "z \<in> U"

 
 text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set
   is homeomorphic to a closed subset of a convex set, and
   if the set is locally compact we can take the convex set to be the universe.\<close>
 
-proposition%important homeomorphic_closedin_convex:
+proposition homeomorphic_closedin_convex:
   fixes S :: "'m::euclidean_space set"
   assumes "aff_dim S < DIM('n)"
   obtains U and T :: "'n::euclidean_space set"
      where "convex U" "U \<noteq> {}" "closedin (subtopology euclidean U) T"
            "S homeomorphic T"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
   case True then show ?thesis
     by (rule_tac U=UNIV and T="{}" in that) auto
 next
   case False
   then obtain a where "a \<in> S" by auto

 subsection%important\<open>Locally compact sets in an open set\<close>
 
 text\<open> Locally compact sets are closed in an open set and are homeomorphic
   to an absolutely closed set if we have one more dimension to play with.\<close>
 
-lemma%important locally_compact_open_Int_closure:
+lemma locally_compact_open_Int_closure:
   fixes S :: "'a :: metric_space set"
   assumes "locally compact S"
   obtains T where "open T" "S = T \<inter> closure S"
-proof%unimportant -
+proof -
   have "\<forall>x\<in>S. \<exists>T v u. u = S \<inter> T \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<and> open T \<and> compact v"
     by (metis assms locally_compact openin_open)
   then obtain t v where
         tv: "\<And>x. x \<in> S
              \<Longrightarrow> v x \<subseteq> S \<and> open (t x) \<and> compact (v x) \<and> (\<exists>u. x \<in> u \<and> u \<subseteq> v x \<and> u = S \<inter> t x)"

   show ?thesis
     by (rule that [OF o e])
 qed
 
 
-lemma%unimportant locally_compact_closedin_open:
+lemma locally_compact_closedin_open:
     fixes S :: "'a :: metric_space set"
     assumes "locally compact S"
     obtains T where "open T" "closedin (subtopology euclidean T) S"
   by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int)
 
 
-lemma%unimportant locally_compact_homeomorphism_projection_closed:
+lemma locally_compact_homeomorphism_projection_closed:
   assumes "locally compact S"
   obtains T and f :: "'a \<Rightarrow> 'a :: euclidean_space \<times> 'b :: euclidean_space"
     where "closed T" "homeomorphism S T f fst"
 proof (cases "closed S")
   case True

       apply (rule homeomorphism_of_subsets [OF homU])
       using US apply auto
       done
 qed
 
-lemma%unimportant locally_compact_closed_Int_open:
+lemma locally_compact_closed_Int_open:
   fixes S :: "'a :: euclidean_space set"
   shows
     "locally compact S \<longleftrightarrow> (\<exists>U u. closed U \<and> open u \<and> S = U \<inter> u)"
 by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact)
 
 
-lemma%unimportant lowerdim_embeddings:
+lemma lowerdim_embeddings:
   assumes  "DIM('a) < DIM('b)"
   obtains f :: "'a::euclidean_space*real \<Rightarrow> 'b::euclidean_space" 
       and g :: "'b \<Rightarrow> 'a*real"
       and j :: 'b
   where "linear f" "linear g" "\<And>z. g (f z) = z" "j \<in> Basis" "\<And>x. f(x,0) \<bullet> j = 0"

       apply (rule comm_monoid_add_class.sum.neutral)
       using b01 inner_not_same_Basis by fastforce
   qed
 qed
 
-proposition%important locally_compact_homeomorphic_closed:
+proposition locally_compact_homeomorphic_closed:
   fixes S :: "'a::euclidean_space set"
   assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)"
   obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T"
-proof%unimportant -
+proof -
   obtain U:: "('a*real)set" and h
     where "closed U" and homU: "homeomorphism S U h fst"
     using locally_compact_homeomorphism_projection_closed assms by metis
   obtain f :: "'a*real \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a*real"
     where "linear f" "linear g" and gf [simp]: "\<And>z. g (f z) = z"

     apply (rule closed_injective_linear_image [OF \<open>closed U\<close> \<open>linear f\<close> \<open>inj f\<close>], assumption)
     done
 qed
 
 
-lemma%important homeomorphic_convex_compact_lemma:
+lemma homeomorphic_convex_compact_lemma:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S"
     and "compact S"
     and "cball 0 1 \<subseteq> S"
   shows "S homeomorphic (cball (0::'a) 1)"
-proof%unimportant (rule starlike_compact_projective_special[OF assms(2-3)])
+proof (rule starlike_compact_projective_special[OF assms(2-3)])
   fix x u
   assume "x \<in> S" and "0 \<le> u" and "u < (1::real)"
   have "open (ball (u *\<^sub>R x) (1 - u))"
     by (rule open_ball)
   moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"

   ultimately have "u *\<^sub>R x \<in> interior S" ..
   then show "u *\<^sub>R x \<in> S - frontier S"
     using frontier_def and interior_subset by auto
 qed
 
-proposition%important homeomorphic_convex_compact_cball:
+proposition homeomorphic_convex_compact_cball:
   fixes e :: real
     and S :: "'a::euclidean_space set"
   assumes "convex S"
     and "compact S"
     and "interior S \<noteq> {}"
     and "e > 0"
   shows "S homeomorphic (cball (b::'a) e)"
-proof%unimportant -
+proof -
   obtain a where "a \<in> interior S"
     using assms(3) by auto
   then obtain d where "d > 0" and d: "cball a d \<subseteq> S"
     unfolding mem_interior_cball by auto
   let ?d = "inverse d" and ?n = "0::'a"

     using \<open>d>0\<close> \<open>e>0\<close>
     apply (auto simp add: scaleR_right_diff_distrib)
     done
 qed
 
-corollary%important homeomorphic_convex_compact:
+corollary homeomorphic_convex_compact:
   fixes S :: "'a::euclidean_space set"
     and T :: "'a set"
   assumes "convex S" "compact S" "interior S \<noteq> {}"
     and "convex T" "compact T" "interior T \<noteq> {}"
   shows "S homeomorphic T"
   using assms
   by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
 
-subsection%important\<open>Covering spaces and lifting results for them\<close>
+subsection\<open>Covering spaces and lifting results for them\<close>
 
 definition%important covering_space
            :: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
   where
   "covering_space c p S \<equiv>

                     (\<exists>v. \<Union>v = c \<inter> p -` T \<and>
                         (\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
                         pairwise disjnt v \<and>
                         (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
 
-lemma%unimportant covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
+lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
   by (simp add: covering_space_def)
 
-lemma%unimportant covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
+lemma covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
   by (simp add: covering_space_def)
 
-lemma%unimportant homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
+lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
   apply (simp add: homeomorphism_def covering_space_def, clarify)
   apply (rule_tac x=T in exI, simp)
   apply (rule_tac x="{S}" in exI, auto)
   done
 
-lemma%unimportant covering_space_local_homeomorphism:
+lemma covering_space_local_homeomorphism:
   assumes "covering_space c p S" "x \<in> c"
   obtains T u q where "x \<in> T" "openin (subtopology euclidean c) T"
                       "p x \<in> u" "openin (subtopology euclidean S) u"
                       "homeomorphism T u p q"
 using assms
 apply (simp add: covering_space_def, clarify)
   apply (drule_tac x="p x" in bspec, force)
   by (metis IntI UnionE vimage_eq) 
 
 
-lemma%important covering_space_local_homeomorphism_alt:
+lemma covering_space_local_homeomorphism_alt:
   assumes p: "covering_space c p S" and "y \<in> S"
   obtains x T U q where "p x = y"
                         "x \<in> T" "openin (subtopology euclidean c) T"
                         "y \<in> U" "openin (subtopology euclidean S) U"
                           "homeomorphism T U p q"
-proof%unimportant -
+proof -
   obtain x where "p x = y" "x \<in> c"
     using assms covering_space_imp_surjective by blast
   show ?thesis
     apply (rule covering_space_local_homeomorphism [OF p \<open>x \<in> c\<close>])
     using that \<open>p x = y\<close> by blast
 qed
 
-proposition%important covering_space_open_map:
+proposition covering_space_open_map:
   fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set"
   assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T"
     shows "openin (subtopology euclidean S) (p ` T)"
-proof%unimportant -
+proof -
   have pce: "p ` c = S"
    and covs:
        "\<And>x. x \<in> S \<Longrightarrow>
             \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean S) X \<and>
                   \<Union>VS = c \<inter> p -` X \<and>

       done
   qed
   with openin_subopen show ?thesis by blast
 qed
 
-lemma%important covering_space_lift_unique_gen:
+lemma covering_space_lift_unique_gen:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
   assumes cov: "covering_space c p S"
       and eq: "g1 a = g2 a"
       and f: "continuous_on T f"  "f ` T \<subseteq> S"

       and fg1: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
       and g2: "continuous_on T g2"  "g2 ` T \<subseteq> c"
       and fg2: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
       and u_compt: "U \<in> components T" and "a \<in> U" "x \<in> U"
     shows "g1 x = g2 x"
-proof%unimportant -
+proof -
   have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
   define G12 where "G12 \<equiv> {x \<in> U. g1 x - g2 x = 0}"
   have "connected U" by (rule in_components_connected [OF u_compt])
   have contu: "continuous_on U g1" "continuous_on U g2"
        using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+

   with eq \<open>a \<in> U\<close> have "\<And>x. x \<in> U \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
   then show ?thesis
     using \<open>x \<in> U\<close> by force
 qed
 
-proposition%important covering_space_lift_unique:
+proposition covering_space_lift_unique:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
   assumes "covering_space c p S"
           "g1 a = g2 a"
           "continuous_on T f"  "f ` T \<subseteq> S"
           "continuous_on T g1"  "g1 ` T \<subseteq> c"  "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
           "continuous_on T g2"  "g2 ` T \<subseteq> c"  "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
           "connected T"  "a \<in> T"   "x \<in> T"
    shows "g1 x = g2 x"
-  using%unimportant covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
-  by%unimportant blast
-
-lemma%unimportant covering_space_locally:
+  using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
+  by blast
+
+lemma covering_space_locally:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes loc: "locally \<phi> C" and cov: "covering_space C p S"
       and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
     shows "locally \<psi> S"
 proof -

   then show ?thesis
     using covering_space_imp_surjective [OF cov] by metis
 qed
 
 
-proposition%important covering_space_locally_eq:
+proposition covering_space_locally_eq:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes cov: "covering_space C p S"
       and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
       and qim: "\<And>q U. \<lbrakk>U \<subseteq> S; continuous_on U q; \<psi> U\<rbrakk> \<Longrightarrow> \<phi>(q ` U)"
     shows "locally \<psi> S \<longleftrightarrow> locally \<phi> C"
          (is "?lhs = ?rhs")
-proof%unimportant
+proof
   assume L: ?lhs
   show ?rhs
   proof (rule locallyI)
     fix V x
     assume V: "openin (subtopology euclidean C) V" and "x \<in> V"

   assume ?rhs
   then show ?lhs
     using cov covering_space_locally pim by blast
 qed
 
-lemma%unimportant covering_space_locally_compact_eq:
+lemma covering_space_locally_compact_eq:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "covering_space C p S"
   shows "locally compact S \<longleftrightarrow> locally compact C"
   apply (rule covering_space_locally_eq [OF assms])
    apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
   using compact_continuous_image by blast
 
-lemma%unimportant covering_space_locally_connected_eq:
+lemma covering_space_locally_connected_eq:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "covering_space C p S"
     shows "locally connected S \<longleftrightarrow> locally connected C"
   apply (rule covering_space_locally_eq [OF assms])
    apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
   using connected_continuous_image by blast
 
-lemma%unimportant covering_space_locally_path_connected_eq:
+lemma covering_space_locally_path_connected_eq:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "covering_space C p S"
     shows "locally path_connected S \<longleftrightarrow> locally path_connected C"
   apply (rule covering_space_locally_eq [OF assms])
    apply (meson path_connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
   using path_connected_continuous_image by blast
 
 
-lemma%unimportant covering_space_locally_compact:
+lemma covering_space_locally_compact:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "locally compact C" "covering_space C p S"
   shows "locally compact S"
   using assms covering_space_locally_compact_eq by blast
 
 
-lemma%unimportant covering_space_locally_connected:
+lemma covering_space_locally_connected:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "locally connected C" "covering_space C p S"
   shows "locally connected S"
   using assms covering_space_locally_connected_eq by blast
 
-lemma%unimportant covering_space_locally_path_connected:
+lemma covering_space_locally_path_connected:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "locally path_connected C" "covering_space C p S"
   shows "locally path_connected S"
   using assms covering_space_locally_path_connected_eq by blast
 
-proposition%important covering_space_lift_homotopy:
+proposition covering_space_lift_homotopy:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and h :: "real \<times> 'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S"
       and conth: "continuous_on ({0..1} \<times> U) h"
       and him: "h ` ({0..1} \<times> U) \<subseteq> S"

       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> C"
     obtains k where "continuous_on ({0..1} \<times> U) k"
                     "k ` ({0..1} \<times> U) \<subseteq> C"
                     "\<And>y. y \<in> U \<Longrightarrow> k(0, y) = f y"
                     "\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p(k z)"
-proof%unimportant -
+proof -
   have "\<exists>V k. openin (subtopology euclidean U) V \<and> y \<in> V \<and>
               continuous_on ({0..1} \<times> V) k \<and> k ` ({0..1} \<times> V) \<subseteq> C \<and>
               (\<forall>z \<in> V. k(0, z) = f z) \<and> (\<forall>z \<in> {0..1} \<times> V. h z = p(k z))"
         if "y \<in> U" for y
   proof -

     show "\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p (k z)"
       using V*k by auto
   qed (auto simp: contk)
 qed
 
-corollary%important covering_space_lift_homotopy_alt:
+corollary covering_space_lift_homotopy_alt:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and h :: "'c::real_normed_vector \<times> real \<Rightarrow> 'b"
   assumes cov: "covering_space C p S"
       and conth: "continuous_on (U \<times> {0..1}) h"
       and him: "h ` (U \<times> {0..1}) \<subseteq> S"

       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> C"
   obtains k where "continuous_on (U \<times> {0..1}) k"
                   "k ` (U \<times> {0..1}) \<subseteq> C"
                   "\<And>y. y \<in> U \<Longrightarrow> k(y, 0) = f y"
                   "\<And>z. z \<in> U \<times> {0..1} \<Longrightarrow> h z = p(k z)"
-proof%unimportant -
+proof -
   have "continuous_on ({0..1} \<times> U) (h \<circ> (\<lambda>z. (snd z, fst z)))"
     by (intro continuous_intros continuous_on_subset [OF conth]) auto
   then obtain k where contk: "continuous_on ({0..1} \<times> U) k"
                   and kim:  "k ` ({0..1} \<times> U) \<subseteq> C"
                   and k0: "\<And>y. y \<in> U \<Longrightarrow> k(0, y) = f y"

        apply (intro continuous_intros continuous_on_subset [OF contk])
     using kim heqp apply (auto simp: k0)
     done
 qed
 
-corollary%important covering_space_lift_homotopic_function:
+corollary covering_space_lift_homotopic_function:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and g:: "'c::real_normed_vector \<Rightarrow> 'a"
   assumes cov: "covering_space C p S"
       and contg: "continuous_on U g"
       and gim: "g ` U \<subseteq> C"
       and pgeq: "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
       and hom: "homotopic_with (\<lambda>x. True) U S f f'"
     obtains g' where "continuous_on U g'" "image g' U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g' y) = f' y"
-proof%unimportant -
+proof -
   obtain h where conth: "continuous_on ({0..1::real} \<times> U) h"
              and him: "h ` ({0..1} \<times> U) \<subseteq> S"
              and h0:  "\<And>x. h(0, x) = f x"
              and h1: "\<And>x. h(1, x) = f' x"
     using hom by (auto simp: homotopic_with_def)

     show "\<And>y. y \<in> U \<Longrightarrow> p ((k \<circ> Pair 1) y) = f' y"
       by (auto simp: h1 heq [symmetric])
   qed
 qed
 
-corollary%important covering_space_lift_inessential_function:
+corollary covering_space_lift_inessential_function:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and U :: "'c::real_normed_vector set"
   assumes cov: "covering_space C p S"
       and hom: "homotopic_with (\<lambda>x. True) U S f (\<lambda>x. a)"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (cases "U = {}")
+proof (cases "U = {}")
   case True
   then show ?thesis
     using that continuous_on_empty by blast
 next
   case False

     done
 qed
 
 subsection%important\<open> Lifting of general functions to covering space\<close>
 
-proposition%important covering_space_lift_path_strong:
+proposition covering_space_lift_path_strong:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S" and "a \<in> C"
       and "path g" and pag: "path_image g \<subseteq> S" and pas: "pathstart g = p a"
     obtains h where "path h" "path_image h \<subseteq> C" "pathstart h = a"
                 and "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = g t"
-proof%unimportant -
+proof -
   obtain k:: "real \<times> 'c \<Rightarrow> 'a"
     where contk: "continuous_on ({0..1} \<times> {undefined}) k"
       and kim: "k ` ({0..1} \<times> {undefined}) \<subseteq> C"
       and k0:  "k (0, undefined) = a"
       and pk: "\<And>z. z \<in> {0..1} \<times> {undefined} \<Longrightarrow> p(k z) = (g \<circ> fst) z"

     show "\<And>t. t \<in> {0..1} \<Longrightarrow> p ((k \<circ> (\<lambda>t. (t, undefined))) t) = g t"
       by (auto simp: pk)
   qed
 qed
 
-corollary%important covering_space_lift_path:
+corollary covering_space_lift_path:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes cov: "covering_space C p S" and "path g" and pig: "path_image g \<subseteq> S"
   obtains h where "path h" "path_image h \<subseteq> C" "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = g t"
-proof%unimportant -
+proof -
   obtain a where "a \<in> C" "pathstart g = p a"
     by (metis pig cov covering_space_imp_surjective imageE pathstart_in_path_image subsetCE)
   show ?thesis
     using covering_space_lift_path_strong [OF cov \<open>a \<in> C\<close> \<open>path g\<close> pig]
     by (metis \<open>pathstart g = p a\<close> that)
 qed
 
   
-proposition%important covering_space_lift_homotopic_paths:
+proposition covering_space_lift_homotopic_paths:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes cov: "covering_space C p S"
       and "path g1" and pig1: "path_image g1 \<subseteq> S"
       and "path g2" and pig2: "path_image g2 \<subseteq> S"
       and hom: "homotopic_paths S g1 g2"
       and "path h1" and pih1: "path_image h1 \<subseteq> C" and ph1: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h1 t) = g1 t"
       and "path h2" and pih2: "path_image h2 \<subseteq> C" and ph2: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h2 t) = g2 t"
       and h1h2: "pathstart h1 = pathstart h2"
     shows "homotopic_paths C h1 h2"
-proof%unimportant -
+proof -
   obtain h :: "real \<times> real \<Rightarrow> 'b"
      where conth: "continuous_on ({0..1} \<times> {0..1}) h"
        and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
        and h0: "\<And>x. h (0, x) = g1 x" and h1: "\<And>x. h (1, x) = g2 x"
        and heq0: "\<And>t. t \<in> {0..1} \<Longrightarrow> h (t, 0) = g1 0"

     qed (use contk kim g1im h1im that in \<open>auto simp: ph1 continuous_on_const\<close>)
   qed (use contk kim in auto)
 qed
 
 
-corollary%important covering_space_monodromy:
+corollary covering_space_monodromy:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes cov: "covering_space C p S"
       and "path g1" and pig1: "path_image g1 \<subseteq> S"
       and "path g2" and pig2: "path_image g2 \<subseteq> S"
       and hom: "homotopic_paths S g1 g2"

     shows "pathfinish h1 = pathfinish h2"
   using%unimportant covering_space_lift_homotopic_paths [OF assms] homotopic_paths_imp_pathfinish
   by%unimportant blast
 
 
-corollary%important covering_space_lift_homotopic_path:
+corollary covering_space_lift_homotopic_path:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes cov: "covering_space C p S"
       and hom: "homotopic_paths S f f'"
       and "path g" and pig: "path_image g \<subseteq> C"
       and a: "pathstart g = a" and b: "pathfinish g = b"
       and pgeq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(g t) = f t"
   obtains g' where "path g'" "path_image g' \<subseteq> C"
                    "pathstart g' = a" "pathfinish g' = b" "\<And>t. t \<in> {0..1} \<Longrightarrow> p(g' t) = f' t"
-proof%unimportant (rule covering_space_lift_path_strong [OF cov, of a f'])
+proof (rule covering_space_lift_path_strong [OF cov, of a f'])
   show "a \<in> C"
     using a pig by auto
   show "path f'" "path_image f' \<subseteq> S"
     using hom homotopic_paths_imp_path homotopic_paths_imp_subset by blast+
   show "pathstart f' = p a"
     by (metis a atLeastAtMost_iff hom homotopic_paths_imp_pathstart order_refl pathstart_def pgeq zero_le_one)
 qed (metis (mono_tags, lifting) assms cov covering_space_monodromy hom homotopic_paths_imp_path homotopic_paths_imp_subset pgeq pig)
 
 
-proposition%important covering_space_lift_general:
+proposition covering_space_lift_general:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S" and "a \<in> C" "z \<in> U"
       and U: "path_connected U" "locally path_connected U"
       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"

       and hom: "\<And>r. \<lbrakk>path r; path_image r \<subseteq> U; pathstart r = z; pathfinish r = z\<rbrakk>
                      \<Longrightarrow> \<exists>q. path q \<and> path_image q \<subseteq> C \<and>
                              pathstart q = a \<and> pathfinish q = a \<and>
                              homotopic_paths S (f \<circ> r) (p \<circ> q)"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant -
+proof -
   have *: "\<exists>g h. path g \<and> path_image g \<subseteq> U \<and>
                  pathstart g = z \<and> pathfinish g = y \<and>
                  path h \<and> path_image h \<subseteq> C \<and> pathstart h = a \<and>
                  (\<forall>t \<in> {0..1}. p(h t) = f(g t))"
           if "y \<in> U" for y

       by (metis IntD1 IntD2 vimage_eq openin_subopen continuous_on_open_gen [OF LC])
   qed
 qed
 
 
-corollary%important covering_space_lift_stronger:
+corollary covering_space_lift_stronger:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
       and U: "path_connected U" "locally path_connected U"
       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
       and feq: "f z = p a"
       and hom: "\<And>r. \<lbrakk>path r; path_image r \<subseteq> U; pathstart r = z; pathfinish r = z\<rbrakk>
                      \<Longrightarrow> \<exists>b. homotopic_paths S (f \<circ> r) (linepath b b)"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (rule covering_space_lift_general [OF cov U contf fim feq])
+proof (rule covering_space_lift_general [OF cov U contf fim feq])
   fix r
   assume "path r" "path_image r \<subseteq> U" "pathstart r = z" "pathfinish r = z"
   then obtain b where b: "homotopic_paths S (f \<circ> r) (linepath b b)"
     using hom by blast
   then have "f (pathstart r) = b"

                   path_image q \<subseteq> C \<and>
                   pathstart q = a \<and> pathfinish q = a \<and> homotopic_paths S (f \<circ> r) (p \<circ> q)"
     by (force simp: \<open>a \<in> C\<close>)
 qed auto
 
-corollary%important covering_space_lift_strong:
+corollary covering_space_lift_strong:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
       and scU: "simply_connected U" and lpcU: "locally path_connected U"
       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
       and feq: "f z = p a"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
+proof (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
   show "path_connected U"
     using scU simply_connected_eq_contractible_loop_some by blast
   fix r
   assume r: "path r" "path_image r \<subseteq> U" "pathstart r = z" "pathfinish r = z"
   have "linepath (f z) (f z) = f \<circ> linepath z z"

     by (metis r contf fim homotopic_paths_continuous_image scU simply_connected_eq_contractible_path)
   then show "\<exists>b. homotopic_paths S (f \<circ> r) (linepath b b)"
     by blast
 qed blast
 
-corollary%important covering_space_lift:
+corollary covering_space_lift:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
   assumes cov: "covering_space C p S"
       and U: "simply_connected U"  "locally path_connected U"
       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
     obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (cases "U = {}")
+proof (cases "U = {}")
   case True
   with that show ?thesis by auto
 next
   case False
   then obtain z where "z \<in> U" by blast