# HG changeset patch
# User wenzelm
# Date 1392581387 -3600
# Node ID 23d2cbac6dce59c57562dcb8c4d03d424fe47206
# Parent  241c6a2fdda135f88e5b76872e014a583d64c9ee
tuned proofs;

diff -r 241c6a2fdda1 -r 23d2cbac6dce src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Feb 16 18:46:13 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Feb 16 21:09:47 2014 +0100
@@ -622,7 +622,7 @@
     apply auto
     done
   then obtain a where a: "a \<in> s" "\<forall>x\<in>s. \<forall>j. x j \<le> a j" ..
-  show ?thesis 
+  show ?thesis
     apply (rule_tac x = a in bexI)
   proof
     fix x
@@ -1755,15 +1755,26 @@
   have **: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a' \<in> s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
   proof -
     case goal1
-    guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this[rule_format]
+    obtain a0 a1 where exta:
+        "a0 \<in> s"
+        "a1 \<in> s"
+        "a0 \<noteq> a1"
+        "\<And>x. x \<in> s \<Longrightarrow> kle n a0 x \<and> kle n x a1"
+        "\<And>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
+      by (rule ksimplex_extrema_strong[OF assms(1,3)]) blast
     have a: "a = a1"
       apply (rule ksimplex_fix_plane_0[OF assms(2,4-5)])
       using exta(1-2,5)
       apply auto
       done
     moreover
-    guess b0 b1 by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)])
-    note extb = this[rule_format]
+    obtain b0 b1 where extb:
+        "b0 \<in> s'"
+        "b1 \<in> s'"
+        "b0 \<noteq> b1"
+        "\<And>x. x \<in> s' \<Longrightarrow> kle n b0 x \<and> kle n x b1"
+        "\<And>i. b1 i = (if i \<in> {1..n} then b0 i + 1 else b0 i)"
+      by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) blast
     have a': "a' = b1"
       apply (rule ksimplex_fix_plane_0[OF goal1(2) assms(4), of b0])
       unfolding goal1(3)
@@ -1815,15 +1826,26 @@
   have lem: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a'\<in>s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
   proof -
     case goal1
-    guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this [rule_format]
+    obtain a0 a1 where exta:
+        "a0 \<in> s"
+        "a1 \<in> s"
+        "a0 \<noteq> a1"
+        "\<And>x. x \<in> s \<Longrightarrow> kle n a0 x \<and> kle n x a1"
+        "\<And>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
+      by (rule ksimplex_extrema_strong[OF assms(1,3)]) blast
     have a: "a = a0"
       apply (rule ksimplex_fix_plane_p[OF assms(1-2,4-5) exta(1,2)])
       unfolding exta
       apply auto
       done
     moreover
-    guess b0 b1 by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)])
-    note extb = this [rule_format]
+    obtain b0 b1 where extb:
+        "b0 \<in> s'"
+        "b1 \<in> s'"
+        "b0 \<noteq> b1"
+        "\<And>x. x \<in> s' \<Longrightarrow> kle n b0 x \<and> kle n x b1"
+        "\<And>i. b1 i = (if i \<in> {1..n} then b0 i + 1 else b0 i)"
+      by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) blast
     have a': "a' = b0"
       apply (rule ksimplex_fix_plane_p[OF goal1(1-2) assms(4), of _ b1])
       unfolding goal1 extb
@@ -1891,7 +1913,13 @@
     then show False
       by auto
   qed
-  guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note a0a1 = this
+  obtain a0 a1 where a0a1:
+      "a0 \<in> s"
+      "a1 \<in> s"
+      "a0 \<noteq> a1"
+      "\<forall>x\<in>s. kle n a0 x \<and> kle n x a1"
+      "\<forall>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
+    by (rule ksimplex_extrema_strong[OF assms(1,3)])
   {
     assume "a = a0"
     have *: "\<And>P Q. P \<or> Q \<Longrightarrow> \<not> P \<Longrightarrow> Q"
@@ -1910,8 +1938,10 @@
       apply (rule_tac *[OF ksimplex_successor[OF assms(1-2),unfolded `a=a0`]])
       apply auto
       done
-    then guess a2 ..
-    from this(2) guess k .. note k = this note a2 =`a2 \<in> s`
+    then
+    obtain a2 k where a2: "a2 \<in> s"
+      and k: "k \<in> {1..n}" "\<forall>j. a2 j = (if j = k then a0 j + 1 else a0 j)"
+      by blast
     def a3 \<equiv> "\<lambda>j. if j = k then a1 j + 1 else a1 j"
     have "a3 \<notin> s"
     proof
@@ -1983,8 +2013,8 @@
               using `a1 \<in> s` ksimplexD(4)[OF assms(1)]
               by auto
           next
-            guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] ..
-            note a4 = this
+            obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> p"
+              using assms(5) k(1) by blast
             have "a2 k \<le> a4 k"
               using lem3[OF a4(1)[unfolded `a = a0`],THEN kle_imp_pointwise]
               by auto
@@ -2028,9 +2058,11 @@
       have lem4: "\<And>x. x\<in>s \<Longrightarrow> x \<noteq> a0 \<Longrightarrow> kle n x a3"
       proof -
         case goal1
-        guess kk using a0a1(4)[rule_format, OF `x\<in>s`,THEN conjunct2,unfolded kle_def]
-          by (elim exE conjE)
-        note kk = this
+        obtain kk where kk:
+            "kk \<subseteq> {1..n}"
+            "\<forall>j. a1 j = x j + (if j \<in> kk then 1 else 0)"
+          using a0a1(4)[rule_format, OF `x\<in>s`,THEN conjunct2,unfolded kle_def]
+          by blast
         have "k \<notin> kk"
         proof
           assume "k \<in> kk"
@@ -2109,9 +2141,16 @@
       unfolding mem_Collect_eq
     proof (erule conjE)
       fix s'
-      assume as: "ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
-      from this(2) guess a' .. note a' = this
-      guess a_min a_max by (rule ksimplex_extrema_strong[OF as assms(3)]) note min_max = this
+      assume as: "ksimplex p n s'"
+      assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
+      then obtain a' where a': "a' \<in> s'" "s' - {a'} = s - {a}" ..
+      obtain a_min a_max where min_max:
+          "a_min \<in> s'"
+          "a_max \<in> s'"
+          "a_min \<noteq> a_max"
+          "\<forall>x\<in>s'. kle n a_min x \<and> kle n x a_max"
+          "\<forall>i. a_max i = (if i \<in> {1..n} then a_min i + 1 else a_min i)"
+        by (rule ksimplex_extrema_strong[OF as assms(3)])
       have *: "\<forall>x\<in>s' - {a'}. x k = a2 k"
         unfolding a'
       proof
@@ -2270,7 +2309,10 @@
       apply (rule_tac *[OF ksimplex_predecessor[OF assms(1-2),unfolded `a=a1`]])
       apply auto
       done
-    then guess a2 .. from this(2) guess k .. note k=this note a2 = `a2 \<in> s`
+    then
+    obtain a2 k where a2: "a2 \<in> s"
+      and k: "k \<in> {1..n}" "\<forall>j. a1 j = (if j = k then a2 j + 1 else a2 j)"
+      by blast
     def a3 \<equiv> "\<lambda>j. if j = k then a0 j - 1 else a0 j"
     have "a2 \<noteq> a1"
       using k(2)[THEN spec[where x=k]] by auto
@@ -2297,8 +2339,8 @@
     qed
     have "a0 k \<noteq> 0"
     proof -
-      guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k\<in>{1..n}`] ..
-      note a4 = this
+      obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> 0"
+        using assms(4) `k\<in>{1..n}` by blast
       have "a4 k \<le> a2 k"
         using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise]
         by auto
@@ -2353,9 +2395,10 @@
               using `a0 \<in> s` ksimplexD(4)[OF assms(1)]
               by auto
           next
-            guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] ..
-            note a4 = this
-            case True have "a3 k \<le> a0 k"
+            case True
+            obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> p"
+              using assms(5) k(1) by blast
+            have "a3 k \<le> a0 k"
               unfolding lem4[rule_format] by auto
             also have "\<dots> \<le> p"
               using ksimplexD(4)[OF assms(1),rule_format, of a0 k] a0a1
@@ -2393,7 +2436,9 @@
         have "kle n a3 a2"
         proof -
           have "kle n a0 a1"
-            using a0a1 by auto then guess kk unfolding kle_def ..
+            using a0a1 by auto
+          then obtain kk where "kk \<subseteq> {1..n}" "(\<forall>j. a1 j = a0 j + (if j \<in> kk then 1 else 0))"
+            unfolding kle_def by blast
           then show ?thesis
             unfolding kle_def
             apply (rule_tac x=kk in exI)
@@ -2404,7 +2449,6 @@
             case goal1
             then show ?case
               apply -
-              apply (erule conjE)
               apply (erule_tac[!] x=j in allE)
               apply (cases "j \<in> kk")
               apply (case_tac[!] "j=k")
@@ -2481,9 +2525,16 @@
       unfolding mem_Collect_eq
     proof (erule conjE)
       fix s'
-      assume as: "ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
-      from this(2) guess a' .. note a' = this
-      guess a_min a_max by (rule ksimplex_extrema_strong[OF as assms(3)]) note min_max = this
+      assume as: "ksimplex p n s'"
+      assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
+      then obtain a' where a': "a' \<in> s'" "s' - {a'} = s - {a}" ..
+      obtain a_min a_max where min_max:
+          "a_min \<in> s'"
+          "a_max \<in> s'"
+          "a_min \<noteq> a_max"
+          "\<forall>x\<in>s'. kle n a_min x \<and> kle n x a_max"
+          "\<forall>i. a_max i = (if i \<in> {1..n} then a_min i + 1 else a_min i)"
+        by (rule ksimplex_extrema_strong[OF as assms(3)])
       have *: "\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a'
       proof
         fix x
@@ -2644,8 +2695,9 @@
     then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j)"
       using ksimplex_predecessor[OF assms(1-2)]
       by blast
-    then guess u .. from this(2) guess k .. note k = this[rule_format]
-    note u = `u \<in> s`
+    then obtain u k where u: "u \<in> s"
+      and k: "k \<in> {1..n}" "\<And>j. a j = (if j = k then u j + 1 else u j)"
+      by blast
     have "\<not> (\<forall>x\<in>s. kle n x a)"
     proof
       case goal1
@@ -2660,9 +2712,9 @@
     qed
     then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j)"
       using ksimplex_successor[OF assms(1-2)] by blast
-    then guess v .. from this(2) guess l ..
-    note l = this[rule_format]
-    note v = `v \<in> s`
+    then obtain v l where v: "v \<in> s"
+      and l: "l \<in> {1..n}" "\<And>j. v j = (if j = l then a j + 1 else a j)"
+      by blast
     def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j"
     have kl: "k \<noteq> l"
     proof
@@ -2969,10 +3021,12 @@
       unfolding mem_Collect_eq
     proof (erule conjE)
       fix s'
-      assume as: "ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
-      from this(2) guess a'' .. note a'' = this
+      assume as: "ksimplex p n s'"
+      assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
+      then obtain a'' where a'': "a'' \<in> s'" "s' - {a''} = s - {a}"
+        by blast
       have "u \<noteq> v"
-        unfolding fun_eq_iff unfolding l(2) k(2) by auto
+        unfolding fun_eq_iff l(2) k(2) by auto
       then have uv': "\<not> kle n v u"
         using uv using kle_antisym by auto
       have "u \<noteq> a" "v \<noteq> a"
@@ -2982,7 +3036,8 @@
       have lem6: "a \<in> s' \<or> a' \<in> s'"
       proof (cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
         case False
-        then guess w unfolding ball_simps .. note w = this
+        then obtain w where w: "w \<in> s'" "\<not> (kle n w u \<or> kle n v w)"
+          by blast
         then have "kle n u w" "kle n w v"
           using ksimplexD(6)[OF as] uvs' by auto
         then have "w = a' \<or> w = a"
@@ -3002,8 +3057,13 @@
         then have "\<exists>y\<in>s'. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then u j + 1 else u j)"
           using ksimplex_successor[OF as `u\<in>s'`]
           by blast
-        then guess w .. note w = this
-        from this(2) guess kk .. note kk = this[rule_format]
+        then obtain w where
+          w: "w \<in> s'" "\<exists>k\<in>{1..n}. \<forall>j. w j = (if j = k then u j + 1 else u j)"
+          ..
+        from this(2) obtain kk where kk:
+            "kk \<in> {1..n}"
+            "\<And>j. w j = (if j = kk then u j + 1 else u j)"
+          by blast
         have "\<not> kle n w u"
           apply -
           apply rule
@@ -3021,7 +3081,7 @@
           then show False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
             apply (erule_tac x=l in allE)
             using `k \<noteq> l`
-            apply auto  
+            apply auto
             done
         next
           case True
@@ -3171,11 +3231,12 @@
     done
   have *: "n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)"
     by auto
-  then guess N
+  then obtain N where N:
+      "N \<le> n \<and> (label x (N + 1) \<noteq> 0 \<or> n = N)"
+      "\<forall>m<N. \<not> (m \<le> n \<and> (label x (m + 1) \<noteq> 0 \<or> n = m))"
     apply (drule_tac num_WOP[of "\<lambda>j. j\<le>n \<and> (label x (j+1) \<noteq> 0 \<or> n = j)"])
-    apply (erule exE)
+    apply blast
     done
-  note N = this
   have N': "N \<le> n"
     "\<forall>i. 1 \<le> i \<and> i < N + 1 \<longrightarrow> label x i = 0" "N = n \<or> label x (N + 1) \<noteq> 0"
     defer
@@ -3183,10 +3244,10 @@
     fix i
     assume i: "1 \<le> i \<and> i < N + 1"
     then show "label x i = 0"
-      using N[THEN conjunct2,THEN spec[where x="i - 1"]]
+      using N(2)[THEN spec[where x="i - 1"]]
       using N
       by auto
-  qed (insert N, auto)
+  qed (insert N(1), auto)
   show ?t1 ?t2 ?t3
     unfolding reduced_def
     apply (rule_tac[!] someI2_ex)
@@ -3251,7 +3312,7 @@
     apply assumption
   proof (cases ?a)
     case True
-    then guess j .. note j = this
+    then obtain j where j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0" ..
     {
       fix x
       assume x: "x \<in> f"
@@ -3267,8 +3328,12 @@
     }
     moreover have "j - 1 \<in> {0..n}"
       using j by auto
-    then guess y unfolding `?l`[THEN conjunct1,symmetric] and image_iff .. note y = this
-    ultimately have False
+    then obtain y where y:
+      "y \<in> f"
+      "j - 1 = reduced lab (n + 1) y"
+      unfolding `?l`[THEN conjunct1,symmetric] and image_iff ..
+    ultimately
+    have False
       by auto
     then show "\<forall>x\<in>f. x (n + 1) = p"
       by auto
@@ -3276,7 +3341,7 @@
     case False
     then have ?b using `?l`
       by blast
-    then guess j .. note j = this
+    then obtain j where j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p" ..
     {
       fix x
       assume x: "x \<in> f"
@@ -3296,8 +3361,10 @@
       moreover
       have "n \<in> {0..n}"
         by auto
-      then guess y unfolding `?l`[THEN conjunct1,symmetric] image_iff ..
-      ultimately show False
+      then obtain y where "y \<in> f" "n = reduced lab (n + 1) y"
+        unfolding `?l`[THEN conjunct1,symmetric] image_iff ..
+      ultimately
+      show False
         using *[of y] by auto
     qed
     then show "\<forall>x\<in>f. x (n + 1) = p"
@@ -3368,8 +3435,9 @@
       unfolding image_iff
       apply auto
       done
-    moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] ..
-    then guess a ..
+    moreover
+    obtain s a where "ksimplex p (n + 1) s \<and> a \<in> s \<and> f = s - {a}"
+      using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] by blast
     ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and>
         a \<in> s \<and> f = s - {a} \<and>
         reduced lab (n + 1) ` f = {0..n} \<and>
@@ -3385,8 +3453,13 @@
     assume as: "\<exists>s a. ksimplex p (n + 1) s \<and>
       a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and>
       ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))"
-    then guess s ..
-    then guess a by (elim exE conjE) note sa = this
+    then obtain s a where sa:
+        "ksimplex p (n + 1) s"
+        "a \<in> s"
+        "f = s - {a}"
+        "reduced lab (n + 1) ` f = {0..n}"
+        "(\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p)"
+      by auto
     {
       fix x
       assume "x \<in> f"
@@ -3411,7 +3484,7 @@
     have *: "\<forall>x\<in>f. x (n + 1) = p"
     proof (cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
       case True
-      then guess j ..
+      then obtain j where "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0" ..
       then have "\<And>x. x \<in> f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1"
         apply -
         apply (rule reduced_labelling_zero)
@@ -3433,7 +3506,8 @@
     next
       case False
       then have "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p"
-        using sa(5) by fastforce then guess j .. note j=this
+        using sa(5) by fastforce
+      then obtain j where j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p" ..
       then show ?thesis
       proof (cases "j = n + 1")
         case False
@@ -3489,7 +3563,9 @@
   (is "?l = ?r")
 proof
   assume l: ?l
-  guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a = this
+  obtain a where a: "a \<in> s" "\<forall>y y'. y \<in> s \<and> y' \<in> s \<longrightarrow> y = y'"
+    using ksimplexD(3)[OF l, unfolded add_0]
+    unfolding card_1_exists ..
   have "a = (\<lambda>x. p)"
     using ksimplexD(5)[OF l, rule_format, OF a(1)]
     by rule auto
@@ -3566,7 +3642,13 @@
     unfolding card_eq_0_iff by auto
   then obtain s where "s \<in> ?A"
     by auto note s=conjD[OF this[unfolded mem_Collect_eq]]
-  guess a b by (rule ksimplex_extrema_strong[OF s(1) `n \<noteq> 0`]) note ab = this
+  obtain a b where ab:
+      "a \<in> s"
+      "b \<in> s"
+      "a \<noteq> b"
+      "\<forall>x\<in>s. kle n a x \<and> kle n x b"
+      "\<forall>i. b i = (if i \<in> {1..n} then a i + 1 else a i)"
+    by (rule ksimplex_extrema_strong[OF s(1) `n \<noteq> 0`])
   show ?thesis
     apply (rule that[of a])
     apply (rule_tac[!] ballI)
@@ -3590,10 +3672,12 @@
     case goal2
     then have "i \<in> reduced label n ` s"
       using s by auto
-    then guess u unfolding image_iff .. note u = this
+    then obtain u where u: "u \<in> s" "i = reduced label n u"
+      unfolding image_iff ..
     from goal2 have "i - 1 \<in> reduced label n ` s"
       using s by auto
-    then guess v unfolding image_iff .. note v = this
+    then obtain v where v: "v \<in> s" "i - 1 = reduced label n v"
+      unfolding image_iff ..
     show ?case
       apply (rule_tac x = u in exI)
       apply (rule_tac x = v in exI)
@@ -3680,16 +3764,24 @@
   assume "\<not> ?thesis"
   then have *: "\<not> (\<exists>x\<in>{0..\<Sum>Basis}. f x - x = 0)"
     by auto
-  guess d
+  obtain d where
+      d: "d > 0" "\<And>x. x \<in> {0..\<Sum>Basis} \<Longrightarrow> d \<le> norm (f x - x)"
     apply (rule brouwer_compactness_lemma[OF compact_interval _ *])
     apply (rule continuous_on_intros assms)+
+    apply blast
     done
-  note d = this [rule_format]
-  have *: "\<forall>x. x \<in> {0..\<Sum>Basis} \<longrightarrow> f x \<in> {0..\<Sum>Basis}"  "\<forall>x. x \<in> {0..(\<Sum>Basis)::'a} \<longrightarrow>
-    (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
+  have *: "\<forall>x. x \<in> {0..\<Sum>Basis} \<longrightarrow> f x \<in> {0..\<Sum>Basis}"
+    "\<forall>x. x \<in> {0..(\<Sum>Basis)::'a} \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
     using assms(2)[unfolded image_subset_iff Ball_def]
-    unfolding mem_interval by auto
-  guess label using kuhn_labelling_lemma[OF *] by (elim exE conjE)
+    unfolding mem_interval
+    by auto
+  obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
+    "\<forall>x. \<forall>i\<in>Basis. label x i \<le> 1"
+    "\<forall>x. \<forall>i\<in>Basis. x \<in> {0..\<Sum>Basis} \<and> True \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
+    "\<forall>x. \<forall>i\<in>Basis. x \<in> {0..\<Sum>Basis} \<and> True \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
+    "\<forall>x. \<forall>i\<in>Basis. x \<in> {0..\<Sum>Basis} \<and> True \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
+    "\<forall>x. \<forall>i\<in>Basis. x \<in> {0..\<Sum>Basis} \<and> True \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
+    using kuhn_labelling_lemma[OF *] by blast
   note label = this [rule_format]
   have lem1: "\<forall>x\<in>{0..\<Sum>Basis}.\<forall>y\<in>{0..\<Sum>Basis}.\<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
     abs (f x \<bullet> i - x \<bullet> i) \<le> norm (f y - f x) + norm (y - x)"
@@ -3760,8 +3852,15 @@
       done
     have *: "uniformly_continuous_on {0..\<Sum>Basis} f"
       by (rule compact_uniformly_continuous[OF assms(1) compact_interval])
-    guess e using *[unfolded uniformly_continuous_on_def,rule_format,OF d'] by (elim exE conjE)
-    note e=this[rule_format,unfolded dist_norm]
+    obtain e where e:
+        "e > 0"
+        "\<And>x x'. x \<in> {0..\<Sum>Basis} \<Longrightarrow>
+          x' \<in> {0..\<Sum>Basis} \<Longrightarrow>
+          norm (x' - x) < e \<Longrightarrow>
+          norm (f x' - f x) < d / real n / 8"
+      using *[unfolded uniformly_continuous_on_def,rule_format,OF d']
+      unfolding dist_norm
+      by blast
     show ?thesis
       apply (rule_tac x="min (e/2) (d/real n/8)" in exI)
       apply safe
@@ -3789,7 +3888,7 @@
           apply auto
           done
         show "\<bar>f x \<bullet> i - f z \<bullet> i\<bar> \<le> norm (f x - f z)" "\<bar>x \<bullet> i - z \<bullet> i\<bar> \<le> norm (x - z)"
-          unfolding inner_diff_left[symmetric]  
+          unfolding inner_diff_left[symmetric]
           by (rule Basis_le_norm[OF i])+
         have tria: "norm (y - x) \<le> norm (y - z) + norm (x - z)"
           using dist_triangle[of y x z, unfolded dist_norm]
@@ -3822,8 +3921,18 @@
       qed (insert as, auto)
     qed
   qed
-  then guess e by (elim exE conjE) note e=this[rule_format]
-  guess p using real_arch_simple[of "1 + real n / e"] .. note p=this
+  then
+  obtain e where e:
+    "e > 0"
+    "\<And>x y z i. x \<in> {0..\<Sum>Basis} \<Longrightarrow>
+      y \<in> {0..\<Sum>Basis} \<Longrightarrow>
+      z \<in> {0..\<Sum>Basis} \<Longrightarrow>
+      i \<in> Basis \<Longrightarrow>
+      norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<Longrightarrow>
+      \<bar>(f z - z) \<bullet> i\<bar> < d / real n"
+    by blast
+  obtain p :: nat where p: "1 + real n / e \<le> real p"
+    using real_arch_simple ..
   have "1 + real n / e > 0"
     apply (rule add_pos_pos)
     defer
@@ -3898,7 +4007,14 @@
         by (intro label(2)) (auto simp add: b'')
     }
   qed
-  guess q by (rule kuhn_lemma[OF q1 q2]) note q = this
+  obtain q where q:
+      "\<forall>i\<in>{1..n}. q i < p"
+      "\<forall>i\<in>{1..n}.
+         \<exists>r s. (\<forall>j\<in>{1..n}. q j \<le> r j \<and> r j \<le> q j + 1) \<and>
+               (\<forall>j\<in>{1..n}. q j \<le> s j \<and> s j \<le> q j + 1) \<and>
+               (label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) i \<noteq>
+               (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) i"
+    by (rule kuhn_lemma[OF q1 q2])
   def z \<equiv> "(\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)::'a"
   have "\<exists>i\<in>Basis. d / real n \<le> abs ((f z - z)\<bullet>i)"
   proof (rule ccontr)
@@ -3929,13 +4045,16 @@
     finally show False
       using d_fz_z by auto
   qed
-  then guess i .. note i = this
+  then obtain i where i: "i \<in> Basis" "d / real n \<le> \<bar>(f z - z) \<bullet> i\<bar>" ..
   have *: "b' i \<in> {1..n}"
-    using i
-    using b'[unfolded bij_betw_def]
+    using i and b'[unfolded bij_betw_def]
     by auto
-  guess r using q(2)[rule_format,OF *] ..
-  then guess s by (elim exE conjE) note rs = this[rule_format]
+  obtain r s where rs:
+    "\<And>j. j \<in> {1..n} \<Longrightarrow> q j \<le> r j \<and> r j \<le> q j + 1"
+    "\<And>j. j \<in> {1..n} \<Longrightarrow> q j \<le> s j \<and> s j \<le> q j + 1"
+    "(label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i) \<noteq>
+      (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i)"
+    using q(2)[rule_format,OF *] by blast
   have b'_im: "\<And>i. i \<in> Basis \<Longrightarrow>  b' i \<in> {1..n}"
     using b' unfolding bij_betw_def by auto
   def r' \<equiv> "(\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i)::'a"
@@ -4040,7 +4159,7 @@
     apply auto
     apply blast
     done
-  then guess x .. note x = this
+  then obtain x where x: "x \<in> s" "(i \<circ> g \<circ> r) x = x" ..
   then have *: "g (r x) \<in> t"
     using assms(4,8) by auto
   have "r ((i \<circ> g \<circ> r) x) = r x"
@@ -4062,8 +4181,16 @@
   shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
     (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
 proof -
-  guess r using assms[unfolded homeomorphic_def homeomorphism_def] ..
-  then guess i ..
+  obtain r i where
+      "\<forall>x\<in>s. i (r x) = x"
+      "r ` s = t"
+      "continuous_on s r"
+      "\<forall>y\<in>t. r (i y) = y"
+      "i ` t = s"
+      "continuous_on t i"
+    using assms
+    unfolding homeomorphic_def homeomorphism_def
+    by blast
   then show ?thesis
     apply -
     apply rule
@@ -4084,7 +4211,8 @@
     and "g ` t \<subseteq> t"
   obtains y where "y \<in> t" and "g y = y"
 proof -
-  guess h using assms(1) unfolding retract_of_def ..
+  obtain h where "retraction s t h"
+    using assms(1) unfolding retract_of_def ..
   then show ?thesis
     unfolding retraction_def
     apply -
@@ -4161,8 +4289,8 @@
     apply (rule_tac x=b in exI)
     apply (auto simp add: dist_norm)
     done
-  then guess e by (elim exE conjE)
-  note e = this
+  then obtain e where e: "e > 0" "s \<subseteq> cball 0 e"
+    by blast
   have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point s) x = x"
     apply (rule_tac brouwer_ball[OF e(1), of 0 "f \<circ> closest_point s"])
     apply (rule continuous_on_compose )
@@ -4174,7 +4302,7 @@
     using e(2)[unfolded subset_eq mem_cball]
     apply (auto simp add: dist_norm)
     done
-  then guess x .. note x=this
+  then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point s) x = x" ..
   have *: "closest_point s x = x"
     apply (rule closest_point_self)
     apply (rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"], unfolded image_iff])
@@ -4203,7 +4331,9 @@
   case goal1
   have *: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
     using scaleR_left_distrib[of 1 1 a] by auto
-  guess x
+  obtain x where x:
+      "x \<in> {x. norm (a - x) = e}"
+      "2 *\<^sub>R a - x = x"
     apply (rule retract_fixpoint_property[OF goal1, of "\<lambda>x. scaleR 2 a - x"])
     apply rule
     apply rule
@@ -4219,8 +4349,8 @@
     apply (erule bexE)
     unfolding dist_norm
     apply (simp add: * norm_minus_commute)
+    apply blast
     done
-  note x = this
   then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
     by (auto simp add: algebra_simps)
   then have "a = x"
diff -r 241c6a2fdda1 -r 23d2cbac6dce src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Feb 16 18:46:13 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Feb 16 21:09:47 2014 +0100
@@ -1158,7 +1158,7 @@
   by (rule convex_box_cart) (simp add: atLeast_def[symmetric] convex_real_interval)
 
 lemma unit_interval_convex_hull_cart:
-  "{0::real^'n .. 1} = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}" (is "?int = convex hull ?points")
+  "{0::real^'n .. 1} = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}"
   unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"]
   by (rule arg_cong[where f="\<lambda>x. convex hull x"]) (simp add: Basis_vec_def inner_axis)
 
@@ -1167,8 +1167,11 @@
   obtains s::"(real^'n) set"
     where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s"
 proof -
-  from cube_convex_hull [OF assms, of x] guess s .
-  with that[of s] show thesis by (simp add: const_vector_cart)
+  from assms obtain s where "finite s"
+    and "{x - setsum (op *\<^sub>R d) Basis..x + setsum (op *\<^sub>R d) Basis} = convex hull s"
+    by (rule cube_convex_hull)
+  with that[of s] show thesis
+    by (simp add: const_vector_cart)
 qed
 
 
diff -r 241c6a2fdda1 -r 23d2cbac6dce src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Feb 16 18:46:13 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Feb 16 21:09:47 2014 +0100
@@ -256,7 +256,12 @@
     using t by auto
   have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0"
     using m by auto
-  from `open S` [THEN ereal_openE] guess l u . note T = this
+  from `open S` [THEN ereal_openE]
+  obtain l u where T:
+      "open (ereal -` S)"
+      "\<infinity> \<in> S \<Longrightarrow> {ereal l<..} \<subseteq> S"
+      "- \<infinity> \<in> S \<Longrightarrow> {..<ereal u} \<subseteq> S"
+    by blast
   let ?f = "(\<lambda>x. m * x + t)"
   show ?thesis
     unfolding open_ereal_def
diff -r 241c6a2fdda1 -r 23d2cbac6dce src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Feb 16 18:46:13 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Feb 16 21:09:47 2014 +0100
@@ -139,12 +139,12 @@
     and f :: "'a set \<Rightarrow> 'a"
   assumes "topological_basis B"
     and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
-  shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))"
+  shows "\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X)"
 proof (intro allI impI)
   fix X :: "'a set"
   assume "open X" and "X \<noteq> {}"
   from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]]
-  guess B' . note B' = this
+  obtain B' where "B' \<in> B" "f X \<in> B'" "B' \<subseteq> X" .
   then show "\<exists>B'\<in>B. f B' \<in> X"
     by (auto intro!: choosefrom_basis)
 qed
@@ -166,8 +166,12 @@
     from open_prod_elim[OF `open S` this]
     obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
       by (metis mem_Sigma_iff)
-    moreover from topological_basisE[OF A a] guess A0 .
-    moreover from topological_basisE[OF B b] guess B0 .
+    moreover
+    from A a obtain A0 where "A0 \<in> A" "x \<in> A0" "A0 \<subseteq> a"
+      by (rule topological_basisE)
+    moreover
+    from B b obtain B0 where "B0 \<in> B" "y \<in> B0" "B0 \<subseteq> b"
+      by (rule topological_basisE)
     ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)"
       by (intro UN_I[of "(A0, B0)"]) auto
   qed auto
@@ -225,7 +229,12 @@
     "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
     "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A"
 proof atomize_elim
-  from first_countable_basisE[of x] guess A' . note A' = this
+  obtain A' where A':
+    "countable A'"
+    "\<And>a. a \<in> A' \<Longrightarrow> x \<in> a"
+    "\<And>a. a \<in> A' \<Longrightarrow> open a"
+    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S"
+    by (rule first_countable_basisE) blast
   def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
   then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and>
         (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)"
@@ -273,8 +282,18 @@
 instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
 proof
   fix x :: "'a \<times> 'b"
-  from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this
-  from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this
+  obtain A where A:
+      "countable A"
+      "\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a"
+      "\<And>a. a \<in> A \<Longrightarrow> open a"
+      "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
+    by (rule first_countable_basisE[of "fst x"]) blast
+  obtain B where B:
+      "countable B"
+      "\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a"
+      "\<And>a. a \<in> B \<Longrightarrow> open a"
+      "\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S"
+    by (rule first_countable_basisE[of "snd x"]) blast
   show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set.
     (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
   proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
@@ -286,10 +305,14 @@
   next
     fix S
     assume "open S" "x \<in> S"
-    from open_prod_elim[OF this] guess a' b' . note a'b' = this
-    moreover from a'b' A(4)[of a'] B(4)[of b']
-    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
-    ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
+    then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S"
+      by (rule open_prod_elim)
+    moreover
+    from a'b' A(4)[of a'] B(4)[of b']
+    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
+      by auto
+    ultimately
+    show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
       by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
   qed (simp add: A B)
 qed
@@ -328,7 +351,9 @@
       next
         case (UN K)
         then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto
-        then guess k unfolding bchoice_iff ..
+        then obtain k where
+            "\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> UNION (k ka) Inter = ka"
+          unfolding bchoice_iff ..
         then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
           by (intro exI[of _ "UNION K k"]) auto
       next
@@ -849,14 +874,16 @@
     from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
     show "?th i" by auto
   qed
-  from choice[OF this] guess a .. note a = this
+  from choice[OF this] obtain a where
+    a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" ..
   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
   proof
     fix i
     from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
     show "?th i" by auto
   qed
-  from choice[OF this] guess b .. note b = this
+  from choice[OF this] obtain b where
+    b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" ..
   let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
   show ?thesis
   proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
@@ -1585,7 +1612,11 @@
     (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  from countable_basis_at_decseq[of x] guess A . note A = this
+  from countable_basis_at_decseq[of x] obtain A where A:
+      "\<And>i. open (A i)"
+      "\<And>i. x \<in> A i"
+      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
+    by blast
   def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
   {
     fix n
@@ -2759,8 +2790,12 @@
   assumes l: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> range f)"
   shows "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
 proof -
-  from countable_basis_at_decseq[of l] guess A . note A = this
-
+  from countable_basis_at_decseq[of l]
+  obtain A where A:
+      "\<And>i. open (A i)"
+      "\<And>i. l \<in> A i"
+      "\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
+    by blast
   def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> f j \<in> A (Suc n)"
   {
     fix n i
@@ -3043,8 +3078,10 @@
   show "?R (\<lambda>x. True)"
     by (rule exI[of _ "{}"]) (simp add: le_fun_def)
 next
-  fix P Q assume "?R P" then guess X ..
-  moreover assume "?R Q" then guess Y ..
+  fix P Q
+  assume "?R P" then guess X ..
+  moreover
+  assume "?R Q" then guess Y ..
   ultimately show "?R (\<lambda>x. P x \<and> Q x)"
     by (intro exI[of _ "X \<union> Y"]) auto
 next
@@ -3221,7 +3258,8 @@
     using * by metis
   then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
     by (auto simp: C_def)
-  then guess f unfolding bchoice_iff Bex_def ..
+  then obtain f where "\<forall>t\<in>T. f t \<in> A \<and> t \<inter> U \<subseteq> f t"
+    unfolding bchoice_iff Bex_def ..
   with T show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
     unfolding C_def by (intro exI[of _ "f`T"]) fastforce
 qed
@@ -3231,9 +3269,10 @@
 proof (rule countably_compact_imp_compact)
   fix T and x :: 'a
   assume "open T" "x \<in> T"
-  from topological_basisE[OF is_basis this] guess b .
+  from topological_basisE[OF is_basis this] obtain b where
+    "b \<in> (SOME B. countable B \<and> topological_basis B)" "x \<in> b" "b \<subseteq> T" .
   then show "\<exists>b\<in>SOME B. countable B \<and> topological_basis B. x \<in> b \<and> b \<inter> U \<subseteq> T"
-    by auto
+    by blast
 qed (insert countable_basis topological_basis_open[OF is_basis], auto)
 
 lemma countably_compact_eq_compact:
@@ -3354,7 +3393,12 @@
   obtain x where "x \<in> U" and x: "inf (nhds x) (filtermap X sequentially) \<noteq> bot" (is "?F \<noteq> _")
     using `compact U` by (auto simp: compact_filter)
 
-  from countable_basis_at_decseq[of x] guess A . note A = this
+  from countable_basis_at_decseq[of x]
+  obtain A where A:
+      "\<And>i. open (A i)"
+      "\<And>i. x \<in> A i"
+      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
+    by blast
   def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> X j \<in> A (Suc n)"
   {
     fix n i
@@ -3426,7 +3470,9 @@
   moreover
   from `countable t` have "countable C"
     unfolding C_def by (auto intro: countable_Collect_finite_subset)
-  ultimately guess D by (rule countably_compactE)
+  ultimately
+  obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> \<Union>D"
+    by (rule countably_compactE)
   then obtain E where E: "E \<subseteq> {F. finite F \<and> F \<subseteq> t }" "finite E"
     and s: "s \<subseteq> (\<Union>F\<in>E. interior (F \<union> (- t)))"
     by (metis (lifting) Union_image_eq finite_subset_image C_def)
@@ -3569,7 +3615,8 @@
   shows "compact s"
 proof -
   from seq_compact_imp_totally_bounded[OF `seq_compact s`]
-  guess f unfolding choice_iff' .. note f = this
+  obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` f e)"
+    unfolding choice_iff' ..
   def K \<equiv> "(\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"
   have "countably_compact s"
     using `seq_compact s` by (rule seq_compact_imp_countably_compact)
@@ -3944,7 +3991,9 @@
         assume "infinite {n. f n \<in> U}"
         then have "\<exists>b\<in>k (e n). infinite {i\<in>{n. f n \<in> U}. f i \<in> ball b (e n)}"
           using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)
-        then guess a ..
+        then obtain a where
+          "a \<in> k (e n)"
+          "infinite {i \<in> {n. f n \<in> U}. f i \<in> ball a (e n)}" ..
         then have "\<exists>b. infinite {i. f i \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"
           by (intro exI[of _ "ball a (e n) \<inter> U"] exI[of _ a]) (auto simp: ac_simps)
         from someI_ex[OF this]
@@ -6617,7 +6666,7 @@
   shows "\<exists>S\<subseteq>A. card S = n"
 proof cases
   assume "finite A"
-  from ex_bij_betw_nat_finite[OF this] guess f .. note f = this
+  from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..<card A} A" ..
   moreover from f `n \<le> card A` have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
     by (auto simp: bij_betw_def intro: subset_inj_on)
   ultimately have "f ` {..< n} \<subseteq> A" "card (f ` {..< n}) = n"
@@ -6642,7 +6691,11 @@
       inj_on f {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
     using dim_substandard[of d] t d assms
     by (intro subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"]]) (auto simp: inner_Basis)
-  then guess f by (elim exE conjE) note f = this
+  then obtain f where f:
+      "linear f"
+      "f ` {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s"
+      "inj_on f {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
+    by blast
   interpret f: bounded_linear f
     using f unfolding linear_conv_bounded_linear by auto
   {