src/HOL/Analysis/Fashoda_Theorem.thy

 lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
   apply(rule continuous_at_imp_continuous_on)
   apply (rule, rule continuous_interval_bij)
   done
 
-lemma%important in_interval_interval_bij:
+lemma in_interval_interval_bij:
   fixes a b u v x :: "'a::euclidean_space"
   assumes "x \<in> cbox a b"
     and "cbox u v \<noteq> {}"
   shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
   apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong)
   apply safe
-proof%unimportant -
+proof -
   fix i :: 'a
   assume i: "i \<in> Basis"
   have "cbox a b \<noteq> {}"
     using assms by auto
   with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"

   fixes x :: "real^2"
   assumes "infnorm x = 1"
   shows "\<bar>x$1\<bar> \<le> 1" and "\<bar>x$2\<bar> \<le> 1"
   using assms unfolding infnorm_eq_1_2 by auto
 
-lemma%important fashoda_unit:
+proposition fashoda_unit:
   fixes f g :: "real \<Rightarrow> real^2"
   assumes "f ` {-1 .. 1} \<subseteq> cbox (-1) 1"
     and "g ` {-1 .. 1} \<subseteq> cbox (-1) 1"
     and "continuous_on {-1 .. 1} f"
     and "continuous_on {-1 .. 1} g"
     and "f (- 1)$1 = - 1"
     and "f 1$1 = 1" "g (- 1) $2 = -1"
     and "g 1 $2 = 1"
   shows "\<exists>s\<in>{-1 .. 1}. \<exists>t\<in>{-1 .. 1}. f s = g t"
-proof%unimportant (rule ccontr)
+proof (rule ccontr)
   assume "\<not> ?thesis"
   note as = this[unfolded bex_simps,rule_format]
   define sqprojection
     where [abs_def]: "sqprojection z = (inverse (infnorm z)) *\<^sub>R z" for z :: "real^2"
   define negatex :: "real^2 \<Rightarrow> real^2"

       unfolding iff[OF nz] vector_component_simps * mem_box_cart
       by (erule_tac x=2 in allE) auto
   qed 
 qed
 
-lemma%important fashoda_unit_path:
+proposition fashoda_unit_path:
   fixes f g :: "real \<Rightarrow> real^2"
   assumes "path f"
     and "path g"
     and "path_image f \<subseteq> cbox (-1) 1"
     and "path_image g \<subseteq> cbox (-1) 1"
     and "(pathstart f)$1 = -1"
     and "(pathfinish f)$1 = 1"
     and "(pathstart g)$2 = -1"
     and "(pathfinish g)$2 = 1"
   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
-proof%unimportant -
+proof -
   note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
   define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real
   have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
     unfolding iscale_def by auto
   have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"

     using isc[unfolded subset_eq, rule_format]
     apply auto
     done
 qed
 
-lemma%important fashoda:
+theorem fashoda:
   fixes b :: "real^2"
   assumes "path f"
     and "path g"
     and "path_image f \<subseteq> cbox a b"
     and "path_image g \<subseteq> cbox a b"
     and "(pathstart f)$1 = a$1"
     and "(pathfinish f)$1 = b$1"
     and "(pathstart g)$2 = a$2"
     and "(pathfinish g)$2 = b$2"
   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
-proof%unimportant -
+proof -
   fix P Q S
   presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
   then show thesis
     by auto
 next

 qed
 
 
 subsection%important \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
 
-lemma%important fashoda_interlace:
+corollary fashoda_interlace:
   fixes a :: "real^2"
   assumes "path f"
     and "path g"
     and paf: "path_image f \<subseteq> cbox a b"
     and pag: "path_image g \<subseteq> cbox a b"

     and "(pathfinish g)$2 = a$2"
     and "(pathstart f)$1 < (pathstart g)$1"
     and "(pathstart g)$1 < (pathfinish f)$1"
     and "(pathfinish f)$1 < (pathfinish g)$1"
   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
-proof%unimportant -
+proof -
   have "cbox a b \<noteq> {}"
     using path_image_nonempty[of f] using assms(3) by auto
   note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
   have "pathstart f \<in> cbox a b"
     and "pathfinish f \<in> cbox a b"