# HG changeset patch
# User paulson
# Date 1672775735 0
# Node ID c0459ee8220c27420b7961a6466a985c3857c54f
# Parent  b3c5bc06f5be3c203fedf1d8dcdb166003a72955# Parent  498d8babe7164883ee22ffaaffb13139c452a2ce
merged

diff -r b3c5bc06f5be -r c0459ee8220c src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Jan 03 18:23:52 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Jan 03 19:55:35 2023 +0000
@@ -17,9 +17,7 @@
 
 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)
-  done
+by (meson dense less_eq_real_def order_le_less_trans)
 
 lemma triangle_lemma:
   fixes x y z :: real
@@ -88,13 +86,18 @@
   qed
 qed
 
+lemma islimpt_closure:
+  "\<lbrakk>S \<subseteq> T; \<And>x. \<lbrakk>x islimpt S; x \<in> T\<rbrakk> \<Longrightarrow> x \<in> S\<rbrakk> \<Longrightarrow> S = T \<inter> closure S"
+  using closure_def by fastforce
+
 lemma closedin_limpt:
   "closedin (top_of_set T) S \<longleftrightarrow> S \<subseteq> T \<and> (\<forall>x. x islimpt S \<and> x \<in> T \<longrightarrow> x \<in> S)"
-  apply (simp add: closedin_closed, safe)
-   apply (simp add: closed_limpt islimpt_subset)
-  apply (rule_tac x="closure S" in exI, simp)
-  apply (force simp: closure_def)
-  done
+proof -
+  have "\<And>U x. \<lbrakk>closed U; S = T \<inter> U; x islimpt S; x \<in> T\<rbrakk> \<Longrightarrow> x \<in> S"
+    by (meson IntI closed_limpt inf_le2 islimpt_subset)
+  then show ?thesis
+    by (metis closed_closure closedin_closed closedin_imp_subset islimpt_closure)
+qed
 
 lemma closedin_closed_eq: "closed S \<Longrightarrow> closedin (top_of_set S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S"
   by (meson closedin_limpt closed_subset closedin_closed_trans)
@@ -104,8 +107,8 @@
     \<Longrightarrow> connected S \<longleftrightarrow> (\<nexists>A B. closed A \<and> closed B \<and> A \<noteq> {} \<and> B \<noteq> {} \<and> A \<union> B = S \<and> A \<inter> B = {})"
   unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
 
-text \<open>If a connnected set is written as the union of two nonempty closed sets, then these sets
-have to intersect.\<close>
+text \<open>If a connnected set is written as the union of two nonempty closed sets, 
+  then these sets have to intersect.\<close>
 
 lemma connected_as_closed_union:
   assumes "connected C" "C = A \<union> B" "closed A" "closed B" "A \<noteq> {}" "B \<noteq> {}"
@@ -128,10 +131,7 @@
 
 lemma closedin_compact_eq:
   fixes S :: "'a::t2_space set"
-  shows
-   "compact S
-         \<Longrightarrow> (closedin (top_of_set S) T \<longleftrightarrow>
-              compact T \<and> T \<subseteq> S)"
+  shows "compact S \<Longrightarrow> (closedin (top_of_set S) T \<longleftrightarrow> compact T \<and> T \<subseteq> S)"
 by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
 
 
@@ -174,12 +174,11 @@
   fix x and A and V
   assume "x \<in> S" "V \<subseteq> A" "open V" "x \<in> V" "T \<inter> A = {}"
   then have "openin (top_of_set S) (A \<inter> V \<inter> S)"
-    by (auto simp: openin_open intro!: exI[where x="V"])
+    by (simp add: inf_absorb2 openin_subtopology_Int)
   moreover have "A \<inter> V \<inter> S \<noteq> {}" using \<open>x \<in> V\<close> \<open>V \<subseteq> A\<close> \<open>x \<in> S\<close>
     by auto
-  ultimately have "T \<inter> (A \<inter> V \<inter> S) \<noteq> {}"
-    by (rule assms)
-  with \<open>T \<inter> A = {}\<close> show False by auto
+  ultimately show False
+    using \<open>T \<inter> A = {}\<close> assms by fastforce
 qed
 
 
@@ -192,10 +191,10 @@
   by (auto simp: frontier_of_def frontier_def)
 
 lemma connected_Int_frontier:
-     "\<lbrakk>connected s; s \<inter> t \<noteq> {}; s - t \<noteq> {}\<rbrakk> \<Longrightarrow> (s \<inter> frontier t \<noteq> {})"
+     "\<lbrakk>connected S; S \<inter> T \<noteq> {}; S - T \<noteq> {}\<rbrakk> \<Longrightarrow> S \<inter> frontier T \<noteq> {}"
   apply (simp add: frontier_interiors connected_openin, safe)
-  apply (drule_tac x="s \<inter> interior t" in spec, safe)
-   apply (drule_tac [2] x="s \<inter> interior (-t)" in spec)
+  apply (drule_tac x="S \<inter> interior T" in spec, safe)
+   apply (drule_tac [2] x="S \<inter> interior (-T)" in spec)
    apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD])
   done
 
@@ -203,8 +202,7 @@
 
 lemma openin_delete:
   fixes a :: "'a :: t1_space"
-  shows "openin (top_of_set u) s
-         \<Longrightarrow> openin (top_of_set u) (s - {a})"
+  shows "openin (top_of_set u) S \<Longrightarrow> openin (top_of_set u) (S - {a})"
 by (metis Int_Diff open_delete openin_open)
 
 lemma compact_eq_openin_cover:
@@ -241,8 +239,7 @@
       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)
-        by (metis Int_Union Int_lower2 \<open>D \<subseteq> (\<inter>) S ` C\<close> image_inv_into_cancel)
+        by (metis \<open>D \<subseteq> (\<inter>) S ` C\<close> image_inv_into_cancel inf_Sup le_infE)
     qed
     then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
   qed
@@ -332,49 +329,47 @@
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuity relative to a union.\<close>
 
 lemma continuous_on_Un_local:
-    "\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t;
-      continuous_on s f; continuous_on t f\<rbrakk>
-     \<Longrightarrow> continuous_on (s \<union> t) f"
+    "\<lbrakk>closedin (top_of_set (S \<union> T)) S; closedin (top_of_set (S \<union> T)) T;
+      continuous_on S f; continuous_on T f\<rbrakk>
+     \<Longrightarrow> continuous_on (S \<union> T) f"
   unfolding continuous_on closedin_limpt
   by (metis Lim_trivial_limit Lim_within_union Un_iff trivial_limit_within)
 
 lemma continuous_on_cases_local:
-     "\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t;
-       continuous_on s f; continuous_on t g;
-       \<And>x. \<lbrakk>x \<in> s \<and> \<not>P x \<or> x \<in> t \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk>
-      \<Longrightarrow> continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
+     "\<lbrakk>closedin (top_of_set (S \<union> T)) S; closedin (top_of_set (S \<union> T)) T;
+       continuous_on S f; continuous_on T g;
+       \<And>x. \<lbrakk>x \<in> S \<and> \<not>P x \<or> x \<in> T \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk>
+      \<Longrightarrow> continuous_on (S \<union> T) (\<lambda>x. if P x then f x else g x)"
   by (rule continuous_on_Un_local) (auto intro: continuous_on_eq)
 
 lemma continuous_on_cases_le:
   fixes h :: "'a :: topological_space \<Rightarrow> real"
-  assumes "continuous_on {t \<in> s. h t \<le> a} f"
-      and "continuous_on {t \<in> s. a \<le> h t} g"
-      and h: "continuous_on s h"
-      and "\<And>t. \<lbrakk>t \<in> s; h t = a\<rbrakk> \<Longrightarrow> f t = g t"
-    shows "continuous_on s (\<lambda>t. if h t \<le> a then f(t) else g(t))"
+  assumes "continuous_on {x \<in> S. h x \<le> a} f"
+      and "continuous_on {x \<in> S. a \<le> h x} g"
+      and h: "continuous_on S h"
+      and "\<And>x. \<lbrakk>x \<in> S; h x = a\<rbrakk> \<Longrightarrow> f x = g x"
+    shows "continuous_on S (\<lambda>x. if h x \<le> a then f(x) else g(x))"
 proof -
-  have s: "s = (s \<inter> h -` atMost a) \<union> (s \<inter> h -` atLeast a)"
+  have S: "S = (S \<inter> h -` atMost a) \<union> (S \<inter> h -` atLeast a)"
     by force
-  have 1: "closedin (top_of_set s) (s \<inter> h -` atMost a)"
+  have 1: "closedin (top_of_set S) (S \<inter> h -` atMost a)"
     by (rule continuous_closedin_preimage [OF h closed_atMost])
-  have 2: "closedin (top_of_set s) (s \<inter> h -` atLeast a)"
+  have 2: "closedin (top_of_set S) (S \<inter> h -` atLeast a)"
     by (rule continuous_closedin_preimage [OF h closed_atLeast])
-  have eq: "s \<inter> h -` {..a} = {t \<in> s. h t \<le> a}" "s \<inter> h -` {a..} = {t \<in> s. a \<le> h t}"
+  have [simp]: "S \<inter> h -` {..a} = {x \<in> S. h x \<le> a}" "S \<inter> h -` {a..} = {x \<in> S. a \<le> h x}"
     by auto
-  show ?thesis
-    apply (rule continuous_on_subset [of s, OF _ order_refl])
-    apply (subst s)
-    apply (rule continuous_on_cases_local)
-    using 1 2 s assms apply (auto simp: eq)
-    done
+  have "continuous_on (S \<inter> h -` {..a} \<union> S \<inter> h -` {a..}) (\<lambda>x. if h x \<le> a then f x else g x)"
+    by (intro continuous_on_cases_local) (use 1 2 S assms in auto)
+  then show ?thesis
+    using S by force
 qed
 
 lemma continuous_on_cases_1:
-  fixes s :: "real set"
-  assumes "continuous_on {t \<in> s. t \<le> a} f"
-      and "continuous_on {t \<in> s. a \<le> t} g"
-      and "a \<in> s \<Longrightarrow> f a = g a"
-    shows "continuous_on s (\<lambda>t. if t \<le> a then f(t) else g(t))"
+  fixes S :: "real set"
+  assumes "continuous_on {t \<in> S. t \<le> a} f"
+      and "continuous_on {t \<in> S. a \<le> t} g"
+      and "a \<in> S \<Longrightarrow> f a = g a"
+    shows "continuous_on S (\<lambda>t. if t \<le> a then f(t) else g(t))"
 using assms
 by (auto intro: continuous_on_cases_le [where h = id, simplified])
 
@@ -504,8 +499,7 @@
     show "\<exists>\<U>\<subseteq>\<B> - {{}}. T = \<Union>\<U>" if "openin (top_of_set S) T" for T
       using \<B> [OF that]
       apply clarify
-      apply (rule_tac x="\<U> - {{}}" in exI, auto)
-        done
+      by (rule_tac x="\<U> - {{}}" in exI, auto)
   qed auto
 qed
 
@@ -666,16 +660,15 @@
       and "U \<subseteq> f ` S"
     shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
            openin (top_of_set (f ` S)) U"
-apply (rule continuous_right_inverse_imp_quotient_map)
-using assms apply force+
-done
+  using assms 
+  by (intro continuous_right_inverse_imp_quotient_map) auto
 
 lemma continuous_imp_quotient_map:
   fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
   assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
     shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
            openin (top_of_set T) U"
-  by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
+  by (simp add: assms closed_map_imp_quotient_map continuous_imp_closed_map)
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Pasting lemmas for functions, for of casewise definitions\<close>
 
@@ -747,14 +740,11 @@
     by auto
   have 1: "(\<Union>i\<in>I. T i \<inter> f i -` U) \<subseteq> topspace X"
     using T by blast
-  then have lf: "locally_finite_in X ((\<lambda>i. T i \<inter> f i -` U) ` I)"
+  then have "locally_finite_in X ((\<lambda>i. T i \<inter> f i -` U) ` I)"
     unfolding locally_finite_in_def
     using finite_subset [OF sub] fin by force
-  show "closedin X (topspace X \<inter> g -` U)"
-    apply (subst *)
-    apply (rule closedin_locally_finite_Union)
-     apply (auto intro: cTf lf)
-    done
+  then show "closedin X (topspace X \<inter> g -` U)"
+    by (smt (verit, best) * cTf closedin_locally_finite_Union image_iff)
 qed
 
 subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close>
@@ -784,10 +774,8 @@
 next
   fix x i
   assume "i \<in> I" and "x \<in> topspace X \<inter> T i"
-  show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
-    apply (rule someI2_ex)
-    using \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> apply blast
-    by (meson Int_iff \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> f)
+  then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
+    by (metis (mono_tags, lifting) IntE IntI f someI2)
 qed
 
 lemma pasting_lemma_exists_closed:
@@ -824,26 +812,19 @@
   show "?f i x = ?f j x"
     if "i \<in> {True,False}" "j \<in> {True,False}" and x: "x \<in> topspace X \<inter> ?T i \<inter> ?T j" for i j x
   proof -
-    have "f x = g x"
-      if "i" "\<not> j"
-      apply (rule fg)
-      unfolding frontier_of_closures eq
-      using x that closure_of_restrict by fastforce
+    have "f x = g x" if "i" "\<not> j"
+      by (smt (verit, best) Diff_Diff_Int closure_of_interior_of closure_of_restrict eq fg 
+          frontier_of_closures interior_of_complement that x)
     moreover
     have "g x = f x"
       if "x \<in> X closure_of {x. \<not> P x}" "x \<in> X closure_of Collect P" "\<not> i" "j" for x
-        apply (rule fg [symmetric])
-        unfolding frontier_of_closures eq
-        using x that closure_of_restrict by fastforce
+      by (metis IntI closure_of_restrict eq fg frontier_of_closures that)
     ultimately show ?thesis
       using that by (auto simp flip: closure_of_restrict)
   qed
   show "\<exists>j. j \<in> {True,False} \<and> x \<in> ?T j \<and> (if P x then f x else g x) = ?f j x"
     if "x \<in> topspace X" for x
-    apply simp
-    apply safe
-    apply (metis Int_iff closure_of inf_sup_absorb mem_Collect_eq that)
-    by (metis DiffI eq closure_of_subset_Int contra_subsetD mem_Collect_eq that)
+    by simp (metis in_closure_of mem_Collect_eq that)
 qed (auto simp: f g)
 
 lemma continuous_map_cases_alt:
@@ -877,8 +858,7 @@
     show "continuous_map (subtopology X ?T) Y g"
       by (simp add: contg)
     have "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> X closure_of {x \<in> topspace X. p x \<in> topspace Z - U}"
-      apply (rule closure_of_mono)
-      using continuous_map_closedin contp by fastforce
+      by (smt (verit, del_insts) DiffI mem_Collect_eq subset_iff closure_of_mono continuous_map_closedin contp) 
     then show "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> ?T"
       by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]])
   qed
@@ -1047,10 +1027,8 @@
   unfolding retract_of_def retraction_def by force
 
 lemma retraction_comp:
-   "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
-        \<Longrightarrow> retraction S U (g \<circ> f)"
-apply (auto simp: retraction_def intro: continuous_on_compose2)
-by blast
+   "\<lbrakk>retraction S T f; retraction T U g\<rbrakk> \<Longrightarrow> retraction S U (g \<circ> f)"
+  by (smt (verit, best) comp_apply continuous_on_compose image_comp retraction subset_iff)
 
 lemma retract_of_trans [trans]:
   assumes "S retract_of T" and "T retract_of U"
@@ -1092,12 +1070,15 @@
   by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
 
 lemma retraction_openin_vimage_iff:
-  "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
-  if retraction: "retraction S T r" and "U \<subseteq> T"
-  using retraction apply (rule retractionE)
-  apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
-  using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
-  done
+  assumes r: "retraction S T r" and "U \<subseteq> T"
+  shows "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    using r retraction_def retractionE
+    by (smt (verit, best) continuous_right_inverse_imp_quotient_map retraction_subset \<open>U \<subseteq> T\<close>)
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (meson continuous_openin_preimage r retraction_def)
+qed
 
 lemma retract_of_Times:
    "\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
@@ -1317,11 +1298,13 @@
 qed
 
 lemma path_connectedin_discrete_topology:
-  "path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
-  apply safe
-  using path_connectedin_subset_topspace apply fastforce
-   apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
-  using subset_singletonD by fastforce
+  "path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
+  show "?rhs \<Longrightarrow> ?lhs"
+    using subset_singletonD by fastforce
+qed
 
 lemma path_connected_space_discrete_topology:
    "path_connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
@@ -1444,17 +1427,14 @@
   have "connected_component_of_set X x = \<Union> {T. connectedin X T \<and> x \<in> T}"
     by (auto simp: connected_component_of_def)
   then show ?thesis
-    apply (rule ssubst)
-    by (blast intro: connectedin_Union)
+    by (metis (no_types, lifting) InterI connectedin_Union emptyE mem_Collect_eq)
 qed
 
 
 lemma Union_connected_components_of:
    "\<Union>(connected_components_of X) = topspace X"
   unfolding connected_components_of_def
-  apply (rule equalityI)
-  apply (simp add: SUP_least connected_component_of_subset_topspace)
-  using connected_component_of_refl by fastforce
+  using connected_component_in_topspace connected_component_of_refl by fastforce
 
 lemma connected_components_of_maximal:
    "\<lbrakk>C \<in> connected_components_of X; connectedin X S; ~disjnt C S\<rbrakk> \<Longrightarrow> S \<subseteq> C"
@@ -1465,15 +1445,13 @@
 lemma pairwise_disjoint_connected_components_of:
    "pairwise disjnt (connected_components_of X)"
   unfolding connected_components_of_def pairwise_def
-  apply clarify
-  by (metis connected_component_of_disjoint connected_component_of_equiv)
+  by (smt (verit, best) connected_component_of_disjoint connected_component_of_eq imageE)
 
 lemma complement_connected_components_of_Union:
    "C \<in> connected_components_of X
       \<Longrightarrow> topspace X - C = \<Union> (connected_components_of X - {C})"
-  apply (rule equalityI)
-  using Union_connected_components_of apply fastforce
-  by (metis Diff_cancel Diff_subset Union_connected_components_of cSup_singleton diff_Union_pairwise_disjoint equalityE insert_subsetI pairwise_disjoint_connected_components_of)
+  by (metis Union_connected_components_of bot.extremum ccpo_Sup_singleton diff_Union_pairwise_disjoint
+      insert_subset pairwise_disjoint_connected_components_of)
 
 lemma nonempty_connected_components_of:
    "C \<in> connected_components_of X \<Longrightarrow> C \<noteq> {}"
@@ -1495,16 +1473,18 @@
 qed
 
 lemma connected_component_in_connected_components_of:
-   "connected_component_of_set X a \<in> connected_components_of X \<longleftrightarrow> a \<in> topspace X"
-  apply (rule iffI)
-  using connected_component_of_eq_empty nonempty_connected_components_of apply fastforce
-  by (simp add: connected_components_of_def)
+  "connected_component_of_set X a \<in> connected_components_of X \<longleftrightarrow> a \<in> topspace X"
+  by (metis (no_types, lifting) connected_component_of_eq_empty connected_components_of_def image_iff)
 
 lemma connected_space_iff_components_eq:
    "connected_space X \<longleftrightarrow> (\<forall>C \<in> connected_components_of X. \<forall>C' \<in> connected_components_of X. C = C')"
-  apply (rule iffI)
-  apply (force simp: connected_components_of_def connected_space_connected_component_set image_iff)
-  by (metis connected_component_in_connected_components_of connected_component_of_refl connected_space_iff_connected_component mem_Collect_eq)
+          (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (simp add: connected_components_of_def connected_space_connected_component_set)
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (metis Union_connected_components_of Union_iff connected_space_subconnected connectedin_connected_components_of)
+qed
 
 lemma connected_components_of_eq_empty:
    "connected_components_of X = {} \<longleftrightarrow> topspace X = {}"
@@ -1522,10 +1502,11 @@
     by (simp add: connected_components_of_empty_space connected_space_topspace_empty)
 next
   case False
-  then show ?thesis
-    by (metis (no_types, opaque_lifting) Union_connected_components_of ccpo_Sup_singleton
-        connected_components_of_eq_empty connected_space_iff_components_eq insertI1 singletonD
-        subsetI subset_singleton_iff)
+  then have "\<lbrakk>connected_components_of X \<subseteq> {S}\<rbrakk> \<Longrightarrow> topspace X = S"
+    by (metis Sup_empty Union_connected_components_of ccpo_Sup_singleton subset_singleton_iff)
+  with False show ?thesis
+    unfolding connected_components_of_def
+    by (metis connected_space_connected_component_set empty_iff image_subset_iff insert_iff)
 qed
 
 lemma connected_space_iff_components_subset_singleton:
diff -r b3c5bc06f5be -r c0459ee8220c src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Tue Jan 03 18:23:52 2023 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Tue Jan 03 19:55:35 2023 +0000
@@ -757,8 +757,8 @@
       have "N > C" if "u N \<ge> n" for N
       proof (rule ccontr)
         assume "\<not>(N > C)"
-        have "u N \<le> Max {u n| n. n \<le> C}"
-          apply (rule Max_ge) using \<open>\<not>(N > C)\<close> by auto
+        then have "u N \<le> Max {u n| n. n \<le> C}"
+          using Max_ge by (simp add: setcompr_eq_image not_less)
         then show False using \<open>u N \<ge> n\<close> \<open>n \<ge> M\<close> unfolding M_def by auto
       qed
       then have **: "{N. u N \<ge> n} \<subseteq> {C..}" by fastforce
@@ -782,7 +782,7 @@
   then obtain N1 where N1: "\<And>N. N \<ge> N1 \<Longrightarrow> u N \<ge> n + 1"
     using eventually_sequentially by auto
   have "{N. u N \<le> n} \<subseteq> {..<N1}"
-    apply auto using N1 by (metis Suc_eq_plus1 not_less not_less_eq_eq)
+    by (metis (no_types, lifting) N1 Suc_eq_plus1 lessThan_iff less_le_not_le mem_Collect_eq nle_le not_less_eq_eq subset_eq)
   then show "finite {N. u N \<le> n}" by (simp add: finite_subset)
 qed
 
@@ -794,7 +794,7 @@
   {
     fix N0::nat
     have "N0 \<le> Max {N. u N \<le> n}" if "n \<ge> u N0" for n
-      apply (rule Max.coboundedI) using pseudo_inverse_finite_set[OF assms] that by auto
+      by (simp add: assms pseudo_inverse_finite_set that)
     then have "eventually (\<lambda>n. N0 \<le> Max {N. u N \<le> n}) sequentially"
       using eventually_sequentially by blast
   }
@@ -895,12 +895,12 @@
   "continuous_on (UNIV::ereal set) abs"
 proof -
   have "continuous_on ({..0} \<union> {(0::ereal)..}) abs"
-    apply (rule continuous_on_closed_Un, auto)
-    apply (rule iffD1[OF continuous_on_cong, of "{..0}" _ "\<lambda>x. -x"])
-    using less_eq_ereal_def apply (auto simp: continuous_uminus_ereal)
-    apply (rule iffD1[OF continuous_on_cong, of "{0..}" _ "\<lambda>x. x"])
-      apply (auto)
-    done
+  proof (intro continuous_on_closed_Un continuous_intros)
+    show "continuous_on {..0::ereal} abs"
+      by (metis abs_ereal_ge0 abs_ereal_less0 continuous_on_eq antisym_conv1 atMost_iff continuous_uminus_ereal ereal_uminus_zero)
+    show "continuous_on {0::ereal..} abs"
+      by (metis abs_ereal_ge0 atLeast_iff continuous_on_eq continuous_on_id)
+  qed
   moreover have "(UNIV::ereal set) = {..0} \<union> {(0::ereal)..}" by auto
   ultimately show ?thesis by auto
 qed
@@ -926,7 +926,7 @@
   shows "((\<lambda>n. u n - v n) \<longlongrightarrow> l - m) F"
 proof -
   have "((\<lambda>n. e2ennreal(enn2ereal(u n) - enn2ereal(v n))) \<longlongrightarrow> e2ennreal(enn2ereal l - enn2ereal m)) F"
-    apply (intro tendsto_intros) using assms by  auto
+    by (intro tendsto_intros) (use assms in auto)
   then show ?thesis by auto
 qed
 
@@ -936,8 +936,7 @@
   shows "((\<lambda>n. u n * v n) \<longlongrightarrow> l * m) F"
 proof -
   have "((\<lambda>n. e2ennreal(enn2ereal (u n) * enn2ereal (v n))) \<longlongrightarrow> e2ennreal(enn2ereal l * enn2ereal m)) F"
-    apply (intro tendsto_intros) using assms apply auto
-    using enn2ereal_inject zero_ennreal.rep_eq by fastforce+
+    by (intro tendsto_intros) (use assms enn2ereal_inject zero_ennreal.rep_eq in fastforce)+
   moreover have "e2ennreal(enn2ereal (u n) * enn2ereal (v n)) = u n * v n" for n
     by (subst times_ennreal.abs_eq[symmetric], auto simp: eq_onp_same_args)
   moreover have "e2ennreal(enn2ereal l * enn2ereal m)  = l * m"
@@ -1095,25 +1094,8 @@
   {
     fix S :: "ereal set"
     assume om: "open S" "mono_set S" "x0 \<in> S"
-    {
-      assume "S = UNIV"
-      then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
-        by auto
-    }
-    moreover
-    {
-      assume "S \<noteq> UNIV"
-      then obtain B where B: "S = {B<..}"
-        using om ereal_open_mono_set by auto
-      then have "B < x0"
-        using om by auto
-      then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
-        unfolding B
-        using \<open>x0 \<le> liminf x\<close> liminf_bounded_iff
-        by auto
-    }
-    ultimately have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
-      by auto
+    then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S"
+        by (metis \<open>x0 \<le> liminf x\<close> ereal_open_mono_set greaterThan_iff liminf_bounded_iff om UNIV_I)
   }
   then show "?P x0"
     by auto
@@ -1126,9 +1108,9 @@
 proof -
   obtain C where C: "limsup u < C" "C < \<infinity>" using assms ereal_dense2 by blast
   then have "C = ereal(real_of_ereal C)" using ereal_real by force
-  have "eventually (\<lambda>n. u n < C) sequentially" using C(1) unfolding Limsup_def
-    apply (auto simp: INF_less_iff)
-    using SUP_lessD eventually_mono by fastforce
+  have "eventually (\<lambda>n. u n < C) sequentially" 
+    using SUP_lessD eventually_mono C(1)
+    by (fastforce simp: INF_less_iff Limsup_def)
   then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> u n < C" using eventually_sequentially by auto
   define D where "D = max (real_of_ereal C) (Max {u n |n. n \<le> N})"
   have "\<And>n. u n \<le> D"
@@ -1156,9 +1138,9 @@
 proof -
   obtain C where C: "liminf u > C" "C > -\<infinity>" using assms using ereal_dense2 by blast
   then have "C = ereal(real_of_ereal C)" using ereal_real by force
-  have "eventually (\<lambda>n. u n > C) sequentially" using C(1) unfolding Liminf_def
-    apply (auto simp: less_SUP_iff)
-    using eventually_elim2 less_INF_D by fastforce
+  have "eventually (\<lambda>n. u n > C) sequentially" 
+    using eventually_elim2 less_INF_D C(1) 
+    by (fastforce simp: less_SUP_iff Liminf_def)
   then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> u n > C" using eventually_sequentially by auto
   define D where "D = min (real_of_ereal C) (Min {u n |n. n \<le> N})"
   have "\<And>n. u n \<ge> D"
@@ -1172,7 +1154,8 @@
       assume "\<not>(n \<le> N)"
       then have "n \<ge> N" by simp
       then have "u n > C" using N by auto
-      then have "u n > real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
+      then have "u n > real_of_ereal C" 
+        using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
       then show "u n \<ge> D" unfolding D_def by linarith
     qed
   qed
@@ -1189,12 +1172,12 @@
   "limsup (\<lambda>n. u (n+1)) = limsup u"
 proof -
   have "(SUP m\<in>{n+1..}. u m) = (SUP m\<in>{n..}. u (m + 1))" for n
-    apply (rule SUP_eq) using Suc_le_D by auto
+    by (rule SUP_eq) (use Suc_le_D in auto)
   then have a: "(INF n. SUP m\<in>{n..}. u (m + 1)) = (INF n. (SUP m\<in>{n+1..}. u m))" by auto
   have b: "(INF n. (SUP m\<in>{n+1..}. u m)) = (INF n\<in>{1..}. (SUP m\<in>{n..}. u m))"
-    apply (rule INF_eq) using Suc_le_D by auto
+    by (rule INF_eq) (use Suc_le_D in auto)
   have "(INF n\<in>{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
-    apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
+    by (rule INF_eq) (use \<open>decseq v\<close> decseq_Suc_iff in auto)
   moreover have "decseq (\<lambda>n. (SUP m\<in>{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
   ultimately have c: "(INF n\<in>{1..}. (SUP m\<in>{n..}. u m)) = (INF n. (SUP m\<in>{n..}. u m))" by simp
   have "(INF n. Sup (u ` {n..})) = (INF n. SUP m\<in>{n..}. u (m + 1))" using a b c by simp
@@ -1213,12 +1196,12 @@
   "liminf (\<lambda>n. u (n+1)) = liminf u"
 proof -
   have "(INF m\<in>{n+1..}. u m) = (INF m\<in>{n..}. u (m + 1))" for n
-    apply (rule INF_eq) using Suc_le_D by (auto)
+    by (rule INF_eq) (use Suc_le_D in auto)
   then have a: "(SUP n. INF m\<in>{n..}. u (m + 1)) = (SUP n. (INF m\<in>{n+1..}. u m))" by auto
   have b: "(SUP n. (INF m\<in>{n+1..}. u m)) = (SUP n\<in>{1..}. (INF m\<in>{n..}. u m))"
-    apply (rule SUP_eq) using Suc_le_D by (auto)
+    by (rule SUP_eq) (use Suc_le_D in auto)
   have "(SUP n\<in>{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
-    apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
+    by (rule SUP_eq) (use \<open>incseq v\<close> incseq_Suc_iff in auto)
   moreover have "incseq (\<lambda>n. (INF m\<in>{n..}. u m))" by (simp add: INF_superset_mono mono_def)
   ultimately have c: "(SUP n\<in>{1..}. (INF m\<in>{n..}. u m)) = (SUP n. (INF m\<in>{n..}. u m))" by simp
   have "(SUP n. Inf (u ` {n..})) = (SUP n. INF m\<in>{n..}. u (m + 1))" using a b c by simp
@@ -1229,7 +1212,8 @@
   "liminf (\<lambda>n. u (n+k)) = liminf u"
 proof (induction k)
   case (Suc k)
-  have "liminf (\<lambda>n. u (n+k+1)) = liminf (\<lambda>n. u (n+k))" using liminf_shift[where ?u="\<lambda>n. u(n+k)"] by simp
+  have "liminf (\<lambda>n. u (n+k+1)) = liminf (\<lambda>n. u (n+k))" 
+    using liminf_shift[where ?u="\<lambda>n. u(n+k)"] by simp
   then show ?case using Suc.IH by simp
 qed (auto)
 
@@ -1392,8 +1376,7 @@
         have "u i \<ge> u p"
         proof (cases)
           assume "i \<le> x"
-          then have "i \<in> {N<..x}" using i by simp
-          then show ?thesis using a by simp
+          then show ?thesis using a \<open>i \<in> {N<..y}\<close> by force
         next
           assume "\<not>(i \<le> x)"
           then have "i > x" by simp
@@ -1608,7 +1591,7 @@
     unfolding w_def using that by (auto simp: ereal_divide_eq)
   ultimately have "eventually (\<lambda>n. (w o s) n / (u o s) n = (v o s) n) sequentially" using eventually_elim2 by force
   moreover have "(\<lambda>n. (w o s) n / (u o s) n) \<longlonglongrightarrow> (liminf w) / a"
-    apply (rule tendsto_divide_ereal[OF s(2) *]) using assms(2) assms(3) by auto
+    using "*" assms s tendsto_divide_ereal by fastforce
   ultimately have "(v o s) \<longlonglongrightarrow> (liminf w) / a" using Lim_transform_eventually by fastforce
   then have "liminf (v o s) = (liminf w) / a" by (simp add: tendsto_iff_Liminf_eq_Limsup)
   then have "liminf v \<le> (liminf w) / a" by (metis liminf_subseq_mono s(1))
@@ -1628,7 +1611,7 @@
   then have **: "abs(liminf (\<lambda>n. -u n)) \<noteq> \<infinity>" using assms(2) by auto
 
   have "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
-    apply (rule ereal_liminf_add_mono) using * by auto
+    using abs_ereal.simps by (metis (full_types) "*" ereal_liminf_add_mono)
   then have up: "liminf (\<lambda>n. u n + v n) \<ge> a + liminf v" using \<open>liminf u = a\<close> by simp
 
   have a: "liminf (\<lambda>n. (u n + v n) + (-u n)) \<ge> liminf (\<lambda>n. u n + v n) + liminf (\<lambda>n. -u n)"
diff -r b3c5bc06f5be -r c0459ee8220c src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Tue Jan 03 18:23:52 2023 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Tue Jan 03 19:55:35 2023 +0000
@@ -474,10 +474,7 @@
     using order.trans by fastforce
 next
   case False
-  then show ?thesis
-    apply simp
-    apply (erule ex_forward)
-    by blast
+  then show ?thesis by fastforce
 qed
 
 lemma faces_of_translation:
@@ -661,23 +658,16 @@
 
 lemma exposed_face_of:
     "T exposed_face_of S \<longleftrightarrow>
-     T face_of S \<and>
-     (T = {} \<or> T = S \<or>
+     T face_of S \<and> (T = {} \<or> T = S \<or>
       (\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b}))"
-proof (cases "T = {}")
-  case False
-  show ?thesis
-  proof (cases "T = S")
-    case True then show ?thesis
-      by (simp add: face_of_refl_eq)
-  next
-    case False
-    with \<open>T \<noteq> {}\<close> show ?thesis
-      apply (auto simp: exposed_face_of_def)
-      apply (metis inner_zero_left)
-      done
-  qed
-qed auto
+     (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (smt (verit) Collect_cong exposed_face_of_def hyperplane_eq_empty inf.absorb_iff1
+                    inf_bot_right inner_zero_left)
+  show "?rhs \<Longrightarrow> ?lhs"
+    using exposed_face_of_def face_of_imp_convex by fastforce
+qed
 
 lemma exposed_face_of_Int_supporting_hyperplane_le:
    "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
@@ -780,10 +770,7 @@
     proof -
       have "\<And>x y. \<lbrakk>z = u \<bullet> (x + y); x \<in> S; y \<in> T\<rbrakk>
            \<Longrightarrow> u \<bullet> x = u \<bullet> a0 \<and> u \<bullet> y = u \<bullet> b0"
-        using z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close>
-        apply (simp add: inner_right_distrib)
-        apply (metis add_le_cancel_right antisym lez [unfolded inner_right_distrib] add.commute)
-        done
+        by (smt (verit, best) z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close> inner_right_distrib lez)
       then show ?thesis
         using feq by blast
     qed
@@ -815,18 +802,18 @@
       then show ?thesis
       proof
         assume "affine hull S \<inter> {x. - a \<bullet> x \<le> - b} = {}"
-       then show ?thesis
-         apply (rule_tac x="0" in exI)
-         apply (rule_tac x="1" in exI)
-         using hull_subset by fastforce
+        then show ?thesis
+          apply (rule_tac x="0" in exI)
+          apply (rule_tac x="1" in exI)
+          using hull_subset by fastforce
+      next
+        assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
+        then show ?thesis
+          apply (rule_tac x="0" in exI)
+          apply (rule_tac x="0" in exI)
+          using Ssub hull_subset by fastforce
+      qed
     next
-      assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
-      then show ?thesis
-         apply (rule_tac x="0" in exI)
-         apply (rule_tac x="0" in exI)
-        using Ssub hull_subset by fastforce
-    qed
-  next
     case False
     then obtain a' b' where "a' \<noteq> 0" 
       and le: "affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> {x. - a \<bullet> x \<le> - b}" 
@@ -1472,9 +1459,8 @@
   have "\<not> affine_dependent c"
     using \<open>c \<subseteq> S\<close> affine_dependent_subset assms by blast
   with affs have "card (S - c) = 1"
-    apply (simp add: aff_dim_affine_independent [symmetric] aff_dim_convex_hull)
-    by (metis aff_dim_affine_independent aff_independent_finite One_nat_def \<open>c \<subseteq> S\<close> add.commute
-                add_diff_cancel_right' assms card_Diff_subset card_mono of_nat_1 of_nat_diff of_nat_eq_iff)
+    by (smt (verit) \<open>c \<subseteq> S\<close> aff_dim_affine_independent aff_independent_finite assms card_Diff_subset 
+        card_mono of_nat_diff of_nat_eq_1_iff)
   then obtain u where u: "u \<in> S - c"
     by (metis DiffI \<open>c \<subseteq> S\<close> aff_independent_finite assms cancel_comm_monoid_add_class.diff_cancel
                 card_Diff_subset subsetI subset_antisym zero_neq_one)
@@ -3361,11 +3347,9 @@
                 ultimately show "convex hull (J - {?z}) \<in> \<U> \<inter> Pow (rel_frontier C)" by auto
                 let ?F = "convex hull insert ?z (convex hull (J - {?z}))"
                 have "F \<subseteq> ?F"
-                  apply (clarsimp simp: \<open>F = convex hull J\<close>)
-                  by (metis True subsetD hull_mono hull_subset subset_insert_iff)
+                  by (simp add: \<open>F = convex hull J\<close> hull_mono hull_subset subset_insert_iff)
                 moreover have "?F \<subseteq> F"
-                  apply (clarsimp simp: \<open>F = convex hull J\<close>)
-                  by (metis (no_types, lifting) True convex_hull_eq_empty convex_hull_insert_segments hull_hull insert_Diff)
+                  by (metis True \<open>F = convex hull J\<close> hull_insert insert_Diff set_eq_subset)
                 ultimately
                 show "F \<in> {?F}" by auto
               qed
diff -r b3c5bc06f5be -r c0459ee8220c src/HOL/Complex_Analysis/Complex_Singularities.thy
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy	Tue Jan 03 18:23:52 2023 +0100
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy	Tue Jan 03 19:55:35 2023 +0000
@@ -43,16 +43,14 @@
   hence "continuous_on (s-{z}) (inverse o f)" unfolding comp_def
     by (auto elim!:continuous_on_inverse simp add:non_z)
   hence "continuous_on (s-{z}) g" unfolding g_def
-    apply (subst continuous_on_cong[where t="s-{z}" and g="inverse o f"])
-    by auto
+    using continuous_on_eq by fastforce
   ultimately have "continuous_on s g" using open_delete[OF \<open>open s\<close>] \<open>open s\<close>
     by (auto simp add:continuous_on_eq_continuous_at)
   moreover have "(inverse o f) holomorphic_on (s-{z})"
     unfolding comp_def using f_holo
     by (auto elim!:holomorphic_on_inverse simp add:non_z)
   hence "g holomorphic_on (s-{z})"
-    apply (subst holomorphic_cong[where t="s-{z}" and g="inverse o f"])
-    by (auto simp add:g_def)
+    using g_def holomorphic_transform by force
   ultimately show ?thesis unfolding g_def using \<open>open s\<close>
     by (auto elim!: no_isolated_singularity)
 qed
@@ -82,9 +80,8 @@
   shows   "is_pole (\<lambda>z. f z / g z) z"
 proof -
   have "filterlim (\<lambda>z. f z * inverse (g z)) at_infinity (at z)"
-    by (intro tendsto_mult_filterlim_at_infinity[of _ "f z"]
-                 filterlim_compose[OF filterlim_inverse_at_infinity])+
-       (insert assms, auto simp: isCont_def)
+    using assms filterlim_compose filterlim_inverse_at_infinity isCont_def 
+      tendsto_mult_filterlim_at_infinity by blast
   thus ?thesis by (simp add: field_split_simps is_pole_def)
 qed
 
@@ -132,9 +129,7 @@
     have "(h \<longlongrightarrow> 0) (at z within ball z r)"
     proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powr (n - m) * g w"])
       have "\<forall>w\<in>ball z r-{z}. h w = (w-z)powr(n-m) * g w"
-        using \<open>n>m\<close> asm \<open>r>0\<close>
-        apply (auto simp add:field_simps powr_diff)
-        by force
+        using \<open>n>m\<close> asm \<open>r>0\<close> by (simp add: field_simps powr_diff) force
       then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
             \<Longrightarrow> (x' - z) powr (n - m) * g x' = h x'" for x' by auto
     next
@@ -142,8 +137,8 @@
       define f' where "f' \<equiv> \<lambda>x. (x - z) powr (n-m)"
       have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
       moreover have "continuous F f'" unfolding f'_def F_def continuous_def
-        apply (subst Lim_ident_at)
-        using \<open>n>m\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros)
+        using \<open>n>m\<close> 
+          by (auto simp add: Lim_ident_at  intro!:tendsto_powr_complex_0 tendsto_eq_intros)
       ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
         by (simp add: continuous_within)
       moreover have "(g \<longlongrightarrow> g z) F"
@@ -162,8 +157,7 @@
     have "(g \<longlongrightarrow> 0) (at z within ball z r)"
     proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powr (m - n) * h w"])
       have "\<forall>w\<in>ball z r -{z}. g w = (w-z) powr (m-n) * h w" using \<open>m>n\<close> asm
-        apply (auto simp add:field_simps powr_diff)
-        by force
+        by (simp add:field_simps powr_diff) force
       then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
             \<Longrightarrow> (x' - z) powr (m - n) * h x' = g x'" for x' by auto
     next
@@ -171,8 +165,8 @@
       define f' where "f' \<equiv>\<lambda>x. (x - z) powr (m-n)"
       have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
       moreover have "continuous F f'" unfolding f'_def F_def continuous_def
-        apply (subst Lim_ident_at)
-        using \<open>m>n\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros)
+        using \<open>m>n\<close> 
+        by (auto simp: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
       ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
         by (simp add: continuous_within)
       moreover have "(h \<longlongrightarrow> h z) F"
@@ -222,22 +216,22 @@
       "\<exists>z'. (h \<longlongrightarrow> z') (at z)" "isolated_singularity_at h z"  "\<exists>\<^sub>Fw in (at z). h w\<noteq>0"
     for h
   proof -
-    from that(2) obtain r where "r>0" "h analytic_on ball z r - {z}"
+    from that(2) obtain r where "r>0" and r: "h analytic_on ball z r - {z}"
       unfolding isolated_singularity_at_def by auto
     obtain z' where "(h \<longlongrightarrow> z') (at z)" using \<open>\<exists>z'. (h \<longlongrightarrow> z') (at z)\<close> by auto
     define h' where "h'=(\<lambda>x. if x=z then z' else h x)"
     have "h' holomorphic_on ball z r"
-      apply (rule no_isolated_singularity'[of "{z}"])
-      subgoal by (metis LIM_equal Lim_at_imp_Lim_at_within \<open>h \<midarrow>z\<rightarrow> z'\<close> empty_iff h'_def insert_iff)
-      subgoal using \<open>h analytic_on ball z r - {z}\<close> analytic_imp_holomorphic h'_def holomorphic_transform
-        by fastforce
-      by auto
+    proof (rule no_isolated_singularity'[of "{z}"])
+      show "\<And>w. w \<in> {z} \<Longrightarrow> (h' \<longlongrightarrow> h' w) (at w within ball z r)"
+        by (simp add: LIM_cong Lim_at_imp_Lim_at_within \<open>h \<midarrow>z\<rightarrow> z'\<close> h'_def)
+      show "h' holomorphic_on ball z r - {z}"
+        using r analytic_imp_holomorphic h'_def holomorphic_transform by fastforce
+    qed auto
     have ?thesis when "z'=0"
     proof -
       have "h' z=0" using that unfolding h'_def by auto
       moreover have "\<not> h' constant_on ball z r"
         using \<open>\<exists>\<^sub>Fw in (at z). h w\<noteq>0\<close> unfolding constant_on_def frequently_def eventually_at h'_def
-        apply simp
         by (metis \<open>0 < r\<close> centre_in_ball dist_commute mem_ball that)
       moreover note \<open>h' holomorphic_on ball z r\<close>
       ultimately obtain g r1 n where "0 < n" "0 < r1" "ball z r1 \<subseteq> ball z r" and
@@ -278,7 +272,7 @@
     ultimately show ?thesis by auto
   qed
 
-  have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)"
+  have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)"  
     apply (rule_tac imp_unique[unfolded P_def])
     using P_exist[OF that(1) f_iso non_zero] unfolding P_def .
   moreover have ?thesis when "is_pole f z"
@@ -292,29 +286,23 @@
         using that eventually_at[of "\<lambda>x. f x\<noteq>0" z UNIV,simplified] by (auto simp add:dist_commute)
       obtain e2 where e2:"e2>0" "f holomorphic_on ball z e2 - {z}"
         using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by auto
-      define e where "e=min e1 e2"
       show ?thesis
-        apply (rule that[of e])
-        using  e1 e2 unfolding e_def by auto
+        using e1 e2 by (force intro: that[of "min e1 e2"])
     qed
 
     define h where "h \<equiv> \<lambda>x. inverse (f x)"
-
     have "\<exists>n g r. P h n g r"
     proof -
-      have "h \<midarrow>z\<rightarrow> 0"
+      have "(\<lambda>x. inverse (f x)) analytic_on ball z e - {z}"
+        by (metis e_holo e_nz open_ball analytic_on_open holomorphic_on_inverse open_delete)
+      moreover have "h \<midarrow>z\<rightarrow> 0"
         using Lim_transform_within_open assms(2) h_def is_pole_tendsto that by fastforce
       moreover have "\<exists>\<^sub>Fw in (at z). h w\<noteq>0"
-        using non_zero
-        apply (elim frequently_rev_mp)
-        unfolding h_def eventually_at by (auto intro:exI[where x=1])
-      moreover have "isolated_singularity_at h z"
+        using non_zero by (simp add: h_def)
+      ultimately show ?thesis
+        using P_exist[of h] \<open>e > 0\<close>
         unfolding isolated_singularity_at_def h_def
-        apply (rule exI[where x=e])
-        using e_holo e_nz \<open>e>0\<close> by (metis open_ball analytic_on_open
-            holomorphic_on_inverse open_delete)
-      ultimately show ?thesis
-        using P_exist[of h] by auto
+        by blast
     qed
     then obtain n g r
       where "0 < r" and
@@ -324,9 +312,8 @@
     have "P f (-n) (inverse o g) r"
     proof -
       have "f w = inverse (g w) * (w - z) powr of_int (- n)" when "w\<in>cball z r - {z}" for w
-        using g_fac[rule_format,of w] that unfolding h_def
-        apply (auto simp add:powr_minus )
-        by (metis inverse_inverse_eq inverse_mult_distrib)
+        by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus 
+            powr_minus that)
       then show ?thesis
         unfolding P_def comp_def
         using \<open>r>0\<close> g_holo g_fac \<open>g z\<noteq>0\<close> by (auto intro:holomorphic_intros)
@@ -378,33 +365,31 @@
     have "(\<lambda>w.  (f w) ^ (nat n)) \<midarrow>z\<rightarrow> x ^ nat n"
       using that assms unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
     then have "fp \<midarrow>z\<rightarrow> x ^ nat n" unfolding fp_def
-      apply (elim Lim_transform_within[where d=1],simp)
-      by (metis less_le powr_0 powr_of_int that zero_less_nat_eq zero_power)
+      by (smt (verit, best) LIM_equal of_int_of_nat power_eq_0_iff powr_nat that zero_less_nat_eq)
     then show ?thesis unfolding not_essential_def fp_def by auto
   qed
   moreover have ?thesis when "n=0"
   proof -
-    have "fp \<midarrow>z\<rightarrow> 1 "
-      apply (subst tendsto_cong[where g="\<lambda>_.1"])
-      using that filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def by auto
+    have "\<forall>\<^sub>F x in at z. fp x = 1"
+      using that filterlim_at_within_not_equal[OF assms] by (auto simp: fp_def)
+    then have "fp \<midarrow>z\<rightarrow> 1"
+      by (simp add: tendsto_eventually)
     then show ?thesis unfolding fp_def not_essential_def by auto
   qed
   moreover have ?thesis when "n<0"
   proof (cases "x=0")
     case True
-    have "LIM w (at z). inverse ((f w) ^ (nat (-n))) :> at_infinity"
-      apply (subst filterlim_inverse_at_iff[symmetric],simp)
-      apply (rule filterlim_atI)
-      subgoal using assms True that unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
-      subgoal using filterlim_at_within_not_equal[OF assms,of 0]
-        by (eventually_elim,insert that,auto)
-      done
+    have "(\<lambda>x. f x ^ nat (- n)) \<midarrow>z\<rightarrow> 0"
+      using assms True that unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
+    moreover have "\<forall>\<^sub>F x in at z. f x ^ nat (- n) \<noteq> 0"
+      by (smt (verit) True assms eventually_at_topological filterlim_at power_eq_0_iff)
+    ultimately have "LIM w (at z). inverse ((f w) ^ (nat (-n))) :> at_infinity"
+      by (metis filterlim_atI filterlim_compose filterlim_inverse_at_infinity)
     then have "LIM w (at z). fp w :> at_infinity"
     proof (elim filterlim_mono_eventually)
       show "\<forall>\<^sub>F x in at z. inverse (f x ^ nat (- n)) = fp x"
         using filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def
-        apply eventually_elim
-        using powr_of_int that by auto
+        by (smt (verit, ccfv_threshold) eventually_mono powr_of_int that)
     qed auto
     then show ?thesis unfolding fp_def not_essential_def is_pole_def by auto
   next
@@ -412,10 +397,9 @@
     let ?xx= "inverse (x ^ (nat (-n)))"
     have "(\<lambda>w. inverse ((f w) ^ (nat (-n)))) \<midarrow>z\<rightarrow>?xx"
       using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
-    then have "fp \<midarrow>z\<rightarrow>?xx"
-      apply (elim Lim_transform_within[where d=1],simp)
-      unfolding fp_def by (metis inverse_zero nat_mono_iff nat_zero_as_int neg_0_less_iff_less
-          not_le power_eq_0_iff powr_0 powr_of_int that)
+    then have "fp \<midarrow>z\<rightarrow> ?xx"
+      by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff 
+          powr_of_int that zero_less_nat_eq)
     then show ?thesis unfolding fp_def not_essential_def by auto
   qed
   ultimately show ?thesis by linarith
@@ -433,14 +417,10 @@
     using assms(2) unfolding eventually_at by auto
   define r3 where "r3=min r1 r2"
   have "(\<lambda>w. (f w) powr of_int n) holomorphic_on ball z r3 - {z}"
-    apply (rule holomorphic_on_powr_of_int)
-    subgoal unfolding r3_def using r1 by auto
-    subgoal unfolding r3_def using r2 by (auto simp add:dist_commute)
-    done
+    by (intro holomorphic_on_powr_of_int) (use r1 r2 in \<open>auto simp: dist_commute r3_def\<close>)
   moreover have "r3>0" unfolding r3_def using \<open>0 < r1\<close> \<open>0 < r2\<close> by linarith
-  ultimately show ?thesis unfolding isolated_singularity_at_def
-    apply (subst (asm) analytic_on_open[symmetric])
-    by auto
+  ultimately show ?thesis
+    by (meson open_ball analytic_on_open isolated_singularity_at_def open_delete)
 qed
 
 lemma non_zero_neighbour:
@@ -478,19 +458,17 @@
   case True
   from isolated_zeros[OF holo \<open>open S\<close> \<open>connected S\<close> \<open>z \<in> S\<close> True \<open>\<beta> \<in> S\<close> \<open>f \<beta> \<noteq> 0\<close>]
   obtain r where "0 < r" "ball z r \<subseteq> S" "\<forall>w \<in> ball z r - {z}.f w \<noteq> 0" by metis
-  then show ?thesis unfolding eventually_at
-    apply (rule_tac x=r in exI)
-    by (auto simp add:dist_commute)
+  then show ?thesis
+    by (smt (verit) open_ball centre_in_ball eventually_at_topological insertE insert_Diff subsetD)
 next
   case False
   obtain r1 where r1:"r1>0" "\<forall>y. dist z y < r1 \<longrightarrow> f y \<noteq> 0"
     using continuous_at_avoid[of z f, OF _ False] assms(2,4) continuous_on_eq_continuous_at
       holo holomorphic_on_imp_continuous_on by blast
   obtain r2 where r2:"r2>0" "ball z r2 \<subseteq> S"
-    using assms(2) assms(4) openE by blast
+    using assms openE by blast
   show ?thesis unfolding eventually_at
-    apply (rule_tac x="min r1 r2" in exI)
-    using r1 r2 by (auto simp add:dist_commute)
+    by (metis (no_types) dist_commute dual_order.strict_trans linorder_less_linear mem_ball r1 r2 subsetD)
 qed
 
 lemma not_essential_times[singularity_intros]:
@@ -541,10 +519,9 @@
       have "(\<lambda>w. (fp w * gp w) * (w - z) ^ (nat (fn+gn))) \<midarrow>z\<rightarrow>0"
         using that by (auto intro!:tendsto_eq_intros)
       then have "fg \<midarrow>z\<rightarrow> 0"
-        apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>])
-        by (metis (no_types, opaque_lifting) Diff_iff cball_trivial dist_commute dist_self
-              eq_iff_diff_eq_0 fg_times less_le linorder_not_le mem_ball mem_cball powr_of_int
-              that)
+        using Lim_transform_within[OF _ \<open>r1>0\<close>]
+        by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq 
+            singletonD that)
       then show ?thesis unfolding not_essential_def fg_def by auto
     qed
     moreover have ?thesis when "fn+gn=0"