diff -r a8faf6f15da7 -r 96a43caa4902 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Thu Jan 17 16:08:41 2019 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy	Thu Jan 17 16:22:21 2019 -0500
@@ -61,8 +61,6 @@
 I realized afterwards that this theory has a lot in common with \<^file>\<open>~~/src/HOL/Library/Finite_Map.thy\<close>.
 \<close>
 
-
-
 subsection%important \<open>Topology without type classes\<close>
 
 subsubsection%important \<open>The topology generated by some (open) subsets\<close>
@@ -80,14 +78,14 @@
 | UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
 | Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"
 
-lemma istopology_generate_topology_on:
+lemma%unimportant istopology_generate_topology_on:
   "istopology (generate_topology_on S)"
 unfolding istopology_def by (auto intro: generate_topology_on.intros)
 
 text \<open>The basic property of the topology generated by a set \<open>S\<close> is that it is the
 smallest topology containing all the elements of \<open>S\<close>:\<close>
 
-lemma generate_topology_on_coarsest:
+lemma%unimportant generate_topology_on_coarsest:
   assumes "istopology T"
           "\<And>s. s \<in> S \<Longrightarrow> T s"
           "generate_topology_on S s0"
@@ -98,17 +96,17 @@
 abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
   where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
 
-lemma openin_topology_generated_by_iff:
+lemma%unimportant openin_topology_generated_by_iff:
   "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
   using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp
 
-lemma openin_topology_generated_by:
+lemma%unimportant openin_topology_generated_by:
   "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
 using openin_topology_generated_by_iff by auto
 
-lemma topology_generated_by_topspace:
+lemma%important topology_generated_by_topspace:
   "topspace (topology_generated_by S) = (\<Union>S)"
-proof
+proof%unimportant
   {
     fix s assume "openin (topology_generated_by S) s"
     then have "generate_topology_on S s" by (rule openin_topology_generated_by)
@@ -123,9 +121,9 @@
     unfolding topspace_def using openin_topology_generated_by_iff by auto
 qed
 
-lemma topology_generated_by_Basis:
+lemma%important topology_generated_by_Basis:
   "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
-  by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
+by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
 
 lemma generate_topology_on_Inter:
   "\<lbrakk>finite \<F>; \<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on \<S> K; \<F> \<noteq> {}\<rbrakk> \<Longrightarrow> generate_topology_on \<S> (\<Inter>\<F>)"
@@ -268,28 +266,28 @@
   where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
                                       \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
 
-lemma continuous_on_continuous_on_topo:
+lemma%important continuous_on_continuous_on_topo:
   "continuous_on s f \<longleftrightarrow> continuous_on_topo (subtopology euclidean s) euclidean f"
-  unfolding continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
+unfolding%unimportant continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
 topspace_euclidean_subtopology open_openin topspace_euclidean by fast
 
-lemma continuous_on_topo_UNIV:
+lemma%unimportant continuous_on_topo_UNIV:
   "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
 using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto
 
-lemma continuous_on_topo_open [intro]:
+lemma%important continuous_on_topo_open [intro]:
   "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
-  unfolding continuous_on_topo_def by auto
+unfolding%unimportant continuous_on_topo_def by auto
 
-lemma continuous_on_topo_topspace [intro]:
+lemma%unimportant continuous_on_topo_topspace [intro]:
   "continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
 unfolding continuous_on_topo_def by auto
 
-lemma continuous_on_generated_topo_iff:
+lemma%important continuous_on_generated_topo_iff:
   "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
       ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
 unfolding continuous_on_topo_def topology_generated_by_topspace
-proof (auto simp add: topology_generated_by_Basis)
+proof%unimportant (auto simp add: topology_generated_by_Basis)
   assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
   fix U assume "openin (topology_generated_by S) U"
   then have "generate_topology_on S U" by (rule openin_topology_generated_by)
@@ -311,17 +309,17 @@
   qed (auto simp add: H)
 qed
 
-lemma continuous_on_generated_topo:
+lemma%important continuous_on_generated_topo:
   assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
           "f`(topspace T1) \<subseteq> (\<Union> S)"
   shows "continuous_on_topo T1 (topology_generated_by S) f"
-  using assms continuous_on_generated_topo_iff by blast
+using%unimportant assms continuous_on_generated_topo_iff by blast
 
-proposition continuous_on_topo_compose:
+lemma%important continuous_on_topo_compose:
   assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
   shows "continuous_on_topo T1 T3 (g o f)"
-  using assms unfolding continuous_on_topo_def
-proof (auto)
+using%unimportant assms unfolding continuous_on_topo_def
+proof%unimportant (auto)
   fix U :: "'c set"
   assume H: "openin T3 U"
   have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
@@ -332,7 +330,7 @@
     by simp
 qed (blast)
 
-lemma continuous_on_topo_preimage_topspace [intro]:
+lemma%unimportant continuous_on_topo_preimage_topspace [intro]:
   assumes "continuous_on_topo T1 T2 f"
   shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
 using assms unfolding continuous_on_topo_def by auto
@@ -351,9 +349,9 @@
 definition%important pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
   where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
 
-lemma istopology_pullback_topology:
+lemma%important istopology_pullback_topology:
   "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
-  unfolding istopology_def proof (auto)
+unfolding%unimportant istopology_def proof (auto)
   fix K assume "\<forall>S\<in>K. \<exists>U. openin T U \<and> S = f -` U \<inter> A"
   then have "\<exists>U. \<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
     by (rule bchoice)
@@ -364,19 +362,19 @@
   then show "\<exists>V. openin T V \<and> \<Union>K = f -` V \<inter> A" by auto
 qed
 
-lemma openin_pullback_topology:
+lemma%unimportant openin_pullback_topology:
   "openin (pullback_topology A f T) S \<longleftrightarrow> (\<exists>U. openin T U \<and> S = f-`U \<inter> A)"
 unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto
 
-lemma topspace_pullback_topology:
+lemma%unimportant topspace_pullback_topology:
   "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
 by (auto simp add: topspace_def openin_pullback_topology)
 
-proposition continuous_on_topo_pullback [intro]:
+lemma%important continuous_on_topo_pullback [intro]:
   assumes "continuous_on_topo T1 T2 g"
   shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
 unfolding continuous_on_topo_def
-proof (auto)
+proof%unimportant (auto)
   fix U::"'b set" assume "openin T2 U"
   then have "openin T1 (g-`U \<inter> topspace T1)"
     using assms unfolding continuous_on_topo_def by auto
@@ -396,11 +394,11 @@
     using assms unfolding continuous_on_topo_def by auto
 qed
 
-proposition continuous_on_topo_pullback' [intro]:
+lemma%important continuous_on_topo_pullback' [intro]:
   assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
   shows "continuous_on_topo T1 (pullback_topology A f T2) g"
 unfolding continuous_on_topo_def
-proof (auto)
+proof%unimportant (auto)
   fix U assume "openin (pullback_topology A f T2) U"
   then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
     unfolding openin_pullback_topology by auto
@@ -549,9 +547,9 @@
     done
 qed
 
-lemma topspace_product_topology:
+lemma%important topspace_product_topology:
   "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
-proof
+proof%unimportant
   show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
     unfolding product_topology_def topology_generated_by_topspace
     unfolding topspace_def by auto
@@ -561,16 +559,16 @@
     unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
 qed
 
-lemma product_topology_basis:
+lemma%unimportant product_topology_basis:
   assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
   shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
   unfolding product_topology_def
   by (rule topology_generated_by_Basis) (use assms in auto)
 
-proposition product_topology_open_contains_basis:
+lemma%important product_topology_open_contains_basis:
   assumes "openin (product_topology T I) U" "x \<in> U"
   shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
-proof -
+proof%unimportant -
   have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"
     using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
   then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
@@ -719,7 +717,7 @@
 
 text \<open>The basic property of the product topology is the continuity of projections:\<close>
 
-lemma continuous_on_topo_product_coordinates [simp]:
+lemma%unimportant continuous_on_topo_product_coordinates [simp]:
   assumes "i \<in> I"
   shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"
 proof -
@@ -741,12 +739,12 @@
     by (auto simp add: assms topspace_product_topology PiE_iff)
 qed
 
-lemma continuous_on_topo_coordinatewise_then_product [intro]:
+lemma%important continuous_on_topo_coordinatewise_then_product [intro]:
   assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
           "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
   shows "continuous_on_topo T1 (product_topology T I) f"
 unfolding product_topology_def
-proof (rule continuous_on_generated_topo)
+proof%unimportant (rule continuous_on_generated_topo)
   fix U assume "U \<in> {Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
   then obtain X where H: "U = Pi\<^sub>E I X" "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
     by blast
@@ -774,7 +772,7 @@
     using assms unfolding continuous_on_topo_def by auto
 qed
 
-lemma continuous_on_topo_product_then_coordinatewise [intro]:
+lemma%unimportant continuous_on_topo_product_then_coordinatewise [intro]:
   assumes "continuous_on_topo T1 (product_topology T I) f"
   shows "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
         "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
@@ -796,7 +794,7 @@
     using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
 qed
 
-lemma continuous_on_restrict:
+lemma%unimportant continuous_on_restrict:
   assumes "J \<subseteq> I"
   shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
 proof (rule continuous_on_topo_coordinatewise_then_product)
@@ -819,7 +817,7 @@
 definition%important open_fun_def:
   "open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"
 
-instance proof
+instance proof%unimportant
   have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
     unfolding topspace_product_topology topspace_euclidean by auto
   then show "open (UNIV::('a \<Rightarrow> 'b) set)"
@@ -828,15 +826,15 @@
 
 end
 
-lemma euclidean_product_topology:
+lemma%unimportant euclidean_product_topology:
   "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
 by (metis open_openin topology_eq open_fun_def)
 
-proposition product_topology_basis':
+lemma%important product_topology_basis':
   fixes x::"'i \<Rightarrow> 'a" and U::"'i \<Rightarrow> ('b::topological_space) set"
   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
   shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
-proof -
+proof%unimportant -
   define J where "J = x`I"
   define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
   define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
@@ -866,24 +864,24 @@
 text \<open>The results proved in the general situation of products of possibly different
 spaces have their counterparts in this simpler setting.\<close>
 
-lemma continuous_on_product_coordinates [simp]:
+lemma%unimportant continuous_on_product_coordinates [simp]:
   "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
 unfolding continuous_on_topo_UNIV euclidean_product_topology
 by (rule continuous_on_topo_product_coordinates, simp)
 
-lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
+lemma%unimportant continuous_on_coordinatewise_then_product [intro, continuous_intros]:
   assumes "\<And>i. continuous_on UNIV (\<lambda>x. f x i)"
   shows "continuous_on UNIV f"
 using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
 by (rule continuous_on_topo_coordinatewise_then_product, simp)
 
-lemma continuous_on_product_then_coordinatewise:
+lemma%unimportant continuous_on_product_then_coordinatewise:
   assumes "continuous_on UNIV f"
   shows "continuous_on UNIV (\<lambda>x. f x i)"
 using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
 by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
 
-lemma continuous_on_product_coordinatewise_iff:
+lemma%unimportant continuous_on_product_coordinatewise_iff:
   "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
 by (auto intro: continuous_on_product_then_coordinatewise)
 
@@ -893,7 +891,7 @@
 of product spaces, but they have more to do with countability and could
 be put in the corresponding theory.\<close>
 
-lemma countable_nat_product_event_const:
+lemma%unimportant countable_nat_product_event_const:
   fixes F::"'a set" and a::'a
   assumes "a \<in> F" "countable F"
   shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"
@@ -930,7 +928,7 @@
   then show ?thesis using countable_subset[OF *] by auto
 qed
 
-lemma countable_product_event_const:
+lemma%unimportant countable_product_event_const:
   fixes F::"('a::countable) \<Rightarrow> 'b set" and b::'b
   assumes "\<And>i. countable (F i)"
   shows "countable {f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}"
@@ -963,7 +961,7 @@
 qed
 
 instance "fun" :: (countable, first_countable_topology) first_countable_topology
-proof
+proof%unimportant
   fix x::"'a \<Rightarrow> 'b"
   have "\<exists>A::('b \<Rightarrow> nat \<Rightarrow> 'b set). \<forall>x. (\<forall>i. x \<in> A x i \<and> open (A x i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A x i \<subseteq> S))"
     apply (rule choice) using first_countable_basis by auto
@@ -1035,11 +1033,11 @@
     using \<open>countable K\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> x \<in> k\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> open k\<close> Inc by auto
 qed
 
-proposition product_topology_countable_basis:
+lemma%important product_topology_countable_basis:
   shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
           topological_basis K \<and> countable K \<and>
           (\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
-proof -
+proof%unimportant -
   obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
     using ex_countable_basis by auto
   then have "B \<noteq> {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)
@@ -1142,15 +1140,15 @@
 definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
 where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
 
-lemma strong_operator_topology_topspace:
+lemma%unimportant strong_operator_topology_topspace:
   "topspace strong_operator_topology = UNIV"
 unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
 
-lemma strong_operator_topology_basis:
+lemma%important strong_operator_topology_basis:
   fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
   shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
-proof -
+proof%unimportant -
   have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
     by (rule product_topology_basis'[OF assms])
   moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
@@ -1160,16 +1158,16 @@
     unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto
 qed
 
-lemma strong_operator_topology_continuous_evaluation:
+lemma%important strong_operator_topology_continuous_evaluation:
   "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
-proof -
+proof%unimportant -
   have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
     unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
     using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
   then show ?thesis unfolding comp_def by simp
 qed
 
-lemma continuous_on_strong_operator_topo_iff_coordinatewise:
+lemma%unimportant continuous_on_strong_operator_topo_iff_coordinatewise:
   "continuous_on_topo T strong_operator_topology f
     \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
 proof (auto)
@@ -1192,9 +1190,9 @@
     by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
 qed
 
-lemma strong_operator_topology_weaker_than_euclidean:
+lemma%important strong_operator_topology_weaker_than_euclidean:
   "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
-  by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
+by%unimportant (subst continuous_on_strong_operator_topo_iff_coordinatewise,
     auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
 
 
@@ -1228,9 +1226,9 @@
 spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
 to do this.\<close>
 
-lemma dist_fun_le_dist_first_terms:
+lemma%important dist_fun_le_dist_first_terms:
   "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
-proof -
+proof%unimportant -
   have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
           = (\<Sum>n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))"
     by (rule suminf_cong, simp add: power_add)
@@ -1278,7 +1276,7 @@
   finally show ?thesis unfolding M_def by simp
 qed
 
-lemma open_fun_contains_ball_aux:
+lemma%unimportant open_fun_contains_ball_aux:
   assumes "open (U::(('a \<Rightarrow> 'b) set))"
           "x \<in> U"
   shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"
@@ -1341,7 +1339,7 @@
   then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
 qed
 
-lemma ball_fun_contains_open_aux:
+lemma%unimportant ball_fun_contains_open_aux:
   fixes x::"('a \<Rightarrow> 'b)" and e::real
   assumes "e>0"
   shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"
@@ -1388,7 +1386,7 @@
   ultimately show ?thesis by auto
 qed
 
-lemma fun_open_ball_aux:
+lemma%unimportant fun_open_ball_aux:
   fixes U::"('a \<Rightarrow> 'b) set"
   shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
 proof (auto)
@@ -1577,7 +1575,7 @@
 
 
 
-subsection%important \<open>Measurability\<close> (*FIX ME move? *)
+subsection%important \<open>Measurability\<close> (*FIX ME mv *)
 
 text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
 generated by open sets in the product, and the product sigma algebra, countably generated by
@@ -1595,11 +1593,11 @@
 compare it with the product sigma algebra as explained above.
 \<close>
 
-lemma measurable_product_coordinates [measurable (raw)]:
+lemma%unimportant measurable_product_coordinates [measurable (raw)]:
   "(\<lambda>x. x i) \<in> measurable borel borel"
 by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
 
-lemma measurable_product_then_coordinatewise:
+lemma%unimportant measurable_product_then_coordinatewise:
   fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
   assumes [measurable]: "f \<in> borel_measurable M"
   shows "(\<lambda>x. f x i) \<in> borel_measurable M"
@@ -1613,10 +1611,10 @@
 of the product sigma algebra that is more similar to the one we used above for the product
 topology.\<close>
 
-lemma sets_PiM_finite:
+lemma%important sets_PiM_finite:
   "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
         {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
-proof
+proof%unimportant
   have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
   proof (auto)
     fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
@@ -1656,9 +1654,9 @@
     done
 qed
 
-lemma sets_PiM_subset_borel:
+lemma%important sets_PiM_subset_borel:
   "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
-proof -
+proof%unimportant -
   have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
   proof -
     define I where "I = {i. X i \<noteq> UNIV}"
@@ -1675,9 +1673,9 @@
     by (simp add: * sets.sigma_sets_subset')
 qed
 
-proposition sets_PiM_equal_borel:
+lemma%important sets_PiM_equal_borel:
   "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
-proof
+proof%unimportant
   obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
             "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
     using product_topology_countable_basis by fast
@@ -1702,11 +1700,11 @@
     unfolding borel_def by auto
 qed (simp add: sets_PiM_subset_borel)
 
-lemma measurable_coordinatewise_then_product:
+lemma%important measurable_coordinatewise_then_product:
   fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
   assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
   shows "f \<in> borel_measurable M"
-proof -
+proof%unimportant -
   have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
     by (rule measurable_PiM_single', auto simp add: assms)
   then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast