# HG changeset patch
# User paulson
# Date 1598715033 -3600
# Node ID 5e26a4bca0c2d9f370c127213a159c6b87bd91d9
# Parent  d36c109bc7738c43602406c6ebc0e153f260cec8# Parent  341b15d092f2515462b98444900580f8e0d752f6
merged

diff -r d36c109bc773 -r 5e26a4bca0c2 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Fri Aug 28 16:14:19 2020 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Sat Aug 29 16:30:33 2020 +0100
@@ -15,15 +15,7 @@
 
 text \<open>Combination of Elementary and Abstract Topology\<close>
 
-(* FIXME: move elsewhere *)
-
-lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
-  apply auto
-  apply (rule_tac x="d/2" in exI)
-  apply auto
-  done
-
-lemma approachable_lt_le2:  \<comment> \<open>like the above, but pushes aside an extra formula\<close>
+lemma approachable_lt_le2: 
     "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
   apply auto
   apply (rule_tac x="d/2" in exI, auto)
@@ -251,10 +243,8 @@
       from \<open>finite D\<close> show "finite ?D"
         by (rule finite_imageI)
       from \<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D"
-        apply (rule subset_trans, clarsimp)
-        apply (frule subsetD [OF \<open>D \<subseteq> ?C\<close>, THEN f_inv_into_f])
-        apply (erule rev_bexI, fast)
-        done
+        apply (rule subset_trans)
+        by (metis Int_Union Int_lower2 \<open>D \<subseteq> (\<inter>) S ` C\<close> image_inv_into_cancel)
     qed
     then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
   qed
@@ -587,9 +577,7 @@
 proof -
   have [simp]: "S \<inter> f -` f ` S = S" by auto
   show ?thesis
-    using ope [OF T]
-    apply (simp add: continuous_on_open)
-    by (meson ope openin_imp_subset openin_trans)
+    by (meson T continuous_on_open_gen ope openin_imp_subset)
 qed
 
 lemma quotient_map_imp_continuous_closed:
@@ -601,9 +589,7 @@
 proof -
   have [simp]: "S \<inter> f -` f ` S = S" by auto
   show ?thesis
-    using ope [OF T]
-    apply (simp add: continuous_on_closed)
-    by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
+    by (meson T closedin_imp_subset continuous_on_closed_gen ope)
 qed
 
 lemma open_map_imp_quotient_map:
@@ -1612,5 +1598,4 @@
     connected_component_of_set X x = connected_component_of_set X y"
   by (meson connected_component_of_nonoverlap)
 
-
 end
\ No newline at end of file
diff -r d36c109bc773 -r 5e26a4bca0c2 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Fri Aug 28 16:14:19 2020 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Sat Aug 29 16:30:33 2020 +0100
@@ -294,9 +294,8 @@
 lemma islimpt_approachable_le: "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x \<le> e)"
   for x :: "'a::metric_space"
   unfolding islimpt_approachable
-  using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x",
-    THEN arg_cong [where f=Not]]
-  by (simp add: Bex_def conj_commute conj_left_commute)
+  using approachable_lt_le2 [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x" and Q="\<lambda>x. True"]
+  by auto
 
 lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \<Longrightarrow> x islimpt S"
   for x :: "'a::metric_space"
@@ -613,22 +612,12 @@
   assume ?lhs
   then show ?rhs
     unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
-    apply auto
-    apply (erule_tac x=e in allE, auto)
-    apply (rule_tac x=d in exI, auto)
-    apply (erule_tac x=xa in allE)
-    apply (auto simp: dist_commute)
-    done
+    by (metis dist_commute dist_pos_lt dist_self)
 next
   assume ?rhs
   then show ?lhs
     unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
-    apply auto
-    apply (erule_tac x=e in allE, auto)
-    apply (rule_tac x=d in exI, auto)
-    apply (erule_tac x="f xa" in allE)
-    apply (auto simp: dist_commute)
-    done
+    by (metis dist_commute)
 qed
 
 text\<open>Define setwise continuity in terms of limits within the set.\<close>
@@ -830,12 +819,8 @@
     have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
     then have "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"
       by (simp add: f(1))
-    have "dist x y \<le> a"
-      apply (rule Lim_dist_ubound [of sequentially f])
-      apply (rule trivial_limit_sequentially)
-      apply (rule f(2))
-      apply fact
-      done
+    then have "dist x y \<le> a"
+      using Lim_dist_ubound f(2) trivial_limit_sequentially by blast
   }
   then show ?thesis
     unfolding bounded_def by auto
@@ -845,10 +830,7 @@
   by (simp add: bounded_subset closure_subset image_mono)
 
 lemma bounded_cball[simp,intro]: "bounded (cball x e)"
-  apply (simp add: bounded_def)
-  apply (rule_tac x=x in exI)
-  apply (rule_tac x=e in exI, auto)
-  done
+  unfolding bounded_def  using mem_cball by blast
 
 lemma bounded_ball[simp,intro]: "bounded (ball x e)"
   by (metis ball_subset_cball bounded_cball bounded_subset)
@@ -860,7 +842,7 @@
   by (induct rule: finite_induct[of F]) auto
 
 lemma bounded_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. bounded (B x) \<Longrightarrow> bounded (\<Union>x\<in>A. B x)"
-  by (induct set: finite) auto
+  by auto
 
 lemma bounded_insert [simp]: "bounded (insert x S) \<longleftrightarrow> bounded S"
 proof -
@@ -940,48 +922,48 @@
   using assms centre_in_ball closure_iff_nhds_not_empty by blast
 
 lemma compact_sup_maxdistance:
-  fixes s :: "'a::metric_space set"
-  assumes "compact s"
-    and "s \<noteq> {}"
-  shows "\<exists>x\<in>s. \<exists>y\<in>s. \<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
+  fixes S :: "'a::metric_space set"
+  assumes "compact S"
+    and "S \<noteq> {}"
+  shows "\<exists>x\<in>S. \<exists>y\<in>S. \<forall>u\<in>S. \<forall>v\<in>S. dist u v \<le> dist x y"
 proof -
-  have "compact (s \<times> s)"
-    using \<open>compact s\<close> by (intro compact_Times)
-  moreover have "s \<times> s \<noteq> {}"
-    using \<open>s \<noteq> {}\<close> by auto
-  moreover have "continuous_on (s \<times> s) (\<lambda>x. dist (fst x) (snd x))"
+  have "compact (S \<times> S)"
+    using \<open>compact S\<close> by (intro compact_Times)
+  moreover have "S \<times> S \<noteq> {}"
+    using \<open>S \<noteq> {}\<close> by auto
+  moreover have "continuous_on (S \<times> S) (\<lambda>x. dist (fst x) (snd x))"
     by (intro continuous_at_imp_continuous_on ballI continuous_intros)
   ultimately show ?thesis
-    using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
+    using continuous_attains_sup[of "S \<times> S" "\<lambda>x. dist (fst x) (snd x)"] by auto
 qed
 
 
 subsubsection\<open>Totally bounded\<close>
 
-lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (s m) (s n) < e)"
+lemma cauchy_def: "Cauchy S \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (S m) (S n) < e)"
   unfolding Cauchy_def by metis
 
 proposition seq_compact_imp_totally_bounded:
-  assumes "seq_compact s"
-  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
+  assumes "seq_compact S"
+  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>k. ball x e)"
 proof -
-  { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"
-    let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
+  { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> S \<Longrightarrow> \<not> S \<subseteq> (\<Union>x\<in>k. ball x e)"
+    let ?Q = "\<lambda>x n r. r \<in> S \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
     have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
     proof (rule dependent_wellorder_choice)
       fix n x assume "\<And>y. y < n \<Longrightarrow> ?Q x y (x y)"
-      then have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
+      then have "\<not> S \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
         using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
-      then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)"
+      then obtain z where z:"z\<in>S" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)"
         unfolding subset_eq by auto
       show "\<exists>r. ?Q x n r"
         using z by auto
     qed simp
-    then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)"
+    then obtain x where "\<forall>n::nat. x n \<in> S" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)"
       by blast
-    then obtain l r where "l \<in> s" and r:"strict_mono  r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"
+    then obtain l r where "l \<in> S" and r:"strict_mono  r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"
       using assms by (metis seq_compact_def)
-    from this(3) have "Cauchy (x \<circ> r)"
+    then have "Cauchy (x \<circ> r)"
       using LIMSEQ_imp_Cauchy by auto
     then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
       unfolding cauchy_def using \<open>e > 0\<close> by blast
@@ -994,17 +976,17 @@
 subsubsection\<open>Heine-Borel theorem\<close>
 
 proposition seq_compact_imp_Heine_Borel:
-  fixes s :: "'a :: metric_space set"
-  assumes "seq_compact s"
-  shows "compact s"
+  fixes S :: "'a :: metric_space set"
+  assumes "seq_compact S"
+  shows "compact S"
 proof -
-  from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>]
-  obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)"
+  from seq_compact_imp_totally_bounded[OF \<open>seq_compact S\<close>]
+  obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>f e. ball x e)"
     unfolding choice_iff' ..
   define K where "K = (\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"
-  have "countably_compact s"
-    using \<open>seq_compact s\<close> by (rule seq_compact_imp_countably_compact)
-  then show "compact s"
+  have "countably_compact S"
+    using \<open>seq_compact S\<close> by (rule seq_compact_imp_countably_compact)
+  then show "compact S"
   proof (rule countably_compact_imp_compact)
     show "countable K"
       unfolding K_def using f
@@ -1013,22 +995,22 @@
     show "\<forall>b\<in>K. open b" by (auto simp: K_def)
   next
     fix T x
-    assume T: "open T" "x \<in> T" and x: "x \<in> s"
+    assume T: "open T" "x \<in> T" and x: "x \<in> S"
     from openE[OF T] obtain e where "0 < e" "ball x e \<subseteq> T"
       by auto
-    then have "0 < e / 2" "ball x (e / 2) \<subseteq> T"
+    then have "0 < e/2" "ball x (e/2) \<subseteq> T"
       by auto
-    from Rats_dense_in_real[OF \<open>0 < e / 2\<close>] obtain r where "r \<in> \<rat>" "0 < r" "r < e / 2"
+    from Rats_dense_in_real[OF \<open>0 < e/2\<close>] obtain r where "r \<in> \<rat>" "0 < r" "r < e/2"
       by auto
-    from f[rule_format, of r] \<open>0 < r\<close> \<open>x \<in> s\<close> obtain k where "k \<in> f r" "x \<in> ball k r"
+    from f[rule_format, of r] \<open>0 < r\<close> \<open>x \<in> S\<close> obtain k where "k \<in> f r" "x \<in> ball k r"
       by auto
     from \<open>r \<in> \<rat>\<close> \<open>0 < r\<close> \<open>k \<in> f r\<close> have "ball k r \<in> K"
       by (auto simp: K_def)
-    then show "\<exists>b\<in>K. x \<in> b \<and> b \<inter> s \<subseteq> T"
+    then show "\<exists>b\<in>K. x \<in> b \<and> b \<inter> S \<subseteq> T"
     proof (rule bexI[rotated], safe)
       fix y
       assume "y \<in> ball k r"
-      with \<open>r < e / 2\<close> \<open>x \<in> ball k r\<close> have "dist x y < e"
+      with \<open>r < e/2\<close> \<open>x \<in> ball k r\<close> have "dist x y < e"
         by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute)
       with \<open>ball x e \<subseteq> T\<close> show "y \<in> T"
         by auto
@@ -1039,7 +1021,7 @@
 qed
 
 proposition compact_eq_seq_compact_metric:
-  "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
+  "compact (S :: 'a::metric_space set) \<longleftrightarrow> seq_compact S"
   using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast
 
 proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
@@ -1050,22 +1032,14 @@
 subsubsection \<open>Complete the chain of compactness variants\<close>
 
 proposition compact_eq_Bolzano_Weierstrass:
-  fixes s :: "'a::metric_space set"
-  shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"
-  (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    using Heine_Borel_imp_Bolzano_Weierstrass[of s] by auto
-next
-  assume ?rhs
-  then show ?lhs
-    unfolding compact_eq_seq_compact_metric by (rule Bolzano_Weierstrass_imp_seq_compact)
-qed
+  fixes S :: "'a::metric_space set"
+  shows "compact S \<longleftrightarrow> (\<forall>T. infinite T \<and> T \<subseteq> S \<longrightarrow> (\<exists>x \<in> S. x islimpt T))"
+  using Bolzano_Weierstrass_imp_seq_compact Heine_Borel_imp_Bolzano_Weierstrass compact_eq_seq_compact_metric 
+  by blast
 
 proposition Bolzano_Weierstrass_imp_bounded:
-  "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
-  using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass .
+  "(\<And>T. \<lbrakk>infinite T; T \<subseteq> S\<rbrakk> \<Longrightarrow> (\<exists>x \<in> S. x islimpt T)) \<Longrightarrow> bounded S"
+  using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass by metis
 
 
 subsection \<open>Banach fixed point theorem\<close>
@@ -1182,9 +1156,9 @@
     then have "e > 0"
       unfolding e_def using zero_le_dist[of "f x" x]
       by (metis dist_eq_0_iff dist_nz e_def)
-    then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e / 2"
+    then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e/2"
       using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto
-    then have N':"dist (z N) x < e / 2" by auto
+    then have N':"dist (z N) x < e/2" by auto
     have *: "c * dist (z N) x \<le> dist (z N) x"
       unfolding mult_le_cancel_right2
       using zero_le_dist[of "z N" x] and c
@@ -1194,7 +1168,7 @@
       using z_in_s[of N] \<open>x\<in>s\<close>
       using c
       by auto
-    also have "\<dots> < e / 2"
+    also have "\<dots> < e/2"
       using N' and c using * by auto
     finally show False
       unfolding fzn
@@ -1218,43 +1192,43 @@
 
 subsection \<open>Edelstein fixed point theorem\<close>
 
-theorem edelstein_fix:\<comment> \<open>TODO: rename to \<open>Edelstein_fix\<close>\<close>
-  fixes s :: "'a::metric_space set"
-  assumes s: "compact s" "s \<noteq> {}"
-    and gs: "(g ` s) \<subseteq> s"
-    and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
-  shows "\<exists>!x\<in>s. g x = x"
+theorem Edelstein_fix:
+  fixes S :: "'a::metric_space set"
+  assumes S: "compact S" "S \<noteq> {}"
+    and gs: "(g ` S) \<subseteq> S"
+    and dist: "\<forall>x\<in>S. \<forall>y\<in>S. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
+  shows "\<exists>!x\<in>S. g x = x"
 proof -
-  let ?D = "(\<lambda>x. (x, x)) ` s"
+  let ?D = "(\<lambda>x. (x, x)) ` S"
   have D: "compact ?D" "?D \<noteq> {}"
     by (rule compact_continuous_image)
-       (auto intro!: s continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)
-
-  have "\<And>x y e. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 < e \<Longrightarrow> dist y x < e \<Longrightarrow> dist (g y) (g x) < e"
+       (auto intro!: S continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)
+
+  have "\<And>x y e. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> 0 < e \<Longrightarrow> dist y x < e \<Longrightarrow> dist (g y) (g x) < e"
     using dist by fastforce
-  then have "continuous_on s g"
+  then have "continuous_on S g"
     by (auto simp: continuous_on_iff)
   then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
     unfolding continuous_on_eq_continuous_within
     by (intro continuous_dist ballI continuous_within_compose)
        (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image)
 
-  obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
+  obtain a where "a \<in> S" and le: "\<And>x. x \<in> S \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
     using continuous_attains_inf[OF D cont] by auto
 
   have "g a = a"
   proof (rule ccontr)
     assume "g a \<noteq> a"
-    with \<open>a \<in> s\<close> gs have "dist (g (g a)) (g a) < dist (g a) a"
+    with \<open>a \<in> S\<close> gs have "dist (g (g a)) (g a) < dist (g a) a"
       by (intro dist[rule_format]) auto
     moreover have "dist (g a) a \<le> dist (g (g a)) (g a)"
-      using \<open>a \<in> s\<close> gs by (intro le) auto
+      using \<open>a \<in> S\<close> gs by (intro le) auto
     ultimately show False by auto
   qed
-  moreover have "\<And>x. x \<in> s \<Longrightarrow> g x = x \<Longrightarrow> x = a"
-    using dist[THEN bspec[where x=a]] \<open>g a = a\<close> and \<open>a\<in>s\<close> by auto
-  ultimately show "\<exists>!x\<in>s. g x = x"
-    using \<open>a \<in> s\<close> by blast
+  moreover have "\<And>x. x \<in> S \<Longrightarrow> g x = x \<Longrightarrow> x = a"
+    using dist[THEN bspec[where x=a]] \<open>g a = a\<close> and \<open>a\<in>S\<close> by auto
+  ultimately show "\<exists>!x\<in>S. g x = x"
+    using \<open>a \<in> S\<close> by blast
 qed
 
 subsection \<open>The diameter of a set\<close>
@@ -1270,72 +1244,68 @@
 
 lemma diameter_le:
   assumes "S \<noteq> {} \<or> 0 \<le> d"
-      and no: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> norm(x - y) \<le> d"
-    shows "diameter S \<le> d"
-using assms
+    and no: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> norm(x - y) \<le> d"
+  shows "diameter S \<le> d"
+  using assms
   by (auto simp: dist_norm diameter_def intro: cSUP_least)
 
 lemma diameter_bounded_bound:
-  fixes s :: "'a :: metric_space set"
-  assumes s: "bounded s" "x \<in> s" "y \<in> s"
-  shows "dist x y \<le> diameter s"
+  fixes S :: "'a :: metric_space set"
+  assumes S: "bounded S" "x \<in> S" "y \<in> S"
+  shows "dist x y \<le> diameter S"
 proof -
-  from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
+  from S obtain z d where z: "\<And>x. x \<in> S \<Longrightarrow> dist z x \<le> d"
     unfolding bounded_def by auto
-  have "bdd_above (case_prod dist ` (s\<times>s))"
+  have "bdd_above (case_prod dist ` (S\<times>S))"
   proof (intro bdd_aboveI, safe)
     fix a b
-    assume "a \<in> s" "b \<in> s"
+    assume "a \<in> S" "b \<in> S"
     with z[of a] z[of b] dist_triangle[of a b z]
     show "dist a b \<le> 2 * d"
       by (simp add: dist_commute)
   qed
-  moreover have "(x,y) \<in> s\<times>s" using s by auto
-  ultimately have "dist x y \<le> (SUP (x,y)\<in>s\<times>s. dist x y)"
+  moreover have "(x,y) \<in> S\<times>S" using S by auto
+  ultimately have "dist x y \<le> (SUP (x,y)\<in>S\<times>S. dist x y)"
     by (rule cSUP_upper2) simp
-  with \<open>x \<in> s\<close> show ?thesis
+  with \<open>x \<in> S\<close> show ?thesis
     by (auto simp: diameter_def)
 qed
 
 lemma diameter_lower_bounded:
-  fixes s :: "'a :: metric_space set"
-  assumes s: "bounded s"
-    and d: "0 < d" "d < diameter s"
-  shows "\<exists>x\<in>s. \<exists>y\<in>s. d < dist x y"
+  fixes S :: "'a :: metric_space set"
+  assumes S: "bounded S"
+    and d: "0 < d" "d < diameter S"
+  shows "\<exists>x\<in>S. \<exists>y\<in>S. d < dist x y"
 proof (rule ccontr)
   assume contr: "\<not> ?thesis"
-  moreover have "s \<noteq> {}"
+  moreover have "S \<noteq> {}"
     using d by (auto simp: diameter_def)
-  ultimately have "diameter s \<le> d"
+  ultimately have "diameter S \<le> d"
     by (auto simp: not_less diameter_def intro!: cSUP_least)
-  with \<open>d < diameter s\<close> show False by auto
+  with \<open>d < diameter S\<close> show False by auto
 qed
 
 lemma diameter_bounded:
-  assumes "bounded s"
-  shows "\<forall>x\<in>s. \<forall>y\<in>s. dist x y \<le> diameter s"
-    and "\<forall>d>0. d < diameter s \<longrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. dist x y > d)"
-  using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms
+  assumes "bounded S"
+  shows "\<forall>x\<in>S. \<forall>y\<in>S. dist x y \<le> diameter S"
+    and "\<forall>d>0. d < diameter S \<longrightarrow> (\<exists>x\<in>S. \<exists>y\<in>S. dist x y > d)"
+  using diameter_bounded_bound[of S] diameter_lower_bounded[of S] assms
   by auto
 
-lemma bounded_two_points:
-  "bounded S \<longleftrightarrow> (\<exists>e. \<forall>x\<in>S. \<forall>y\<in>S. dist x y \<le> e)"
-  apply (rule iffI)
-  subgoal using diameter_bounded(1) by auto
-  subgoal using bounded_any_center[of S] by meson
-  done
+lemma bounded_two_points: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>x\<in>S. \<forall>y\<in>S. dist x y \<le> e)"
+  by (meson bounded_def diameter_bounded(1))
 
 lemma diameter_compact_attained:
-  assumes "compact s"
-    and "s \<noteq> {}"
-  shows "\<exists>x\<in>s. \<exists>y\<in>s. dist x y = diameter s"
+  assumes "compact S"
+    and "S \<noteq> {}"
+  shows "\<exists>x\<in>S. \<exists>y\<in>S. dist x y = diameter S"
 proof -
-  have b: "bounded s" using assms(1)
+  have b: "bounded S" using assms(1)
     by (rule compact_imp_bounded)
-  then obtain x y where xys: "x\<in>s" "y\<in>s"
-    and xy: "\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
+  then obtain x y where xys: "x\<in>S" "y\<in>S"
+    and xy: "\<forall>u\<in>S. \<forall>v\<in>S. dist u v \<le> dist x y"
     using compact_sup_maxdistance[OF assms] by auto
-  then have "diameter s \<le> dist x y"
+  then have "diameter S \<le> dist x y"
     unfolding diameter_def
     apply clarsimp
     apply (rule cSUP_least, fast+)
@@ -1477,41 +1447,30 @@
     "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
 
 proposition bounded_closed_imp_seq_compact:
-  fixes s::"'a::heine_borel set"
-  assumes "bounded s"
-    and "closed s"
-  shows "seq_compact s"
+  fixes S::"'a::heine_borel set"
+  assumes "bounded S"
+    and "closed S"
+  shows "seq_compact S"
 proof (unfold seq_compact_def, clarify)
   fix f :: "nat \<Rightarrow> 'a"
-  assume f: "\<forall>n. f n \<in> s"
-  with \<open>bounded s\<close> have "bounded (range f)"
+  assume f: "\<forall>n. f n \<in> S"
+  with \<open>bounded S\<close> have "bounded (range f)"
     by (auto intro: bounded_subset)
   obtain l r where r: "strict_mono (r :: nat \<Rightarrow> nat)" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
     using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto
-  from f have fr: "\<forall>n. (f \<circ> r) n \<in> s"
+  from f have fr: "\<forall>n. (f \<circ> r) n \<in> S"
     by simp
-  have "l \<in> s" using \<open>closed s\<close> fr l
+  have "l \<in> S" using \<open>closed S\<close> fr l
     by (rule closed_sequentially)
-  show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
-    using \<open>l \<in> s\<close> r l by blast
+  show "\<exists>l\<in>S. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+    using \<open>l \<in> S\<close> r l by blast
 qed
 
 lemma compact_eq_bounded_closed:
-  fixes s :: "'a::heine_borel set"
-  shows "compact s \<longleftrightarrow> bounded s \<and> closed s"
-  (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    using compact_imp_closed compact_imp_bounded
-    by blast
-next
-  assume ?rhs
-  then show ?lhs
-    using bounded_closed_imp_seq_compact[of s]
-    unfolding compact_eq_seq_compact_metric
-    by auto
-qed
+  fixes S :: "'a::heine_borel set"
+  shows "compact S \<longleftrightarrow> bounded S \<and> closed S"
+  using bounded_closed_imp_seq_compact compact_eq_seq_compact_metric compact_imp_bounded compact_imp_closed 
+  by auto
 
 lemma compact_Inter:
   fixes \<F> :: "'a :: heine_borel set set"
@@ -1675,7 +1634,7 @@
           using n M by auto
         moreover have "r n \<ge> N"
           using lr'[of n] n by auto
-        then have "dist (f n) ((f \<circ> r) n) < e / 2"
+        then have "dist (f n) ((f \<circ> r) n) < e/2"
           using N and n by auto
         ultimately have "dist (f n) l < e" using n M
           by metric
@@ -1754,12 +1713,8 @@
       moreover have "\<forall>i. (f \<circ> t) i \<in> s"
         using f by auto
       moreover
-      {
-        fix n
-        have "(f \<circ> t) n \<in> F n"
-          by (cases n) (simp_all add: t_def sel)
-      }
-      note t = this
+      have t: "(f \<circ> t) n \<in> F n" for n
+        by (cases n) (simp_all add: t_def sel)
 
       have "Cauchy (f \<circ> t)"
       proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE)
@@ -2467,7 +2422,7 @@
       by (simp add: field_simps)
     also have "... < e/2"
       using N2 \<open>0 < e\<close> by (simp add: field_simps)
-    finally have "dist (f (r (max N1 N2))) x < e / 2" .
+    finally have "dist (f (r (max N1 N2))) x < e/2" .
     moreover have "dist (f (r (max N1 N2))) l < e/2"
       using N1 max.cobounded1 by blast
     ultimately have "dist x l < e"
@@ -2491,7 +2446,7 @@
   obtain d where d_pos: "\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk> \<Longrightarrow> 0 < d x e"
      and d_dist : "\<And>x x' e f. \<lbrakk>dist x' x < d x e; x \<in> S; x' \<in> S; 0 < e; f \<in> \<F>\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
     using cont by metis
-  let ?\<G> = "((\<lambda>x. ball x (d x (e / 2))) ` S)"
+  let ?\<G> = "((\<lambda>x. ball x (d x (e/2))) ` S)"
   have Ssub: "S \<subseteq> \<Union> ?\<G>"
     by clarsimp (metis d_pos \<open>0 < e\<close> dist_self half_gt_zero_iff)
   then obtain k where "0 < k" and k: "\<And>x. x \<in> S \<Longrightarrow> \<exists>G \<in> ?\<G>. ball x k \<subseteq> G"
@@ -2501,7 +2456,7 @@
     obtain G where "G \<in> ?\<G>" "u \<in> G" "v \<in> G"
       using k that
       by (metis \<open>dist v u < k\<close> \<open>u \<in> S\<close> \<open>0 < k\<close> centre_in_ball subsetD dist_commute mem_ball)
-    then obtain w where w: "dist w u < d w (e / 2)" "dist w v < d w (e / 2)" "w \<in> S"
+    then obtain w where w: "dist w u < d w (e/2)" "dist w v < d w (e/2)" "w \<in> S"
       by auto
     with that d_dist have "dist (f w) (f v) < e/2"
       by (metis \<open>0 < e\<close> dist_commute half_gt_zero)
@@ -2646,7 +2601,7 @@
     show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l"
     proof (rule tendstoI)
       fix e::real assume "e > 0"
-      define e' where "e' \<equiv> e / 2"
+      define e' where "e' \<equiv> e/2"
       have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
 
       have "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) l < e'"
diff -r d36c109bc773 -r 5e26a4bca0c2 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Fri Aug 28 16:14:19 2020 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Sat Aug 29 16:30:33 2020 +0100
@@ -822,14 +822,10 @@
 
 lemma interior_singleton [simp]: "interior {a} = {}"
   for a :: "'a::perfect_space"
-  apply (rule interior_unique, simp_all)
-  using not_open_singleton subset_singletonD
-  apply fastforce
-  done
+  by (meson interior_eq interior_subset not_open_singleton subset_singletonD)
 
 lemma interior_Int [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
-  by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
-    Int_lower2 interior_maximal interior_subset open_Int open_interior)
+  by (meson Int_mono Int_subset_iff antisym_conv interior_maximal interior_subset open_Int open_interior)
 
 lemma eventually_nhds_in_nhd: "x \<in> interior s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
   using interior_subset[of s] by (subst eventually_nhds) blast
@@ -2586,10 +2582,7 @@
   then have "g ` t = s" by auto
   ultimately show ?thesis
     unfolding homeomorphism_def homeomorphic_def
-    apply (rule_tac x=g in exI)
-    using g and assms(3) and continuous_on_inv[OF assms(2,1), of g, unfolded assms(3)] and assms(2)
-    apply auto
-    done
+    using assms continuous_on_inv by fastforce
 qed
 
 lemma homeomorphic_compact: