# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1691831369 -3600
# Node ID 56a408fa2440bed602351f33e1b73a16d6f04eeb
# Parent  1425a366fe7f42f43dd59251498f005561f58677
substantial tidy-up, shortening many proofs

diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Analysis/Affine.thy
--- a/src/HOL/Analysis/Affine.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Affine.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -5,7 +5,7 @@
 begin
 
 lemma if_smult: "(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)"
-  by (fact if_distrib)
+  by simp
 
 lemma sum_delta_notmem:
   assumes "x \<notin> s"
@@ -13,12 +13,7 @@
     and "sum (\<lambda>y. if (x = y) then P x else Q y) s = sum Q s"
     and "sum (\<lambda>y. if (y = x) then P y else Q y) s = sum Q s"
     and "sum (\<lambda>y. if (x = y) then P y else Q y) s = sum Q s"
-  apply (rule_tac [!] sum.cong)
-  using assms
-  apply auto
-  done
-
-lemmas independent_finite = independent_imp_finite
+  by (smt (verit, best) assms sum.cong)+
 
 lemma span_substd_basis:
   assumes d: "d \<subseteq> Basis"
@@ -32,13 +27,11 @@
   ultimately have "span d \<subseteq> ?B"
     using span_mono[of d "?B"] span_eq_iff[of "?B"] by blast
   moreover have *: "card d \<le> dim (span d)"
-    using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms]
-      span_superset[of d]
-    by auto
+    by (simp add: d dim_eq_card_independent independent_substdbasis)
   moreover from * have "dim ?B \<le> dim (span d)"
     using dim_substandard[OF assms] by auto
   ultimately show ?thesis
-    using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto
+    by (simp add: s subspace_dim_equal)
 qed
 
 lemma basis_to_substdbasis_subspace_isomorphism:
@@ -51,7 +44,8 @@
     using dim_unique[of B B "card B"] assms span_superset[of B] by auto
   have "dim B \<le> card (Basis :: 'a set)"
     using dim_subset_UNIV[of B] by simp
-  from obtain_subset_with_card_n[OF this] obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B"
+  from obtain_subset_with_card_n[OF this] 
+  obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B"
     by auto
   let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
   have "\<exists>f. linear f \<and> f ` B = d \<and> f ` span B = ?t \<and> inj_on f (span B)"
@@ -65,9 +59,9 @@
 subsection \<open>Affine set and affine hull\<close>
 
 definition\<^marker>\<open>tag important\<close> affine :: "'a::real_vector set \<Rightarrow> bool"
-  where "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
+  where "affine S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> S)"
 
-lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
+lemma affine_alt: "affine S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> S)"
   unfolding affine_def by (metis eq_diff_eq')
 
 lemma affine_empty [iff]: "affine {}"
@@ -79,21 +73,21 @@
 lemma affine_UNIV [iff]: "affine UNIV"
   unfolding affine_def by auto
 
-lemma affine_Inter [intro]: "(\<And>s. s\<in>f \<Longrightarrow> affine s) \<Longrightarrow> affine (\<Inter>f)"
+lemma affine_Inter [intro]: "(\<And>S. S\<in>\<F> \<Longrightarrow> affine S) \<Longrightarrow> affine (\<Inter>\<F>)"
   unfolding affine_def by auto
 
-lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
+lemma affine_Int[intro]: "affine S \<Longrightarrow> affine T \<Longrightarrow> affine (S \<inter> T)"
   unfolding affine_def by auto
 
-lemma affine_scaling: "affine s \<Longrightarrow> affine (image (\<lambda>x. c *\<^sub>R x) s)"
-  apply (clarsimp simp add: affine_def)
+lemma affine_scaling: "affine S \<Longrightarrow> affine ((*\<^sub>R) c ` S)"
+  apply (clarsimp simp: affine_def)
   apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI)
   apply (auto simp: algebra_simps)
   done
 
-lemma affine_affine_hull [simp]: "affine(affine hull s)"
+lemma affine_affine_hull [simp]: "affine(affine hull S)"
   unfolding hull_def
-  using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] by auto
+  using affine_Inter[of "{T. affine T \<and> S \<subseteq> T}"] by auto
 
 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
   by (metis affine_affine_hull hull_same)
@@ -198,6 +192,8 @@
   "affine hull p = {y. \<exists>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p \<and> sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
   (is "_ = ?rhs")
 proof (rule hull_unique)
+  have "\<And>x. sum (\<lambda>z. 1) {x} = 1"
+      by auto
   show "p \<subseteq> ?rhs"
   proof (intro subsetI CollectI exI conjI)
     show "\<And>x. sum (\<lambda>z. 1) {x} = 1"
@@ -452,31 +448,16 @@
   unfolding affine_parallel_def
   using image_add_0 by blast
 
-lemma affine_parallel_commut:
+lemma affine_parallel_commute:
   assumes "affine_parallel A B"
   shows "affine_parallel B A"
-proof -
-  from assms obtain a where B: "B = (\<lambda>x. a + x) ` A"
-    unfolding affine_parallel_def by auto
-  have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
-  from B show ?thesis
-    using translation_galois [of B a A]
-    unfolding affine_parallel_def by blast
-qed
+  by (metis affine_parallel_def assms translation_galois)
 
 lemma affine_parallel_assoc:
   assumes "affine_parallel A B"
     and "affine_parallel B C"
   shows "affine_parallel A C"
-proof -
-  from assms obtain ab where "B = (\<lambda>x. ab + x) ` A"
-    unfolding affine_parallel_def by auto
-  moreover
-  from assms obtain bc where "C = (\<lambda>x. bc + x) ` B"
-    unfolding affine_parallel_def by auto
-  ultimately show ?thesis
-    using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto
-qed
+  by (metis affine_parallel_def assms translation_assoc)
 
 lemma affine_translation_aux:
   fixes a :: "'a::real_vector"
@@ -503,24 +484,13 @@
 
 lemma affine_translation:
   "affine S \<longleftrightarrow> affine ((+) a ` S)" for a :: "'a::real_vector"
-proof
-  show "affine ((+) a ` S)" if "affine S"
-    using that translation_assoc [of "- a" a S]
-    by (auto intro: affine_translation_aux [of "- a" "((+) a ` S)"])
-  show "affine S" if "affine ((+) a ` S)"
-    using that by (rule affine_translation_aux)
-qed
+  by (metis affine_translation_aux translation_galois)
 
 lemma parallel_is_affine:
   fixes S T :: "'a::real_vector set"
   assumes "affine S" "affine_parallel S T"
   shows "affine T"
-proof -
-  from assms obtain a where "T = (\<lambda>x. a + x) ` S"
-    unfolding affine_parallel_def by auto
-  then show ?thesis
-    using affine_translation assms by auto
-qed
+  by (metis affine_parallel_def affine_translation assms)
 
 lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
   unfolding subspace_def affine_def by auto
@@ -532,64 +502,12 @@
 subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Subspace parallel to an affine set\<close>
 
 lemma subspace_affine: "subspace S \<longleftrightarrow> affine S \<and> 0 \<in> S"
-proof -
-  have h0: "subspace S \<Longrightarrow> affine S \<and> 0 \<in> S"
-    using subspace_imp_affine[of S] subspace_0 by auto
-  {
-    assume assm: "affine S \<and> 0 \<in> S"
-    {
-      fix c :: real
-      fix x
-      assume x: "x \<in> S"
-      have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto
-      moreover
-      have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \<in> S"
-        using affine_alt[of S] assm x by auto
-      ultimately have "c *\<^sub>R x \<in> S" by auto
-    }
-    then have h1: "\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S" by auto
-
-    {
-      fix x y
-      assume xy: "x \<in> S" "y \<in> S"
-      define u where "u = (1 :: real)/2"
-      have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)"
-        by auto
-      moreover
-      have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y"
-        by (simp add: algebra_simps)
-      moreover
-      have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> S"
-        using affine_alt[of S] assm xy by auto
-      ultimately
-      have "(1/2) *\<^sub>R (x+y) \<in> S"
-        using u_def by auto
-      moreover
-      have "x + y = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))"
-        by auto
-      ultimately
-      have "x + y \<in> S"
-        using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
-    }
-    then have "\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S"
-      by auto
-    then have "subspace S"
-      using h1 assm unfolding subspace_def by auto
-  }
-  then show ?thesis using h0 by metis
-qed
+  by (metis add_cancel_right_left affine_alt diff_add_cancel mem_affine_3 scaleR_eq_0_iff subspace_def vector_space_assms(4))
 
 lemma affine_diffs_subspace:
   assumes "affine S" "a \<in> S"
   shows "subspace ((\<lambda>x. (-a)+x) ` S)"
-proof -
-  have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
-  have "affine ((\<lambda>x. (-a)+x) ` S)"
-    using affine_translation assms by blast
-  moreover have "0 \<in> ((\<lambda>x. (-a)+x) ` S)"
-    using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto
-  ultimately show ?thesis using subspace_affine by auto
-qed
+  by (metis ab_left_minus affine_translation assms image_eqI subspace_affine)
 
 lemma affine_diffs_subspace_subtract:
   "subspace ((\<lambda>x. x - a) ` S)" if "affine S" "a \<in> S"
@@ -600,61 +518,26 @@
     and "a \<in> S"
   assumes "L \<equiv> {y. \<exists>x \<in> S. (-a) + x = y}"
   shows "subspace L \<and> affine_parallel S L"
-proof -
-  from assms have "L = plus (- a) ` S" by auto
-  then have par: "affine_parallel S L"
-    unfolding affine_parallel_def ..
-  then have "affine L" using assms parallel_is_affine by auto
-  moreover have "0 \<in> L"
-    using assms by auto
-  ultimately show ?thesis
-    using subspace_affine par by auto
-qed
+  by (smt (verit) Collect_cong ab_left_minus affine_parallel_def assms image_def mem_Collect_eq parallel_is_affine subspace_affine)
 
 lemma parallel_subspace_aux:
   assumes "subspace A"
     and "subspace B"
     and "affine_parallel A B"
   shows "A \<supseteq> B"
-proof -
-  from assms obtain a where a: "\<forall>x. x \<in> A \<longleftrightarrow> a + x \<in> B"
-    using affine_parallel_expl[of A B] by auto
-  then have "-a \<in> A"
-    using assms subspace_0[of B] by auto
-  then have "a \<in> A"
-    using assms subspace_neg[of A "-a"] by auto
-  then show ?thesis
-    using assms a unfolding subspace_def by auto
-qed
+  by (metis add.right_neutral affine_parallel_expl assms subsetI subspace_def)
 
 lemma parallel_subspace:
   assumes "subspace A"
     and "subspace B"
     and "affine_parallel A B"
   shows "A = B"
-proof
-  show "A \<supseteq> B"
-    using assms parallel_subspace_aux by auto
-  show "A \<subseteq> B"
-    using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto
-qed
+  by (simp add: affine_parallel_commute assms parallel_subspace_aux subset_antisym)
 
 lemma affine_parallel_subspace:
   assumes "affine S" "S \<noteq> {}"
   shows "\<exists>!L. subspace L \<and> affine_parallel S L"
-proof -
-  have ex: "\<exists>L. subspace L \<and> affine_parallel S L"
-    using assms parallel_subspace_explicit by auto
-  {
-    fix L1 L2
-    assume ass: "subspace L1 \<and> affine_parallel S L1" "subspace L2 \<and> affine_parallel S L2"
-    then have "affine_parallel L1 L2"
-      using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto
-    then have "L1 = L2"
-      using ass parallel_subspace by auto
-  }
-  then show ?thesis using ex by auto
-qed
+  by (meson affine_parallel_assoc affine_parallel_commute assms equals0I parallel_subspace parallel_subspace_explicit)
 
 
 subsection \<open>Affine Dependence\<close>
@@ -662,50 +545,49 @@
 text "Formalized by Lars Schewe."
 
 definition\<^marker>\<open>tag important\<close> affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
-  where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
+  where "affine_dependent S \<longleftrightarrow> (\<exists>x\<in>S. x \<in> affine hull (S - {x}))"
 
-lemma affine_dependent_imp_dependent: "affine_dependent s \<Longrightarrow> dependent s"
+lemma affine_dependent_imp_dependent: "affine_dependent S \<Longrightarrow> dependent S"
   unfolding affine_dependent_def dependent_def
   using affine_hull_subset_span by auto
 
 lemma affine_dependent_subset:
-   "\<lbrakk>affine_dependent s; s \<subseteq> t\<rbrakk> \<Longrightarrow> affine_dependent t"
-apply (simp add: affine_dependent_def Bex_def)
-apply (blast dest: hull_mono [OF Diff_mono [OF _ subset_refl]])
-done
+   "\<lbrakk>affine_dependent S; S \<subseteq> T\<rbrakk> \<Longrightarrow> affine_dependent T"
+  using hull_mono [OF Diff_mono [OF _ subset_refl]]
+  by (smt (verit) affine_dependent_def subsetD)
 
 lemma affine_independent_subset:
-  shows "\<lbrakk>\<not> affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> \<not> affine_dependent s"
-by (metis affine_dependent_subset)
+  shows "\<lbrakk>\<not> affine_dependent T; S \<subseteq> T\<rbrakk> \<Longrightarrow> \<not> affine_dependent S"
+  by (metis affine_dependent_subset)
 
 lemma affine_independent_Diff:
-   "\<not> affine_dependent s \<Longrightarrow> \<not> affine_dependent(s - t)"
+   "\<not> affine_dependent S \<Longrightarrow> \<not> affine_dependent(S - T)"
 by (meson Diff_subset affine_dependent_subset)
 
 proposition affine_dependent_explicit:
   "affine_dependent p \<longleftrightarrow>
-    (\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
+    (\<exists>S U. finite S \<and> S \<subseteq> p \<and> sum U S = 0 \<and> (\<exists>v\<in>S. U v \<noteq> 0) \<and> sum (\<lambda>v. U v *\<^sub>R v) S = 0)"
 proof -
-  have "\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> (\<Sum>w\<in>S. u w *\<^sub>R w) = 0"
-    if "(\<Sum>w\<in>S. u w *\<^sub>R w) = x" "x \<in> p" "finite S" "S \<noteq> {}" "S \<subseteq> p - {x}" "sum u S = 1" for x S u
+  have "\<exists>S U. finite S \<and> S \<subseteq> p \<and> sum U S = 0 \<and> (\<exists>v\<in>S. U v \<noteq> 0) \<and> (\<Sum>w\<in>S. U w *\<^sub>R w) = 0"
+    if "(\<Sum>w\<in>S. U w *\<^sub>R w) = x" "x \<in> p" "finite S" "S \<noteq> {}" "S \<subseteq> p - {x}" "sum U S = 1" for x S U
   proof (intro exI conjI)
     have "x \<notin> S" 
       using that by auto
-    then show "(\<Sum>v \<in> insert x S. if v = x then - 1 else u v) = 0"
+    then show "(\<Sum>v \<in> insert x S. if v = x then - 1 else U v) = 0"
       using that by (simp add: sum_delta_notmem)
-    show "(\<Sum>w \<in> insert x S. (if w = x then - 1 else u w) *\<^sub>R w) = 0"
+    show "(\<Sum>w \<in> insert x S. (if w = x then - 1 else U w) *\<^sub>R w) = 0"
       using that \<open>x \<notin> S\<close> by (simp add: if_smult sum_delta_notmem cong: if_cong)
   qed (use that in auto)
-  moreover have "\<exists>x\<in>p. \<exists>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p - {x} \<and> sum u S = 1 \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = x"
-    if "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0" "finite S" "S \<subseteq> p" "sum u S = 0" "v \<in> S" "u v \<noteq> 0" for S u v
+  moreover have "\<exists>x\<in>p. \<exists>S U. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p - {x} \<and> sum U S = 1 \<and> (\<Sum>v\<in>S. U v *\<^sub>R v) = x"
+    if "(\<Sum>v\<in>S. U v *\<^sub>R v) = 0" "finite S" "S \<subseteq> p" "sum U S = 0" "v \<in> S" "U v \<noteq> 0" for S U v
   proof (intro bexI exI conjI)
     have "S \<noteq> {v}"
       using that by auto
     then show "S - {v} \<noteq> {}"
       using that by auto
-    show "(\<Sum>x \<in> S - {v}. - (1 / u v) * u x) = 1"
+    show "(\<Sum>x \<in> S - {v}. - (1 / U v) * U x) = 1"
       unfolding sum_distrib_left[symmetric] sum_diff1[OF \<open>finite S\<close>] by (simp add: that)
-    show "(\<Sum>x\<in>S - {v}. (- (1 / u v) * u x) *\<^sub>R x) = v"
+    show "(\<Sum>x\<in>S - {v}. (- (1 / U v) * U x) *\<^sub>R x) = v"
       unfolding sum_distrib_left [symmetric] scaleR_scaleR[symmetric]
                 scaleR_right.sum [symmetric] sum_diff1[OF \<open>finite S\<close>] 
       using that by auto
@@ -720,90 +602,82 @@
   fixes S :: "'a::real_vector set"
   assumes "finite S"
   shows "affine_dependent S \<longleftrightarrow>
-    (\<exists>u. sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
+    (\<exists>U. sum U S = 0 \<and> (\<exists>v\<in>S. U v \<noteq> 0) \<and> sum (\<lambda>v. U v *\<^sub>R v) S = 0)"
   (is "?lhs = ?rhs")
 proof
-  have *: "\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else 0::'a)"
+  have *: "\<And>vt U v. (if vt then U v else 0) *\<^sub>R v = (if vt then (U v) *\<^sub>R v else 0::'a)"
     by auto
   assume ?lhs
-  then obtain t u v where
-    "finite t" "t \<subseteq> S" "sum u t = 0" "v\<in>t" "u v \<noteq> 0"  "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0"
+  then obtain T U v where
+    "finite T" "T \<subseteq> S" "sum U T = 0" "v\<in>T" "U v \<noteq> 0"  "(\<Sum>v\<in>T. U v *\<^sub>R v) = 0"
     unfolding affine_dependent_explicit by auto
   then show ?rhs
-    apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
-    apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \<open>t\<subseteq>S\<close>])
+    apply (rule_tac x="\<lambda>x. if x\<in>T then U x else 0" in exI)
+    apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \<open>T\<subseteq>S\<close>])
     done
 next
   assume ?rhs
-  then obtain u v where "sum u S = 0"  "v\<in>S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0"
+  then obtain U v where "sum U S = 0"  "v\<in>S" "U v \<noteq> 0" "(\<Sum>v\<in>S. U v *\<^sub>R v) = 0"
     by auto
   then show ?lhs unfolding affine_dependent_explicit
     using assms by auto
 qed
 
 lemma dependent_imp_affine_dependent:
-  assumes "dependent {x - a| x . x \<in> s}"
-    and "a \<notin> s"
-  shows "affine_dependent (insert a s)"
+  assumes "dependent {x - a| x . x \<in> S}"
+    and "a \<notin> S"
+  shows "affine_dependent (insert a S)"
 proof -
-  from assms(1)[unfolded dependent_explicit] obtain S u v
-    where obt: "finite S" "S \<subseteq> {x - a |x. x \<in> s}" "v\<in>S" "u v  \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0"
+  from assms(1)[unfolded dependent_explicit] obtain S' U v
+    where S: "finite S'" "S' \<subseteq> {x - a |x. x \<in> S}" "v\<in>S'" "U v  \<noteq> 0" "(\<Sum>v\<in>S'. U v *\<^sub>R v) = 0"
     by auto
-  define t where "t = (\<lambda>x. x + a) ` S"
-
-  have inj: "inj_on (\<lambda>x. x + a) S"
+  define T where "T = (\<lambda>x. x + a) ` S'"
+  have inj: "inj_on (\<lambda>x. x + a) S'"
     unfolding inj_on_def by auto
-  have "0 \<notin> S"
-    using obt(2) assms(2) unfolding subset_eq by auto
-  have fin: "finite t" and "t \<subseteq> s"
-    unfolding t_def using obt(1,2) by auto
-  then have "finite (insert a t)" and "insert a t \<subseteq> insert a s"
+  have "0 \<notin> S'"
+    using S(2) assms(2) unfolding subset_eq by auto
+  have fin: "finite T" and "T \<subseteq> S"
+    unfolding T_def using S(1,2) by auto
+  then have "finite (insert a T)" and "insert a T \<subseteq> insert a S"
     by auto
-  moreover have *: "\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x)) = (\<Sum>x\<in>t. Q x)"
-    apply (rule sum.cong)
-    using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close>
-    apply auto
-    done
-  have "(\<Sum>x\<in>insert a t. if x = a then - (\<Sum>x\<in>t. u (x - a)) else u (x - a)) = 0"
-    unfolding sum_clauses(2)[OF fin] * using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close> by auto
-  moreover have "\<exists>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) \<noteq> 0"
-    using obt(3,4) \<open>0\<notin>S\<close>
-    by (rule_tac x="v + a" in bexI) (auto simp: t_def)
-  moreover have *: "\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x) *\<^sub>R x) = (\<Sum>x\<in>t. Q x *\<^sub>R x)"
-    using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close> by (auto intro!: sum.cong)
-  have "(\<Sum>x\<in>t. u (x - a)) *\<^sub>R a = (\<Sum>v\<in>t. u (v - a) *\<^sub>R v)"
+  moreover have *: "\<And>P Q. (\<Sum>x\<in>T. (if x = a then P x else Q x)) = (\<Sum>x\<in>T. Q x)"
+    by (smt (verit, best) \<open>T \<subseteq> S\<close> assms(2) subsetD sum.cong)
+  have "(\<Sum>x\<in>insert a T. if x = a then - (\<Sum>x\<in>T. U (x - a)) else U (x - a)) = 0"
+    by (smt (verit) \<open>T \<subseteq> S\<close> assms(2) fin insert_absorb insert_subset sum.insert sum_mono)
+  moreover have "\<exists>v\<in>insert a T. (if v = a then - (\<Sum>x\<in>T. U (x - a)) else U (v - a)) \<noteq> 0"
+    using S(3,4) \<open>0\<notin>S'\<close>
+    by (rule_tac x="v + a" in bexI) (auto simp: T_def)
+  moreover have *: "\<And>P Q. (\<Sum>x\<in>T. (if x = a then P x else Q x) *\<^sub>R x) = (\<Sum>x\<in>T. Q x *\<^sub>R x)"
+    using \<open>a\<notin>S\<close> \<open>T\<subseteq>S\<close> by (auto intro!: sum.cong)
+  have "(\<Sum>x\<in>T. U (x - a)) *\<^sub>R a = (\<Sum>v\<in>T. U (v - a) *\<^sub>R v)"
     unfolding scaleR_left.sum
-    unfolding t_def and sum.reindex[OF inj] and o_def
-    using obt(5)
+    unfolding T_def and sum.reindex[OF inj] and o_def
+    using S(5)
     by (auto simp: sum.distrib scaleR_right_distrib)
-  then have "(\<Sum>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0"
-    unfolding sum_clauses(2)[OF fin]
-    using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close>
-    by (auto simp: *)
+  then have "(\<Sum>v\<in>insert a T. (if v = a then - (\<Sum>x\<in>T. U (x - a)) else U (v - a)) *\<^sub>R v) = 0"
+    unfolding sum_clauses(2)[OF fin] using \<open>a\<notin>S\<close> \<open>T\<subseteq>S\<close> by (auto simp: *)
   ultimately show ?thesis
     unfolding affine_dependent_explicit
-    apply (rule_tac x="insert a t" in exI, auto)
-    done
+    by (force intro!: exI[where x="insert a T"])
 qed
 
 lemma affine_dependent_biggerset:
-  fixes s :: "'a::euclidean_space set"
-  assumes "finite s" "card s \<ge> DIM('a) + 2"
-  shows "affine_dependent s"
+  fixes S :: "'a::euclidean_space set"
+  assumes "finite S" "card S \<ge> DIM('a) + 2"
+  shows "affine_dependent S"
 proof -
-  have "s \<noteq> {}" using assms by auto
-  then obtain a where "a\<in>s" by auto
-  have *: "{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})"
+  have "S \<noteq> {}" using assms by auto
+  then obtain a where "a\<in>S" by auto
+  have *: "{x - a |x. x \<in> S - {a}} = (\<lambda>x. x - a) ` (S - {a})"
     by auto
-  have "card {x - a |x. x \<in> s - {a}} = card (s - {a})"
+  have "card {x - a |x. x \<in> S - {a}} = card (S - {a})"
     unfolding * by (simp add: card_image inj_on_def)
   also have "\<dots> > DIM('a)" using assms(2)
-    unfolding card_Diff_singleton[OF \<open>a\<in>s\<close>] by auto
-  finally show ?thesis
-    apply (subst insert_Diff[OF \<open>a\<in>s\<close>, symmetric])
-    apply (rule dependent_imp_affine_dependent)
-    apply (rule dependent_biggerset, auto)
-    done
+    unfolding card_Diff_singleton[OF \<open>a\<in>S\<close>] by auto
+  finally  have "affine_dependent (insert a (S - {a}))"
+    using dependent_biggerset dependent_imp_affine_dependent by blast
+  then show ?thesis
+    by (simp add: \<open>a \<in> S\<close> insert_absorb)
 qed
 
 lemma affine_dependent_biggerset_general:
@@ -822,13 +696,10 @@
   also have "\<dots> < dim S + 1" by auto
   also have "\<dots> \<le> card (S - {a})"
     using assms card_Diff_singleton[OF \<open>a\<in>S\<close>] by auto
-  finally show ?thesis
-    apply (subst insert_Diff[OF \<open>a\<in>S\<close>, symmetric])
-    apply (rule dependent_imp_affine_dependent)
-    apply (rule dependent_biggerset_general)
-    unfolding **
-    apply auto
-    done
+  finally have "affine_dependent (insert a (S - {a}))"
+    by (smt (verit) Collect_cong dependent_imp_affine_dependent dependent_biggerset_general ** Diff_iff insertCI)
+  then show ?thesis
+    by (simp add: \<open>a \<in> S\<close> insert_absorb)
 qed
 
 
@@ -882,16 +753,7 @@
 
 lemma affine_dependent_translation_eq:
   "affine_dependent S \<longleftrightarrow> affine_dependent ((\<lambda>x. a + x) ` S)"
-proof -
-  {
-    assume "affine_dependent ((\<lambda>x. a + x) ` S)"
-    then have "affine_dependent S"
-      using affine_dependent_translation[of "((\<lambda>x. a + x) ` S)" "-a"] translation_assoc[of "-a" a]
-      by auto
-  }
-  then show ?thesis
-    using affine_dependent_translation by auto
-qed
+  by (metis affine_dependent_translation translation_galois)
 
 lemma affine_hull_0_dependent:
   assumes "0 \<in> affine hull S"
@@ -919,14 +781,8 @@
   ultimately have "x \<in> span (S - {x})" by auto
   then have "x \<noteq> 0 \<Longrightarrow> dependent S"
     using x dependent_def by auto
-  moreover
-  {
-    assume "x = 0"
-    then have "0 \<in> affine hull S"
-      using x hull_mono[of "S - {0}" S] by auto
-    then have "dependent S"
-      using affine_hull_0_dependent by auto
-  }
+  moreover have "dependent S" if "x = 0"
+    by (metis that affine_hull_0_dependent Diff_insert_absorb dependent_zero x)
   ultimately show ?thesis by auto
 qed
 
@@ -945,60 +801,45 @@
 lemma affine_dependent_iff_dependent2:
   assumes "a \<in> S"
   shows "affine_dependent S \<longleftrightarrow> dependent ((\<lambda>x. -a + x) ` (S-{a}))"
-proof -
-  have "insert a (S - {a}) = S"
-    using assms by auto
-  then show ?thesis
-    using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto
-qed
+  by (metis Diff_iff affine_dependent_iff_dependent assms insert_Diff singletonI)
 
 lemma affine_hull_insert_span_gen:
-  "affine hull (insert a s) = (\<lambda>x. a + x) ` span ((\<lambda>x. - a + x) ` s)"
+  "affine hull (insert a S) = (\<lambda>x. a + x) ` span ((\<lambda>x. - a + x) ` S)"
 proof -
-  have h1: "{x - a |x. x \<in> s} = ((\<lambda>x. -a+x) ` s)"
+  have h1: "{x - a |x. x \<in> S} = ((\<lambda>x. -a+x) ` S)"
     by auto
   {
-    assume "a \<notin> s"
+    assume "a \<notin> S"
     then have ?thesis
-      using affine_hull_insert_span[of a s] h1 by auto
+      using affine_hull_insert_span[of a S] h1 by auto
   }
   moreover
   {
-    assume a1: "a \<in> s"
-    have "\<exists>x. x \<in> s \<and> -a+x=0"
-      apply (rule exI[of _ a])
-      using a1
-      apply auto
-      done
-    then have "insert 0 ((\<lambda>x. -a+x) ` (s - {a})) = (\<lambda>x. -a+x) ` s"
+    assume a1: "a \<in> S"
+    then have "insert 0 ((\<lambda>x. -a+x) ` (S - {a})) = (\<lambda>x. -a+x) ` S"
       by auto
-    then have "span ((\<lambda>x. -a+x) ` (s - {a}))=span ((\<lambda>x. -a+x) ` s)"
-      using span_insert_0[of "(+) (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff)
-    moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
+    then have "span ((\<lambda>x. -a+x) ` (S - {a})) = span ((\<lambda>x. -a+x) ` S)"
+      using span_insert_0[of "(+) (- a) ` (S - {a})"]
+      by presburger
+    moreover have "{x - a |x. x \<in> (S - {a})} = ((\<lambda>x. -a+x) ` (S - {a}))"
       by auto
-    moreover have "insert a (s - {a}) = insert a s"
+    moreover have "insert a (S - {a}) = insert a S"
       by auto
     ultimately have ?thesis
-      using affine_hull_insert_span[of "a" "s-{a}"] by auto
+      using affine_hull_insert_span[of "a" "S-{a}"] by auto
   }
   ultimately show ?thesis by auto
 qed
 
 lemma affine_hull_span2:
-  assumes "a \<in> s"
-  shows "affine hull s = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` (s-{a}))"
-  using affine_hull_insert_span_gen[of a "s - {a}", unfolded insert_Diff[OF assms]]
-  by auto
+  assumes "a \<in> S"
+  shows "affine hull S = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` (S-{a}))"
+  by (metis affine_hull_insert_span_gen assms insert_Diff)
 
 lemma affine_hull_span_gen:
-  assumes "a \<in> affine hull s"
-  shows "affine hull s = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` s)"
-proof -
-  have "affine hull (insert a s) = affine hull s"
-    using hull_redundant[of a affine s] assms by auto
-  then show ?thesis
-    using affine_hull_insert_span_gen[of a "s"] by auto
-qed
+  assumes "a \<in> affine hull S"
+  shows "affine hull S = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` S)"
+  by (metis affine_hull_insert_span_gen assms hull_redundant)
 
 lemma affine_hull_span_0:
   assumes "0 \<in> affine hull S"
@@ -1044,29 +885,13 @@
 lemma affine_basis_exists:
   fixes V :: "'n::real_vector set"
   shows "\<exists>B. B \<subseteq> V \<and> \<not> affine_dependent B \<and> affine hull V = affine hull B"
-proof (cases "V = {}")
-  case True
-  then show ?thesis
-    using affine_independent_0 by auto
-next
-  case False
-  then obtain x where "x \<in> V" by auto
-  then show ?thesis
-    using affine_dependent_def[of "{x}"] extend_to_affine_basis_nonempty[of "{x}" V]
-    by auto
-qed
+  by (metis affine_dependent_def affine_independent_1 empty_subsetI extend_to_affine_basis_nonempty insert_subset order_refl)
 
 proposition extend_to_affine_basis:
   fixes S V :: "'n::real_vector set"
   assumes "\<not> affine_dependent S" "S \<subseteq> V"
   obtains T where "\<not> affine_dependent T" "S \<subseteq> T" "T \<subseteq> V" "affine hull T = affine hull V"
-proof (cases "S = {}")
-  case True then show ?thesis
-    using affine_basis_exists by (metis empty_subsetI that)
-next
-  case False
-  then show ?thesis by (metis assms extend_to_affine_basis_nonempty that)
-qed
+  by (metis affine_basis_exists assms(1) assms(2) bot.extremum extend_to_affine_basis_nonempty)
 
 
 subsection \<open>Affine Dimension of a Set\<close>
@@ -1095,7 +920,7 @@
 by (metis affine_empty subset_empty subset_hull)
 
 lemma empty_eq_affine_hull[simp]: "{} = affine hull S \<longleftrightarrow> S = {}"
-by (metis affine_hull_eq_empty)
+  by (metis affine_hull_eq_empty)
 
 lemma aff_dim_parallel_subspace_aux:
   fixes B :: "'n::euclidean_space set"
@@ -1146,7 +971,7 @@
   define Lb where "Lb = span ((\<lambda>x. -a+x) ` (B-{a}))"
   moreover have "affine_parallel (affine hull B) Lb"
     using Lb_def B assms affine_hull_span2[of a B] a
-      affine_parallel_commut[of "Lb" "(affine hull B)"]
+      affine_parallel_commute[of "Lb" "(affine hull B)"]
     unfolding affine_parallel_def
     by auto
   moreover have "subspace Lb"
@@ -1168,15 +993,7 @@
   fixes B :: "'n::euclidean_space set"
   assumes "\<not> affine_dependent B"
   shows "finite B"
-proof -
-  {
-    assume "B \<noteq> {}"
-    then obtain a where "a \<in> B" by auto
-    then have ?thesis
-      using aff_dim_parallel_subspace_aux assms by auto
-  }
-  then show ?thesis by auto
-qed
+  using aff_dim_parallel_subspace_aux assms finite.simps by fastforce
 
 
 lemma aff_dim_empty:
@@ -1195,7 +1012,7 @@
 qed
 
 lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"
-  by (simp add: aff_dim_empty [symmetric])
+  using aff_dim_empty by blast
 
 lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S"
   unfolding aff_dim_def using hull_hull[of _ S] by auto
@@ -1224,7 +1041,7 @@
   define Lb where "Lb = span ((\<lambda>x. -a+x) ` (B-{a}))"
   have "affine_parallel (affine hull B) Lb"
     using Lb_def affine_hull_span2[of a B] a
-      affine_parallel_commut[of "Lb" "(affine hull B)"]
+      affine_parallel_commute[of "Lb" "(affine hull B)"]
     unfolding affine_parallel_def by auto
   moreover have "subspace Lb"
     using Lb_def subspace_span by auto
@@ -1245,11 +1062,14 @@
   using aff_dim_unique[of B B] assms by auto
 
 lemma affine_independent_iff_card:
-    fixes s :: "'a::euclidean_space set"
-    shows "\<not> affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
-  apply (rule iffI)
-  apply (simp add: aff_dim_affine_independent aff_independent_finite)
-  by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff)
+    fixes S :: "'a::euclidean_space set"
+    shows "\<not> affine_dependent S \<longleftrightarrow> finite S \<and> aff_dim S = int(card S) - 1" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs" 
+    by (simp add: aff_dim_affine_independent aff_independent_finite)
+  show "?rhs \<Longrightarrow> ?lhs" 
+    by (metis of_nat_eq_iff affine_basis_exists aff_dim_unique card_subset_eq diff_add_cancel)
+qed
 
 lemma aff_dim_sing [simp]:
   fixes a :: "'n::euclidean_space"
@@ -1272,78 +1092,39 @@
   fixes V :: "('n::euclidean_space) set"
   shows "\<exists>B. B \<subseteq> V \<and> affine hull B = affine hull V \<and>
     \<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1"
-proof -
-  obtain B where B: "\<not> affine_dependent B" "B \<subseteq> V" "affine hull B = affine hull V"
-    using affine_basis_exists[of V] by auto
-  then have "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto
-  with B show ?thesis by auto
-qed
+  by (metis aff_dim_unique affine_basis_exists)
 
 lemma aff_dim_le_card:
   fixes V :: "'n::euclidean_space set"
   assumes "finite V"
   shows "aff_dim V \<le> of_nat (card V) - 1"
-proof -
-  obtain B where B: "B \<subseteq> V" "of_nat (card B) = aff_dim V + 1"
-    using aff_dim_inner_basis_exists[of V] by auto
-  then have "card B \<le> card V"
-    using assms card_mono by auto
-  with B show ?thesis by auto
+  by (metis aff_dim_inner_basis_exists assms card_mono le_diff_eq of_nat_le_iff)
+
+lemma aff_dim_parallel_le:
+  fixes S T :: "'n::euclidean_space set"
+  assumes "affine_parallel (affine hull S) (affine hull T)"
+  shows "aff_dim S \<le> aff_dim T"
+proof (cases "S={} \<or> T={}")
+  case True
+  then show ?thesis
+    by (smt (verit, best) aff_dim_affine_hull2 affine_hull_empty affine_parallel_def assms empty_is_image)
+next
+  case False
+    then obtain L where L: "subspace L" "affine_parallel (affine hull T) L"
+      by (metis affine_affine_hull affine_hull_eq_empty affine_parallel_subspace)
+    with False show ?thesis
+      by (metis aff_dim_parallel_subspace affine_parallel_assoc assms dual_order.refl)
 qed
 
 lemma aff_dim_parallel_eq:
   fixes S T :: "'n::euclidean_space set"
   assumes "affine_parallel (affine hull S) (affine hull T)"
   shows "aff_dim S = aff_dim T"
-proof -
-  {
-    assume "T \<noteq> {}" "S \<noteq> {}"
-    then obtain L where L: "subspace L \<and> affine_parallel (affine hull T) L"
-      using affine_parallel_subspace[of "affine hull T"]
-        affine_affine_hull[of T]
-      by auto
-    then have "aff_dim T = int (dim L)"
-      using aff_dim_parallel_subspace \<open>T \<noteq> {}\<close> by auto
-    moreover have *: "subspace L \<and> affine_parallel (affine hull S) L"
-       using L affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto
-    moreover from * have "aff_dim S = int (dim L)"
-      using aff_dim_parallel_subspace \<open>S \<noteq> {}\<close> by auto
-    ultimately have ?thesis by auto
-  }
-  moreover
-  {
-    assume "S = {}"
-    then have "S = {}" and "T = {}"
-      using assms
-      unfolding affine_parallel_def
-      by auto
-    then have ?thesis using aff_dim_empty by auto
-  }
-  moreover
-  {
-    assume "T = {}"
-    then have "S = {}" and "T = {}"
-      using assms
-      unfolding affine_parallel_def
-      by auto
-    then have ?thesis
-      using aff_dim_empty by auto
-  }
-  ultimately show ?thesis by blast
-qed
+  by (smt (verit, del_insts) aff_dim_parallel_le affine_parallel_commute assms)
 
 lemma aff_dim_translation_eq:
   "aff_dim ((+) a ` S) = aff_dim S" for a :: "'n::euclidean_space"
-proof -
-  have "affine_parallel (affine hull S) (affine hull ((\<lambda>x. a + x) ` S))"
-    unfolding affine_parallel_def
-    apply (rule exI[of _ "a"])
-    using affine_hull_translation[of a S]
-    apply auto
-    done
-  then show ?thesis
-    using aff_dim_parallel_eq[of S "(\<lambda>x. a + x) ` S"] by auto
-qed
+  by (metis aff_dim_parallel_eq affine_hull_translation affine_parallel_def)
 
 lemma aff_dim_translation_eq_subtract:
   "aff_dim ((\<lambda>x. x - a) ` S) = aff_dim S" for a :: "'n::euclidean_space"
@@ -1351,97 +1132,51 @@
 
 lemma aff_dim_affine:
   fixes S L :: "'n::euclidean_space set"
-  assumes "S \<noteq> {}"
-    and "affine S"
-    and "subspace L"
-    and "affine_parallel S L"
+  assumes "affine S" "subspace L" "affine_parallel S L" "S \<noteq> {}"
   shows "aff_dim S = int (dim L)"
-proof -
-  have *: "affine hull S = S"
-    using assms affine_hull_eq[of S] by auto
-  then have "affine_parallel (affine hull S) L"
-    using assms by (simp add: *)
-  then show ?thesis
-    using assms aff_dim_parallel_subspace[of S L] by blast
-qed
+  by (simp add: aff_dim_parallel_subspace assms hull_same)
 
-lemma dim_affine_hull:
+lemma dim_affine_hull [simp]:
   fixes S :: "'n::euclidean_space set"
   shows "dim (affine hull S) = dim S"
-proof -
-  have "dim (affine hull S) \<ge> dim S"
-    using dim_subset by auto
-  moreover have "dim (span S) \<ge> dim (affine hull S)"
-    using dim_subset affine_hull_subset_span by blast
-  moreover have "dim (span S) = dim S"
-    using dim_span by auto
-  ultimately show ?thesis by auto
-qed
+  by (metis affine_hull_subset_span dim_eq_span dim_mono hull_subset span_eq_dim)
 
 lemma aff_dim_subspace:
   fixes S :: "'n::euclidean_space set"
   assumes "subspace S"
   shows "aff_dim S = int (dim S)"
-proof (cases "S={}")
-  case True with assms show ?thesis
-    by (simp add: subspace_affine)
-next
-  case False
-  with aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] subspace_affine
-  show ?thesis by auto
-qed
+  by (metis aff_dim_affine affine_parallel_subspace assms empty_iff parallel_subspace subspace_affine)
 
 lemma aff_dim_zero:
   fixes S :: "'n::euclidean_space set"
   assumes "0 \<in> affine hull S"
   shows "aff_dim S = int (dim S)"
-proof -
-  have "subspace (affine hull S)"
-    using subspace_affine[of "affine hull S"] affine_affine_hull assms
-    by auto
-  then have "aff_dim (affine hull S) = int (dim (affine hull S))"
-    using assms aff_dim_subspace[of "affine hull S"] by auto
-  then show ?thesis
-    using aff_dim_affine_hull[of S] dim_affine_hull[of S]
-    by auto
-qed
+  by (metis aff_dim_affine_hull aff_dim_subspace affine_hull_span_0 assms dim_span subspace_span)
 
 lemma aff_dim_eq_dim:
-  "aff_dim S = int (dim ((+) (- a) ` S))" if "a \<in> affine hull S"
-    for S :: "'n::euclidean_space set"
-proof -
-  have "0 \<in> affine hull (+) (- a) ` S"
-    unfolding affine_hull_translation
-    using that by (simp add: ac_simps)
-  with aff_dim_zero show ?thesis
-    by (metis aff_dim_translation_eq)
-qed
+  fixes S :: "'n::euclidean_space set"
+  assumes "a \<in> affine hull S"
+  shows "aff_dim S = int (dim ((+) (- a) ` S))" 
+  by (metis ab_left_minus aff_dim_translation_eq aff_dim_zero affine_hull_translation image_eqI assms)
 
 lemma aff_dim_eq_dim_subtract:
-  "aff_dim S = int (dim ((\<lambda>x. x - a) ` S))" if "a \<in> affine hull S"
-    for S :: "'n::euclidean_space set"
-  using aff_dim_eq_dim [of a] that by (simp cong: image_cong_simp)
+  fixes S :: "'n::euclidean_space set"
+  assumes "a \<in> affine hull S"
+  shows "aff_dim S = int (dim ((\<lambda>x. x - a) ` S))"
+  using aff_dim_eq_dim assms by auto
 
 lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
-  using aff_dim_subspace[of "(UNIV :: 'n::euclidean_space set)"]
-    dim_UNIV[where 'a="'n::euclidean_space"]
-  by auto
+  by (simp add: aff_dim_subspace)
 
 lemma aff_dim_geq:
   fixes V :: "'n::euclidean_space set"
   shows "aff_dim V \<ge> -1"
-proof -
-  obtain B where "affine hull B = affine hull V"
-    and "\<not> affine_dependent B"
-    and "int (card B) = aff_dim V + 1"
-    using aff_dim_basis_exists by auto
-  then show ?thesis by auto
-qed
+  by (metis add_le_cancel_right aff_dim_basis_exists diff_self of_nat_0_le_iff uminus_add_conv_diff)
 
 lemma aff_dim_negative_iff [simp]:
   fixes S :: "'n::euclidean_space set"
-  shows "aff_dim S < 0 \<longleftrightarrow>S = {}"
-by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq)
+  shows "aff_dim S < 0 \<longleftrightarrow> S = {}"
+  by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq)
 
 lemma aff_lowdim_subset_hyperplane:
   fixes S :: "'a::euclidean_space set"
@@ -1482,83 +1217,48 @@
   fixes S :: "'a :: euclidean_space set"
   assumes "\<not> affine_dependent S" "a \<in> S"
     shows "card S = dim ((\<lambda>x. x - a) ` S) + 1"
-proof -
-  have non: "\<not> affine_dependent (insert a S)"
-    by (simp add: assms insert_absorb)
-  have "finite S"
-    by (meson assms aff_independent_finite)
-  with \<open>a \<in> S\<close> have "card S \<noteq> 0" by auto
-  moreover have "dim ((\<lambda>x. x - a) ` S) = card S - 1"
-    using aff_dim_eq_dim_subtract aff_dim_unique \<open>a \<in> S\<close> hull_inc insert_absorb non by fastforce
-  ultimately show ?thesis
-    by auto
-qed
+  using aff_dim_affine_independent aff_dim_eq_dim_subtract assms hull_subset by fastforce
 
 lemma independent_card_le_aff_dim:
   fixes B :: "'n::euclidean_space set"
   assumes "B \<subseteq> V"
   assumes "\<not> affine_dependent B"
   shows "int (card B) \<le> aff_dim V + 1"
-proof -
-  obtain T where T: "\<not> affine_dependent T \<and> B \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
-    by (metis assms extend_to_affine_basis[of B V])
-  then have "of_nat (card T) = aff_dim V + 1"
-    using aff_dim_unique by auto
-  then show ?thesis
-    using T card_mono[of T B] aff_independent_finite[of T] by auto
-qed
+  by (metis aff_dim_unique aff_independent_finite assms card_mono extend_to_affine_basis of_nat_mono)
 
 lemma aff_dim_subset:
   fixes S T :: "'n::euclidean_space set"
   assumes "S \<subseteq> T"
   shows "aff_dim S \<le> aff_dim T"
-proof -
-  obtain B where B: "\<not> affine_dependent B" "B \<subseteq> S" "affine hull B = affine hull S"
-    "of_nat (card B) = aff_dim S + 1"
-    using aff_dim_inner_basis_exists[of S] by auto
-  then have "int (card B) \<le> aff_dim T + 1"
-    using assms independent_card_le_aff_dim[of B T] by auto
-  with B show ?thesis by auto
-qed
+  by (metis add_le_cancel_right aff_dim_inner_basis_exists assms dual_order.trans independent_card_le_aff_dim)
 
 lemma aff_dim_le_DIM:
   fixes S :: "'n::euclidean_space set"
   shows "aff_dim S \<le> int (DIM('n))"
-proof -
-  have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
-    using aff_dim_UNIV by auto
-  then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
-    using aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
-qed
+  by (metis aff_dim_UNIV aff_dim_subset top_greatest)
 
 lemma affine_dim_equal:
   fixes S :: "'n::euclidean_space set"
   assumes "affine S" "affine T" "S \<noteq> {}" "S \<subseteq> T" "aff_dim S = aff_dim T"
   shows "S = T"
 proof -
-  obtain a where "a \<in> S" using assms by auto
-  then have "a \<in> T" using assms by auto
+  obtain a where "a \<in> S" "a \<in> T" "T \<noteq> {}" using assms by auto
   define LS where "LS = {y. \<exists>x \<in> S. (-a) + x = y}"
   then have ls: "subspace LS" "affine_parallel S LS"
     using assms parallel_subspace_explicit[of S a LS] \<open>a \<in> S\<close> by auto
   then have h1: "int(dim LS) = aff_dim S"
     using assms aff_dim_affine[of S LS] by auto
-  have "T \<noteq> {}" using assms by auto
   define LT where "LT = {y. \<exists>x \<in> T. (-a) + x = y}"
   then have lt: "subspace LT \<and> affine_parallel T LT"
     using assms parallel_subspace_explicit[of T a LT] \<open>a \<in> T\<close> by auto
-  then have "int(dim LT) = aff_dim T"
-    using assms aff_dim_affine[of T LT] \<open>T \<noteq> {}\<close> by auto
   then have "dim LS = dim LT"
-    using h1 assms by auto
+    using assms aff_dim_affine[of T LT] \<open>T \<noteq> {}\<close>  h1 by auto
   moreover have "LS \<le> LT"
     using LS_def LT_def assms by auto
   ultimately have "LS = LT"
     using subspace_dim_equal[of LS LT] ls lt by auto
-  moreover have "S = {x. \<exists>y \<in> LS. a+y=x}"
-    using LS_def by auto
-  moreover have "T = {x. \<exists>y \<in> LT. a+y=x}"
-    using LT_def by auto
+  moreover have "S = {x. \<exists>y \<in> LS. a+y=x}" "T = {x. \<exists>y \<in> LT. a+y=x}"
+    using LS_def LT_def by auto
   ultimately show ?thesis by auto
 qed
 
@@ -1566,10 +1266,6 @@
   fixes S :: "'a::euclidean_space set"
   shows "aff_dim S = 0 \<longleftrightarrow> (\<exists>a. S = {a})"
 proof (cases "S = {}")
-  case True
-  then show ?thesis
-    by auto
-next
   case False
   then obtain a where "a \<in> S" by auto
   show ?thesis
@@ -1580,58 +1276,39 @@
     then show "\<exists>a. S = {a}"
       using \<open>a \<in> S\<close> by blast
   qed auto
-qed
+qed auto
 
 lemma affine_hull_UNIV:
   fixes S :: "'n::euclidean_space set"
   assumes "aff_dim S = int(DIM('n))"
   shows "affine hull S = (UNIV :: ('n::euclidean_space) set)"
-proof -
-  have "S \<noteq> {}"
-    using assms aff_dim_empty[of S] by auto
-  have h0: "S \<subseteq> affine hull S"
-    using hull_subset[of S _] by auto
-  have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S"
-    using aff_dim_UNIV assms by auto
-  then have h2: "aff_dim (affine hull S) \<le> aff_dim (UNIV :: ('n::euclidean_space) set)"
-    using aff_dim_le_DIM[of "affine hull S"] assms h0 by auto
-  have h3: "aff_dim S \<le> aff_dim (affine hull S)"
-    using h0 aff_dim_subset[of S "affine hull S"] assms by auto
-  then have h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)"
-    using h0 h1 h2 by auto
-  then show ?thesis
-    using affine_dim_equal[of "affine hull S" "(UNIV :: ('n::euclidean_space) set)"]
-      affine_affine_hull[of S] affine_UNIV assms h4 h0 \<open>S \<noteq> {}\<close>
-    by auto
-qed
+  by (simp add: aff_dim_empty affine_dim_equal assms)
 
 lemma disjoint_affine_hull:
-  fixes s :: "'n::euclidean_space set"
-  assumes "\<not> affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
-    shows "(affine hull t) \<inter> (affine hull u) = {}"
+  fixes S :: "'n::euclidean_space set"
+  assumes "\<not> affine_dependent S" "T \<subseteq> S" "U \<subseteq> S" "T \<inter> U = {}"
+    shows "(affine hull T) \<inter> (affine hull U) = {}"
 proof -
-  from assms(1) have "finite s"
-    by (simp add: aff_independent_finite)
-  with assms(2,3) have "finite t" "finite u"
-    by (blast intro: finite_subset)+
-  have False if "y \<in> affine hull t" and "y \<in> affine hull u" for y
+  obtain "finite S" "finite T" "finite U"
+    using assms by (simp add: aff_independent_finite finite_subset)
+  have False if "y \<in> affine hull T" and "y \<in> affine hull U" for y
   proof -
     from that obtain a b
-      where a1 [simp]: "sum a t = 1"
-        and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) t = y"
-        and [simp]: "sum b u = 1" "sum (\<lambda>v. b v *\<^sub>R v) u = y"
-      by (auto simp: affine_hull_finite \<open>finite t\<close> \<open>finite u\<close>)
-    define c where "c x = (if x \<in> t then a x else if x \<in> u then -(b x) else 0)" for x
-    from assms(2,3,4) have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u"
-      by auto
-    have "sum c s = 0"
-      by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite s\<close> sum_negf)
-    moreover have "\<not> (\<forall>v\<in>s. c v = 0)"
-      by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum.neutral zero_neq_one)
-    moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
-      by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases \<open>finite s\<close>)
+      where a1 [simp]: "sum a T = 1"
+        and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) T = y"
+        and [simp]: "sum b U = 1" "sum (\<lambda>v. b v *\<^sub>R v) U = y"
+      by (auto simp: affine_hull_finite \<open>finite T\<close> \<open>finite U\<close>)
+    define c where "c x = (if x \<in> T then a x else if x \<in> U then -(b x) else 0)" for x
+    have [simp]: "S \<inter> T = T" "S \<inter> - T \<inter> U = U"
+      using assms by auto
+    have "sum c S = 0"
+      by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite S\<close> sum_negf)
+    moreover have "\<not> (\<forall>v\<in>S. c v = 0)"
+      by (metis (no_types) IntD1 \<open>S \<inter> T = T\<close> a1 c_def sum.neutral zero_neq_one)
+    moreover have "(\<Sum>v\<in>S. c v *\<^sub>R v) = 0"
+      by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases \<open>finite S\<close>)
     ultimately show ?thesis
-      using assms(1) \<open>finite s\<close> by (auto simp: affine_dependent_explicit)
+      using assms(1) \<open>finite S\<close> by (auto simp: affine_dependent_explicit)
   qed
   then show ?thesis by blast
 qed
diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -77,13 +77,7 @@
         using of_rat_dense by blast
       assume * [rule_format]: "\<forall>d>0. \<exists>x\<in>A. x \<noteq> a \<and> dist x a < d \<and> \<not> l < f x"
       from q2 have "real_of_rat q2 < f a \<and> (\<forall>x\<in>A. x < a \<longrightarrow> f x < real_of_rat q2)"
-      proof auto
-        fix x assume "x \<in> A" "x < a"
-        with q2 *[of "a - x"] show "f x < real_of_rat q2"
-          apply (auto simp add: dist_real_def not_less)
-          apply (subgoal_tac "f x \<le> f xa")
-          by (auto intro: mono)
-      qed
+        using q2 *[of "a - _"] dist_real_def mono by fastforce
       thus ?thesis by auto
     next
       fix u assume "u > f a"
@@ -91,13 +85,7 @@
         using of_rat_dense by blast
       assume *[rule_format]: "\<forall>d>0. \<exists>x\<in>A. x \<noteq> a \<and> dist x a < d \<and> \<not> u > f x"
       from q2 have "real_of_rat q2 > f a \<and> (\<forall>x\<in>A. x > a \<longrightarrow> f x > real_of_rat q2)"
-      proof auto
-        fix x assume "x \<in> A" "x > a"
-        with q2 *[of "x - a"] show "f x > real_of_rat q2"
-          apply (auto simp add: dist_real_def)
-          apply (subgoal_tac "f x \<ge> f xa")
-          by (auto intro: mono)
-      qed
+        using q2 *[of "_ - a"] dist_real_def mono by fastforce
       thus ?thesis by auto
     qed
   qed
@@ -127,13 +115,8 @@
   fixes A :: "real set"
   assumes "open A" "mono_on A f"
   shows "countable {a\<in>A. \<not>isCont f a}"
-proof -
-  have "{a\<in>A. \<not>isCont f a} = {a\<in>A. \<not>(continuous (at a within A) f)}"
-    by (auto simp add: continuous_within_open [OF _ \<open>open A\<close>])
-  thus ?thesis
-    apply (elim ssubst)
-    by (rule mono_on_ctble_discont, rule assms)
-qed
+  using continuous_within_open [OF _ \<open>open A\<close>] \<open>mono_on A f\<close>
+  by (smt (verit, ccfv_threshold) Collect_cong mono_on_ctble_discont)
 
 lemma mono_ctble_discont:
   fixes f :: "real \<Rightarrow> real"
@@ -144,8 +127,7 @@
 lemma has_real_derivative_imp_continuous_on:
   assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
   shows "continuous_on A f"
-  apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
-  using assms differentiable_at_withinI real_differentiable_def by blast
+  by (meson DERIV_isCont assms continuous_at_imp_continuous_on)
 
 lemma continuous_interval_vimage_Int:
   assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
@@ -173,14 +155,11 @@
              intro!: mono)
   moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
   moreover have "g c' \<le> c" "g d' \<ge> d"
-    apply (insert c'' d'' c'd'_in_set)
-    apply (subst c''(2)[symmetric])
-    apply (auto simp: c'_def intro!: mono cInf_lower c'') []
-    apply (subst d''(2)[symmetric])
-    apply (auto simp: d'_def intro!: mono cSup_upper d'') []
-    done
-  with c'd'_in_set have "g c' = c" "g d' = d" by auto
-  ultimately show ?thesis using that by blast
+    using c'' d'' calculation by (metis IntE atLeastAtMost_iff mono order_class.order_eq_iff)+
+  with c'd'_in_set have "g c' = c" "g d' = d" 
+    by auto
+  ultimately show ?thesis 
+    using that by blast
 qed
 
 subsection \<open>Generic Borel spaces\<close>
@@ -196,9 +175,7 @@
   by (auto simp add: measurable_def borel_def)
 
 lemma in_borel_measurable_borel:
-   "f \<in> borel_measurable M \<longleftrightarrow>
-    (\<forall>S \<in> sets borel.
-      f -` S \<inter> space M \<in> sets M)"
+   "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>S \<in> sets borel. f -` S \<inter> space M \<in> sets M)"
   by (auto simp add: measurable_def borel_def)
 
 lemma space_borel[simp]: "space borel = UNIV"
@@ -219,10 +196,7 @@
 
 lemma borel_open[measurable (raw generic)]:
   assumes "open A" shows "A \<in> sets borel"
-proof -
-  have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
-  thus ?thesis unfolding borel_def by auto
-qed
+  by (simp add: assms sets_borel)
 
 lemma borel_closed[measurable (raw generic)]:
   assumes "closed A" shows "A \<in> sets borel"
@@ -237,12 +211,7 @@
   unfolding insert_def by (rule sets.Un) auto
 
 lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV"
-proof -
-  have "(\<Union>a\<in>A. {a}) \<in> sets borel" for A :: "'a set"
-    by (intro sets.countable_UN') auto
-  then show ?thesis
-    by auto
-qed
+  by (simp add: set_eq_iff sets.countable)
 
 lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
   unfolding Compl_eq_Diff_UNIV by simp
@@ -312,7 +281,7 @@
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
   by (subst measurable_restrict_space_iff)
-     (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
+     (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a] cong: if_cong)
 
 lemma borel_measurable_restrict_space_iff_ennreal:
   fixes f :: "'a \<Rightarrow> ennreal"
@@ -320,7 +289,7 @@
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
   by (subst measurable_restrict_space_iff)
-     (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
+     (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a] cong: if_cong)
 
 lemma borel_measurable_restrict_space_iff:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
@@ -329,7 +298,7 @@
     (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
   by (subst measurable_restrict_space_iff)
      (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps
-       cong del: if_weak_cong)
+       cong: if_cong)
 
 lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
   by (auto intro: borel_closed)
@@ -338,7 +307,7 @@
   by (auto intro: borel_open)
 
 lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel"
-  by (auto intro: borel_closed dest!: compact_imp_closed)
+  by (simp add: borel_closed compact_imp_closed)
 
 lemma borel_sigma_sets_subset:
   "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
@@ -360,7 +329,7 @@
     using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto
   finally show "sigma_sets UNIV {S. open S} \<subseteq> sigma_sets UNIV (F`A)" .
   show "sigma_sets UNIV (F`A) \<subseteq> sigma_sets UNIV {S. open S}"
-    unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto
+    by (metis F image_subset_iff sets_borel sigma_sets_mono)
 qed auto
 
 lemma borel_eq_sigmaI2:
@@ -371,7 +340,7 @@
   assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel"
   shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)"
   using assms
-  by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` B" and F="(\<lambda>(i, j). F i j)"]) auto
+  by (smt (verit, del_insts) borel_eq_sigmaI1 image_iff prod.collapse split_beta)
 
 lemma borel_eq_sigmaI3:
   fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
@@ -443,20 +412,15 @@
 qed (auto simp: eq intro: generate_topology.Basis)
 
 lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
-  unfolding borel_def
-proof (intro sigma_eqI sigma_sets_eqI, safe)
-  fix x :: "'a set" assume "open x"
-  hence "x = UNIV - (UNIV - x)" by auto
-  also have "\<dots> \<in> sigma_sets UNIV (Collect closed)"
-    by (force intro: sigma_sets.Compl simp: \<open>open x\<close>)
-  finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp
-next
-  fix x :: "'a set" assume "closed x"
-  hence "x = UNIV - (UNIV - x)" by auto
-  also have "\<dots> \<in> sigma_sets UNIV (Collect open)"
-    by (force intro: sigma_sets.Compl simp: \<open>closed x\<close>)
-  finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
-qed simp_all
+proof -
+  have "x \<in> sigma_sets UNIV (Collect closed)" 
+     if  "open x" for x :: "'a set"
+    by (metis that Compl_eq_Diff_UNIV closed_Compl double_complement mem_Collect_eq 
+        sigma_sets.Basic sigma_sets.Compl)
+  then show ?thesis
+    unfolding borel_def
+    by (metis Pow_UNIV borel_closed mem_Collect_eq sets_borel sigma_eqI sigma_sets_eqI top_greatest)
+qed
 
 proposition borel_eq_countable_basis:
   fixes B::"'a::topological_space set set"
@@ -517,8 +481,7 @@
 lemma borel_measurable_continuous_on_indicator:
   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "A \<in> sets borel \<Longrightarrow> continuous_on A f \<Longrightarrow> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable borel"
-  by (subst borel_measurable_restrict_space_iff[symmetric])
-     (auto intro: borel_measurable_continuous_on_restrict)
+  using borel_measurable_continuous_on_restrict borel_measurable_restrict_space_iff inf_top.right_neutral by blast
 
 lemma borel_measurable_Pair[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
@@ -720,7 +683,7 @@
   shows "(\<lambda>x. SUP i\<in>I. F i x) \<in> borel_measurable M"
 proof cases
   assume "I = {}" then show ?thesis
-    unfolding \<open>I = {}\<close> image_empty by simp
+    by (simp add: borel_measurable_const)
 next
   assume "I \<noteq> {}"
   show ?thesis
@@ -742,7 +705,7 @@
   shows "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable M"
 proof cases
   assume "I = {}" then show ?thesis
-    unfolding \<open>I = {}\<close> image_empty by simp
+    by (simp add: borel_measurable_const)
 next
   assume "I \<noteq> {}"
   show ?thesis
@@ -1045,25 +1008,23 @@
 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
   fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
   then have i: "i \<in> Basis" by auto
-  have "{x::'a. x\<bullet>i \<le> a} = UNIV - {x::'a. a < x\<bullet>i}" by auto
-  also have *: "{x::'a. a < x\<bullet>i} =
-      (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
-  proof (safe, simp_all add: eucl_less_def split: if_split_asm)
-    fix x :: 'a
+  have **: "\<exists>y. \<forall>j\<in>Basis. j \<noteq> i \<longrightarrow> - real y < x \<bullet> j" if "a < x \<bullet> i" for x
+  proof -
     obtain k where k: "Max ((\<bullet>) (- x) ` Basis) < real k"
       using reals_Archimedean2 by blast
     { fix i :: 'a assume "i \<in> Basis"
       then have "-x\<bullet>i < real k"
         using k by (subst (asm) Max_less_iff) auto
       then have "- real k < x\<bullet>i" by simp }
-    then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> -real k < x \<bullet> ia"
+    then show ?thesis
       by (auto intro!: exI[of _ k])
   qed
-  finally show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA"
-    apply (simp only:)
-    apply (intro sets.countable_UN sets.Diff)
-    apply (auto intro: sigma_sets_top)
-    done
+  have "{x::'a. x\<bullet>i \<le> a} = UNIV - {x::'a. a < x\<bullet>i}" by auto
+  also have *: "{x::'a. a < x\<bullet>i} = (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -k) *\<^sub>R n) <e x})" 
+    using i ** by (force simp add: eucl_less_def split: if_split_asm)
+  finally have eq: "{x. x \<bullet> i \<le> a} = UNIV - (\<Union>x. {xa. (\<Sum>n\<in>Basis. (if n = i then a else - real x) *\<^sub>R n) <e xa})" .
+  show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA"
+    unfolding eq by (fastforce intro!: sigma_sets_top sets.Diff)
 qed auto
 
 lemma borel_eq_lessThan:
@@ -1072,24 +1033,26 @@
 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge])
   fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
   then have i: "i \<in> Basis" by auto
-  have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
-  also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using \<open>i\<in> Basis\<close>
-  proof (safe, simp_all add: eucl_less_def split: if_split_asm)
-    fix x :: 'a
+  have **: "\<exists>y. \<forall>j\<in>Basis. j \<noteq> i \<longrightarrow> real y > x \<bullet> j" if "a > x \<bullet> i" for x
+  proof -
     obtain k where k: "Max ((\<bullet>) x ` Basis) < real k"
       using reals_Archimedean2 by blast
     { fix i :: 'a assume "i \<in> Basis"
       then have "x\<bullet>i < real k"
         using k by (subst (asm) Max_less_iff) auto
       then have "x\<bullet>i < real k" by simp }
-    then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> x \<bullet> ia < real k"
+    then show ?thesis
       by (auto intro!: exI[of _ k])
   qed
-  finally show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA"
-    apply (simp only:)
-    apply (intro sets.countable_UN sets.Diff)
-    apply (auto intro: sigma_sets_top )
-    done
+  have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
+  also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using \<open>i\<in> Basis\<close>
+    using i ** by (force simp add: eucl_less_def split: if_split_asm)
+  finally
+  have eq: "{x. a \<le> x \<bullet> i} =
+            UNIV - (\<Union>k. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" .
+
+  show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA"
+    unfolding eq by (fastforce intro!: sigma_sets_top sets.Diff)
 qed auto
 
 lemma borel_eq_atLeastAtMost:
@@ -1276,9 +1239,7 @@
 lemma borel_measurable_uminus_eq [simp]:
   fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   shows "(\<lambda>x. - f x) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
-proof
-  assume ?l from borel_measurable_uminus[OF this] show ?r by simp
-qed auto
+  by (smt (verit, ccfv_SIG) borel_measurable_uminus equation_minus_iff measurable_cong)
 
 lemma affine_borel_measurable_vector:
   fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
@@ -1294,8 +1255,10 @@
       by (auto simp: algebra_simps)
     hence "?S \<in> sets borel" by auto
     moreover
-    from \<open>b \<noteq> 0\<close> have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"
-      apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all)
+    have "\<And>x. \<lbrakk>a + b *\<^sub>R f x \<in> S\<rbrakk> \<Longrightarrow> f x \<in> (\<lambda>x. (x - a) /\<^sub>R b) ` S"
+      using \<open>b \<noteq> 0\<close> image_iff by fastforce
+    with \<open>b \<noteq> 0\<close> have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"
+      by auto
     ultimately show ?thesis using assms unfolding in_borel_measurable_borel
       by auto
   qed simp
@@ -1313,10 +1276,12 @@
   fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra"
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
-  apply (rule measurable_compose[OF f])
-  apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
-  apply (auto intro!: continuous_on_inverse continuous_on_id)
-  done
+proof -
+  have "countable {0::'b}" "continuous_on (- {0::'b}) inverse"
+    by (auto intro!: continuous_on_inverse continuous_on_id)
+  then show ?thesis
+    by (metis borel_measurable_continuous_countable_exceptions f measurable_compose)
+qed
 
 lemma borel_measurable_divide[measurable (raw)]:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
@@ -1341,10 +1306,8 @@
 lemma borel_measurable_ln[measurable (raw)]:
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. ln (f x :: real)) \<in> borel_measurable M"
-  apply (rule measurable_compose[OF f])
-  apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
-  apply (auto intro!: continuous_on_ln continuous_on_id)
-  done
+  using borel_measurable_continuous_countable_exceptions[of "{0}"] measurable_compose[OF f]
+  by (auto intro!: continuous_on_ln continuous_on_id)
 
 lemma borel_measurable_log[measurable (raw)]:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
@@ -1402,12 +1365,16 @@
 
 lemma\<^marker>\<open>tag important\<close> borel_measurable_complex_iff:
   "f \<in> borel_measurable M \<longleftrightarrow>
-    (\<lambda>x. Re (f x)) \<in> borel_measurable M \<and> (\<lambda>x. Im (f x)) \<in> borel_measurable M"
-  apply auto
-  apply (subst fun_complex_eq)
-  apply (intro borel_measurable_add)
-  apply auto
-  done
+    (\<lambda>x. Re (f x)) \<in> borel_measurable M \<and> (\<lambda>x. Im (f x)) \<in> borel_measurable M" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    using borel_measurable_Im borel_measurable_Re measurable_compose by blast
+  assume R: ?rhs
+  then have "(\<lambda>x. complex_of_real (Re (f x)) + \<i> * complex_of_real (Im (f x))) \<in> borel_measurable M"
+    by (intro borel_measurable_add) auto
+  then show ?lhs
+    using complex_eq by force
+qed
 
 lemma powr_real_measurable [measurable]:
   assumes "f \<in> measurable M borel" "g \<in> measurable M borel"
@@ -1427,10 +1394,8 @@
   fixes f :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. real_of_ereal (f x)) \<in> borel_measurable M"
-  apply (rule measurable_compose[OF f])
-  apply (rule borel_measurable_continuous_countable_exceptions[of "{\<infinity>, -\<infinity> }"])
-  apply (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV)
-  done
+  using measurable_compose[OF f] borel_measurable_continuous_countable_exceptions[of "{\<infinity>, -\<infinity> }"]
+  by (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV)
 
 lemma borel_measurable_ereal_cases:
   fixes f :: "'a \<Rightarrow> ereal"
@@ -1451,10 +1416,8 @@
   by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
 
 lemma borel_measurable_uminus_eq_ereal[simp]:
-  "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
-proof
-  assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
-qed auto
+  "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
+  by (smt (verit, ccfv_SIG) borel_measurable_uminus_ereal ereal_uminus_uminus measurable_cong)
 
 lemma set_Collect_ereal2:
   fixes f g :: "'a \<Rightarrow> ereal"
@@ -1511,13 +1474,7 @@
 
 lemma vimage_sets_compl_iff:
   "f -` A \<inter> space M \<in> sets M \<longleftrightarrow> f -` (- A) \<inter> space M \<in> sets M"
-proof -
-  { fix A assume "f -` A \<inter> space M \<in> sets M"
-    moreover have "f -` (- A) \<inter> space M = space M - f -` A \<inter> space M" by auto
-    ultimately have "f -` (- A) \<inter> space M \<in> sets M" by auto }
-  from this[of A] this[of "-A"] show ?thesis
-    by (metis double_complement)
-qed
+  by (metis Diff_Compl Diff_Diff_Int diff_eq inf_aci(1) sets.Diff sets.top vimage_Compl)
 
 lemma borel_measurable_iff_Iic_ereal:
   "(f::'a\<Rightarrow>ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
@@ -1741,7 +1698,7 @@
 lemma Collect_closed_imp_pred_borel: "closed {x. P x} \<Longrightarrow> Measurable.pred borel P"
   by (simp add: pred_def)
 
-(* Proof by Jeremy Avigad and Luke Serafin *)
+text \<open>Proof by Jeremy Avigad and Luke Serafin\<close>
 lemma isCont_borel_pred[measurable]:
   fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
   shows "Measurable.pred borel (isCont f)"
@@ -1821,12 +1778,19 @@
   fixes f :: "real \<Rightarrow> real" and A :: "real set"
   assumes "mono_on A f"
   shows "f \<in> borel_measurable (restrict_space borel A)"
-  apply (rule measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]])
-  apply (auto intro!: image_eqI[where x="{x}" for x] simp: sets_restrict_space)
-  apply (auto simp add: sets_restrict_restrict_space continuous_on_eq_continuous_within
-              cong: measurable_cong_sets
-              intro!: borel_measurable_continuous_on_restrict intro: continuous_within_subset)
-  done
+proof -
+  have "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets (restrict_space borel A)"
+    using sets_restrict_space by fastforce
+  moreover
+  have "continuous_on (A \<inter> - {a \<in> A. \<not> continuous (at a within A) f}) f"
+    by (force simp: continuous_on_eq_continuous_within intro: continuous_within_subset)
+  then have "f \<in> borel_measurable (restrict_space (restrict_space borel A) 
+              (- {a \<in> A. \<not> continuous (at a within A) f}))"
+    by (smt (verit, best) borel_measurable_continuous_on_restrict measurable_cong_sets sets_restrict_restrict_space)
+  ultimately show ?thesis
+    using measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]]
+    by (smt (verit, del_insts) UNIV_I mem_Collect_eq space_borel)
+qed
 
 lemma borel_measurable_piecewise_mono:
   fixes f::"real \<Rightarrow> real" and C::"real set set"
@@ -1920,7 +1884,6 @@
   fixes f g::"_\<Rightarrow> 'a::{second_countable_topology, t2_space}"
   assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   shows "{x \<in> space M. f x = g x} \<in> sets M"
-
 proof -
   define A where "A = {x \<in> space M. f x = g x}"
   define B where "B = {y. \<exists>x::'a. y = (x,x)}"
@@ -1931,33 +1894,8 @@
   then show ?thesis unfolding A_def by simp
 qed
 
-lemma measurable_inequality_set [measurable]:
-  fixes f g::"_ \<Rightarrow> 'a::{second_countable_topology, linorder_topology}"
-  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-  shows "{x \<in> space M. f x \<le> g x} \<in> sets M"
-        "{x \<in> space M. f x < g x} \<in> sets M"
-        "{x \<in> space M. f x \<ge> g x} \<in> sets M"
-        "{x \<in> space M. f x > g x} \<in> sets M"
-proof -
-  define F where "F = (\<lambda>x. (f x, g x))"
-  have * [measurable]: "F \<in> borel_measurable M" unfolding F_def by simp
-
-  have "{x \<in> space M. f x \<le> g x} = F-`{(x, y) | x y. x \<le> y} \<inter> space M" unfolding F_def by auto
-  moreover have "{(x, y) | x y. x \<le> (y::'a)} \<in> sets borel" using closed_subdiagonal borel_closed by blast
-  ultimately show "{x \<in> space M. f x \<le> g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets)
-
-  have "{x \<in> space M. f x < g x} = F-`{(x, y) | x y. x < y} \<inter> space M" unfolding F_def by auto
-  moreover have "{(x, y) | x y. x < (y::'a)} \<in> sets borel" using open_subdiagonal borel_open by blast
-  ultimately show "{x \<in> space M. f x < g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets)
-
-  have "{x \<in> space M. f x \<ge> g x} = F-`{(x, y) | x y. x \<ge> y} \<inter> space M" unfolding F_def by auto
-  moreover have "{(x, y) | x y. x \<ge> (y::'a)} \<in> sets borel" using closed_superdiagonal borel_closed by blast
-  ultimately show "{x \<in> space M. f x \<ge> g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets)
-
-  have "{x \<in> space M. f x > g x} = F-`{(x, y) | x y. x > y} \<inter> space M" unfolding F_def by auto
-  moreover have "{(x, y) | x y. x > (y::'a)} \<in> sets borel" using open_superdiagonal borel_open by blast
-  ultimately show "{x \<in> space M. f x > g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets)
-qed
+lemmas measurable_inequality_set [measurable] =
+  borel_measurable_le borel_measurable_less borel_measurable_le borel_measurable_less
 
 proposition measurable_limit [measurable]:
   fixes f::"nat \<Rightarrow> 'a \<Rightarrow> 'b::first_countable_topology"
@@ -2051,8 +1989,8 @@
 lemma measurable_restrict_mono:
   assumes f: "f \<in> restrict_space M A \<rightarrow>\<^sub>M N" and "B \<subseteq> A"
   shows "f \<in> restrict_space M B \<rightarrow>\<^sub>M N"
-by (rule measurable_compose[OF measurable_restrict_space3 f])
-   (insert \<open>B \<subseteq> A\<close>, auto)
+  by (rule measurable_compose[OF measurable_restrict_space3 f]) (use \<open>B \<subseteq> A\<close> in auto)
+
 
 text \<open>The next one is a variation around \<open>measurable_piecewise_restrict\<close>.\<close>
 
@@ -2065,22 +2003,27 @@
   fix B assume [measurable]: "B \<in> sets N"
   {
     fix n::nat
-    obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" using assms(3) by blast
+    obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" 
+      using assms(3) by blast
     then have *: "f-`B \<inter> A n = h-`B \<inter> A n" by auto
-    have "h-`B \<inter> A n = h-`B \<inter> space M \<inter> A n" using assms(2) sets.sets_into_space by auto
-    then have "h-`B \<inter> A n \<in> sets M" by simp
-    then have "f-`B \<inter> A n \<in> sets M" using * by simp
+    have "h-`B \<inter> A n = h-`B \<inter> space M \<inter> A n" 
+      using assms(2) sets.sets_into_space by auto
+    then have "f-`B \<inter> A n \<in> sets M"
+      by (simp add: "*")
   }
-  then have "(\<Union>n. f-`B \<inter> A n) \<in> sets M" by measurable
-  moreover have "f-`B \<inter> space M = (\<Union>n. f-`B \<inter> A n)" using assms(2) by blast
+  then have "(\<Union>n. f-`B \<inter> A n) \<in> sets M" 
+    by measurable
+  moreover have "f-`B \<inter> space M = (\<Union>n. f-`B \<inter> A n)" 
+    using assms(2) by blast
   ultimately show "f-`B \<inter> space M \<in> sets M" by simp
 next
   fix x assume "x \<in> space M"
-  then obtain n where "x \<in> A n" using assms(2) by blast
-  obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" using assms(3) by blast
-  then have "f x = h x" using \<open>x \<in> A n\<close> by blast
-  moreover have "h x \<in> space N" by (metis measurable_space \<open>x \<in> space M\<close> \<open>h \<in> measurable M N\<close>)
-  ultimately show "f x \<in> space N" by simp
+  then obtain n where "x \<in> A n" 
+    using assms(2) by blast
+  obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" 
+    using assms(3) by blast
+  then show "f x \<in> space N"
+    by (metis \<open>x \<in> A n\<close> \<open>x \<in> space M\<close> measurable_space)
 qed
 
 end
diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -138,25 +138,23 @@
   fixes l::complex
   assumes "(f \<longlongrightarrow> l) F" and "\<not> trivial_limit F" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
   shows  "l \<in> \<real>"
-proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
-  show "eventually (\<lambda>x. f x \<in> \<real>) F"
-    using assms(3, 4) by (auto intro: eventually_mono)
-qed
+  using Lim_in_closed_set[OF closed_complex_Reals] assms
+  by (smt (verit) eventually_mono)
 
 lemma real_lim_sequentially:
   fixes l::complex
   shows "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
-by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially)
+  by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially)
 
 lemma real_series:
   fixes l::complex
   shows "f sums l \<Longrightarrow> (\<And>n. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
-unfolding sums_def
-by (metis real_lim_sequentially sum_in_Reals)
+  unfolding sums_def
+  by (metis real_lim_sequentially sum_in_Reals)
 
 lemma Lim_null_comparison_Re:
   assumes "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g \<longlongrightarrow> 0) F" shows "(f \<longlongrightarrow> 0) F"
-  by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp
+  using Lim_null_comparison assms tendsto_Re by fastforce
 
 subsection\<open>Holomorphic functions\<close>
 
@@ -191,25 +189,11 @@
 lemma holomorphic_on_UN_open:
   assumes "\<And>n. n \<in> I \<Longrightarrow> f holomorphic_on A n" "\<And>n. n \<in> I \<Longrightarrow> open (A n)"
   shows   "f holomorphic_on (\<Union>n\<in>I. A n)"
-proof -
-  have "f field_differentiable at z within (\<Union>n\<in>I. A n)" if "z \<in> (\<Union>n\<in>I. A n)" for z
-  proof -
-    from that obtain n where "n \<in> I" "z \<in> A n"
-      by blast
-    hence "f holomorphic_on A n" "open (A n)"
-      by (simp add: assms)+
-    with \<open>z \<in> A n\<close> have "f field_differentiable at z"
-      by (auto simp: holomorphic_on_open field_differentiable_def)
-    thus ?thesis
-      by (meson field_differentiable_at_within)
-  qed
-  thus ?thesis
-    by (auto simp: holomorphic_on_def)
-qed
+  by (metis UN_E assms holomorphic_on_open open_UN)
 
 lemma holomorphic_on_imp_continuous_on:
     "f holomorphic_on s \<Longrightarrow> continuous_on s f"
-  by (metis field_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
+  using differentiable_imp_continuous_on holomorphic_on_imp_differentiable_on by blast
 
 lemma holomorphic_closedin_preimage_constant:
   assumes "f holomorphic_on D" 
@@ -247,22 +231,15 @@
 lemma constant_on_imp_holomorphic_on:
   assumes "f constant_on A"
   shows   "f holomorphic_on A"
-proof -
-  from assms obtain c where c: "\<forall>x\<in>A. f x = c"
-    unfolding constant_on_def by blast
-  have "f holomorphic_on A \<longleftrightarrow> (\<lambda>_. c) holomorphic_on A"
-    by (intro holomorphic_cong) (use c in auto)
-  thus ?thesis
-    by simp
-qed
+  by (metis assms constant_on_def holomorphic_on_const holomorphic_transform)
 
 lemma holomorphic_on_compose:
-  "f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s) \<Longrightarrow> (g o f) holomorphic_on s"
+  "f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s) \<Longrightarrow> (g \<circ> f) holomorphic_on s"
   using field_differentiable_compose_within[of f _ s g]
   by (auto simp: holomorphic_on_def)
 
 lemma holomorphic_on_compose_gen:
-  "f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g o f) holomorphic_on s"
+  "f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g \<circ> f) holomorphic_on s"
   by (metis holomorphic_on_compose holomorphic_on_subset)
 
 lemma holomorphic_on_balls_imp_entire:
@@ -284,15 +261,10 @@
 lemma holomorphic_on_balls_imp_entire':
   assumes "\<And>r. r > 0 \<Longrightarrow> f holomorphic_on ball c r"
   shows   "f holomorphic_on B"
-proof (rule holomorphic_on_balls_imp_entire)
-  {
-    fix M :: real
-    have "\<exists>x. x > max M 0" by (intro gt_ex)
-    hence "\<exists>x>0. x > M" by auto
-  }
-  thus "\<not>bdd_above {(0::real)<..}" unfolding bdd_above_def
-    by (auto simp: not_le)
-qed (insert assms, auto)
+proof (rule holomorphic_on_balls_imp_entire)  
+  show "\<not>bdd_above {(0::real)<..}" unfolding bdd_above_def
+    by (meson greaterThan_iff gt_ex less_le_not_le order_le_less_trans)
+qed (use assms in auto)
 
 lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on A \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on A"
   by (metis field_differentiable_minus holomorphic_on_def)
@@ -357,8 +329,7 @@
 lemma holomorphic_on_Un [holomorphic_intros]:
   assumes "f holomorphic_on A" "f holomorphic_on B" "open A" "open B"
   shows   "f holomorphic_on (A \<union> B)"
-  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A]
-                             at_within_open[of _ B]  at_within_open[of _ "A \<union> B"] open_Un)
+  by (metis Un_iff assms holomorphic_on_open open_Un)
 
 lemma holomorphic_on_If_Un [holomorphic_intros]:
   assumes "f holomorphic_on A" "g holomorphic_on B" "open A" "open B"
@@ -374,19 +345,16 @@
   also have "g holomorphic_on B \<longleftrightarrow> ?h holomorphic_on B"
     using assms by (intro holomorphic_cong) auto
   finally show \<dots> .
-qed (insert assms, auto)
+qed (use assms in auto)
 
 lemma holomorphic_derivI:
-     "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
-      \<Longrightarrow> (f has_field_derivative deriv f x) (at x within T)"
-by (metis DERIV_deriv_iff_field_differentiable at_within_open  holomorphic_on_def has_field_derivative_at_within)
+     "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk> \<Longrightarrow> (f has_field_derivative deriv f x) (at x within T)"
+  by (metis DERIV_deriv_iff_field_differentiable at_within_open  holomorphic_on_def has_field_derivative_at_within)
 
 lemma complex_derivative_transform_within_open:
   "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk>
    \<Longrightarrow> deriv f z = deriv g z"
-  unfolding holomorphic_on_def
-  by (rule DERIV_imp_deriv)
-     (metis DERIV_deriv_iff_field_differentiable has_field_derivative_transform_within_open at_within_open)
+  by (smt (verit) DERIV_imp_deriv has_field_derivative_transform_within_open holomorphic_on_open)
 
 lemma holomorphic_on_compose_cnj_cnj:
   assumes "f holomorphic_on cnj ` A" "open A"
@@ -408,13 +376,13 @@
 subsection\<open>Analyticity on a set\<close>
 
 definition\<^marker>\<open>tag important\<close> analytic_on (infixl "(analytic'_on)" 50)
-  where "f analytic_on S \<equiv> \<forall>x \<in> S. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
+  where "f analytic_on S \<equiv> \<forall>x \<in> S. \<exists>\<epsilon>. 0 < \<epsilon> \<and> f holomorphic_on (ball x \<epsilon>)"
 
 named_theorems\<^marker>\<open>tag important\<close> analytic_intros "introduction rules for proving analyticity"
 
 lemma analytic_imp_holomorphic: "f analytic_on S \<Longrightarrow> f holomorphic_on S"
-  by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
-     (metis centre_in_ball field_differentiable_at_within)
+  unfolding analytic_on_def holomorphic_on_def
+  using centre_in_ball field_differentiable_at_within field_differentiable_within_open by blast
 
 lemma analytic_on_open: "open S \<Longrightarrow> f analytic_on S \<longleftrightarrow> f holomorphic_on S"
   by (meson analytic_imp_holomorphic analytic_on_def holomorphic_on_subset openE)
@@ -426,15 +394,12 @@
 lemma analytic_at_imp_isCont:
   assumes "f analytic_on {z}"
   shows   "isCont f z"
-  using assms by (meson analytic_on_imp_differentiable_at field_differentiable_imp_continuous_at insertI1)
+  by (meson analytic_on_imp_differentiable_at assms field_differentiable_imp_continuous_at insertCI)
 
 lemma analytic_at_neq_imp_eventually_neq:
   assumes "f analytic_on {x}" "f x \<noteq> c"
   shows   "eventually (\<lambda>y. f y \<noteq> c) (at x)"
-proof (intro tendsto_imp_eventually_ne)
-  show "f \<midarrow>x\<rightarrow> f x"
-    using assms by (simp add: analytic_at_imp_isCont isContD)
-qed (use assms in auto)
+  using analytic_at_imp_isCont assms isContD tendsto_imp_eventually_ne by blast
 
 lemma analytic_on_subset: "f analytic_on S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> f analytic_on T"
   by (auto simp: analytic_on_def)
@@ -455,18 +420,21 @@
   have "?lhs \<longleftrightarrow> (\<exists>T. open T \<and> S \<subseteq> T \<and> f analytic_on T)"
   proof safe
     assume "f analytic_on S"
-    then show "\<exists>T. open T \<and> S \<subseteq> T \<and> f analytic_on T"
-      apply (simp add: analytic_on_def)
-      apply (rule exI [where x="\<Union>{U. open U \<and> f analytic_on U}"], auto)
-      apply (metis open_ball analytic_on_open centre_in_ball)
-      by (metis analytic_on_def)
+    then have "\<forall>x \<in> \<Union>{U. open U \<and> f analytic_on U}. \<exists>\<epsilon>>0. f holomorphic_on ball x \<epsilon>"
+      using analytic_on_def by force
+    moreover have "S \<subseteq> \<Union>{U. open U \<and> f analytic_on U}"
+      using \<open>f analytic_on S\<close>
+      by (smt (verit, best) open_ball Union_iff analytic_on_def analytic_on_open centre_in_ball mem_Collect_eq subsetI)
+    ultimately show "\<exists>T. open T \<and> S \<subseteq> T \<and> f analytic_on T"
+      unfolding analytic_on_def
+      by (metis (mono_tags, lifting) mem_Collect_eq open_Union)
   next
     fix T
     assume "open T" "S \<subseteq> T" "f analytic_on T"
     then show "f analytic_on S"
         by (metis analytic_on_subset)
   qed
-  also have "... \<longleftrightarrow> ?rhs"
+  also have "\<dots> \<longleftrightarrow> ?rhs"
     by (auto simp: analytic_on_open)
   finally show ?thesis .
 qed
@@ -486,7 +454,7 @@
 lemma analytic_on_compose:
   assumes f: "f analytic_on S"
       and g: "g analytic_on (f ` S)"
-    shows "(g o f) analytic_on S"
+    shows "(g \<circ> f) analytic_on S"
 unfolding analytic_on_def
 proof (intro ballI)
   fix x
@@ -500,21 +468,19 @@
   with e' obtain d where d: "0 < d" and fd: "f ` ball x d \<subseteq> ball (f x) e'"
      by (auto simp: continuous_at_ball)
   have "g \<circ> f holomorphic_on ball x (min d e)"
-    apply (rule holomorphic_on_compose)
-    apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
-    by (metis fd gh holomorphic_on_subset image_mono min.cobounded1 subset_ball)
+    by (meson fd fh gh holomorphic_on_compose_gen holomorphic_on_subset image_mono min.cobounded1 min.cobounded2 subset_ball)
   then show "\<exists>e>0. g \<circ> f holomorphic_on ball x e"
     by (metis d e min_less_iff_conj)
 qed
 
 lemma analytic_on_compose_gen:
   "f analytic_on S \<Longrightarrow> g analytic_on T \<Longrightarrow> (\<And>z. z \<in> S \<Longrightarrow> f z \<in> T)
-             \<Longrightarrow> g o f analytic_on S"
-by (metis analytic_on_compose analytic_on_subset image_subset_iff)
+             \<Longrightarrow> g \<circ> f analytic_on S"
+  by (metis analytic_on_compose analytic_on_subset image_subset_iff)
 
 lemma analytic_on_neg [analytic_intros]:
   "f analytic_on S \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on S"
-by (metis analytic_on_holomorphic holomorphic_on_minus)
+  by (metis analytic_on_holomorphic holomorphic_on_minus)
 
 lemma analytic_on_add [analytic_intros]:
   assumes f: "f analytic_on S"
@@ -529,33 +495,11 @@
   obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
     by (metis analytic_on_def g z)
   have "(\<lambda>z. f z + g z) holomorphic_on ball z (min e e')"
-    apply (rule holomorphic_on_add)
-    apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
-    by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
+    by (metis fh gh holomorphic_on_add holomorphic_on_subset linorder_linear min_def subset_ball)
   then show "\<exists>e>0. (\<lambda>z. f z + g z) holomorphic_on ball z e"
     by (metis e e' min_less_iff_conj)
 qed
 
-lemma analytic_on_diff [analytic_intros]:
-  assumes f: "f analytic_on S"
-      and g: "g analytic_on S"
-    shows "(\<lambda>z. f z - g z) analytic_on S"
-unfolding analytic_on_def
-proof (intro ballI)
-  fix z
-  assume z: "z \<in> S"
-  then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f
-    by (metis analytic_on_def)
-  obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
-    by (metis analytic_on_def g z)
-  have "(\<lambda>z. f z - g z) holomorphic_on ball z (min e e')"
-    apply (rule holomorphic_on_diff)
-    apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
-    by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
-  then show "\<exists>e>0. (\<lambda>z. f z - g z) holomorphic_on ball z e"
-    by (metis e e' min_less_iff_conj)
-qed
-
 lemma analytic_on_mult [analytic_intros]:
   assumes f: "f analytic_on S"
       and g: "g analytic_on S"
@@ -569,13 +513,23 @@
   obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
     by (metis analytic_on_def g z)
   have "(\<lambda>z. f z * g z) holomorphic_on ball z (min e e')"
-    apply (rule holomorphic_on_mult)
-    apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
-    by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
+    by (metis fh gh holomorphic_on_mult holomorphic_on_subset min.absorb_iff2 min_def subset_ball)
   then show "\<exists>e>0. (\<lambda>z. f z * g z) holomorphic_on ball z e"
     by (metis e e' min_less_iff_conj)
 qed
 
+lemma analytic_on_diff [analytic_intros]:
+  assumes f: "f analytic_on S" and g: "g analytic_on S"
+  shows "(\<lambda>z. f z - g z) analytic_on S"
+proof -
+  have "(\<lambda>z. - g z) analytic_on S"
+    by (simp add: analytic_on_neg g)
+  then have "(\<lambda>z. f z + - g z) analytic_on S"
+    using analytic_on_add f by blast
+  then show ?thesis
+    by fastforce
+qed
+
 lemma analytic_on_inverse [analytic_intros]:
   assumes f: "f analytic_on S"
       and nz: "(\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0)"
@@ -591,24 +545,20 @@
   then obtain e' where e': "0 < e'" and nz': "\<And>y. dist z y < e' \<Longrightarrow> f y \<noteq> 0"
     by (metis open_ball centre_in_ball continuous_on_open_avoid e z nz)
   have "(\<lambda>z. inverse (f z)) holomorphic_on ball z (min e e')"
-    apply (rule holomorphic_on_inverse)
-    apply (metis fh holomorphic_on_subset min.cobounded2 min.commute subset_ball)
-    by (metis nz' mem_ball min_less_iff_conj)
+    using fh holomorphic_on_inverse holomorphic_on_open nz' by fastforce
   then show "\<exists>e>0. (\<lambda>z. inverse (f z)) holomorphic_on ball z e"
     by (metis e e' min_less_iff_conj)
 qed
 
 lemma analytic_on_divide [analytic_intros]:
-  assumes f: "f analytic_on S"
-      and g: "g analytic_on S"
-      and nz: "(\<And>z. z \<in> S \<Longrightarrow> g z \<noteq> 0)"
-    shows "(\<lambda>z. f z / g z) analytic_on S"
-unfolding divide_inverse
-by (metis analytic_on_inverse analytic_on_mult f g nz)
+  assumes f: "f analytic_on S" and g: "g analytic_on S"
+    and nz: "(\<And>z. z \<in> S \<Longrightarrow> g z \<noteq> 0)"
+  shows "(\<lambda>z. f z / g z) analytic_on S"
+  unfolding divide_inverse by (metis analytic_on_inverse analytic_on_mult f g nz)
 
 lemma analytic_on_power [analytic_intros]:
   "f analytic_on S \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on S"
-by (induct n) (auto simp: analytic_on_mult)
+  by (induct n) (auto simp: analytic_on_mult)
 
 lemma analytic_on_power_int [analytic_intros]:
   assumes nz: "n \<ge> 0 \<or> (\<forall>x\<in>A. f x \<noteq> 0)" and f: "f analytic_on A"
@@ -645,15 +595,15 @@
 proof -
   have "deriv f w * deriv g (f w) = deriv g (f w) * deriv f w"
     by (simp add: algebra_simps)
-  also have "... = deriv (g o f) w"
+  also have "\<dots> = deriv (g \<circ> f) w"
     using assms
     by (metis analytic_on_imp_differentiable_at analytic_on_open deriv_chain image_subset_iff)
-  also have "... = deriv id w"
+  also have "\<dots> = deriv id w"
   proof (rule complex_derivative_transform_within_open [where s=S])
     show "g \<circ> f holomorphic_on S"
       by (rule assms holomorphic_on_compose_gen holomorphic_intros)+
   qed (use assms in auto)
-  also have "... = 1"
+  also have "\<dots> = 1"
     by simp
   finally show ?thesis .
 qed
@@ -679,19 +629,16 @@
 
 lemma analytic_at_two:
   "f analytic_on {z} \<and> g analytic_on {z} \<longleftrightarrow>
-   (\<exists>s. open s \<and> z \<in> s \<and> f holomorphic_on s \<and> g holomorphic_on s)"
+   (\<exists>S. open S \<and> z \<in> S \<and> f holomorphic_on S \<and> g holomorphic_on S)"
   (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then obtain s t
-    where st: "open s" "z \<in> s" "f holomorphic_on s"
-              "open t" "z \<in> t" "g holomorphic_on t"
+  then obtain S T
+    where st: "open S" "z \<in> S" "f holomorphic_on S"
+              "open T" "z \<in> T" "g holomorphic_on T"
     by (auto simp: analytic_at)
-  show ?rhs
-    apply (rule_tac x="s \<inter> t" in exI)
-    using st
-    apply (auto simp: holomorphic_on_subset)
-    done
+  then show ?rhs
+    by (metis Int_iff holomorphic_on_subset inf_le1 inf_le2 open_Int)
 next
   assume ?rhs
   then show ?lhs
@@ -707,32 +654,23 @@
     and complex_derivative_mult_at: "deriv (\<lambda>w. f w * g w) z =
            f z * deriv g z + deriv f z * g z"
 proof -
-  obtain s where s: "open s" "z \<in> s" "f holomorphic_on s" "g holomorphic_on s"
-    using assms by (metis analytic_at_two)
   show "deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
-    apply (rule DERIV_imp_deriv [OF DERIV_add])
-    using s
-    apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
-    done
+    using analytic_on_imp_differentiable_at assms by auto
   show "deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
-    apply (rule DERIV_imp_deriv [OF DERIV_diff])
-    using s
-    apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
-    done
-  show "deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
-    apply (rule DERIV_imp_deriv [OF DERIV_mult'])
-    using s
-    apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
-    done
+    using analytic_on_imp_differentiable_at assms by force
+  obtain S where "open S" "z \<in> S" "f holomorphic_on S" "g holomorphic_on S"
+    using assms by (metis analytic_at_two)
+  then show "deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
+    by (simp add: DERIV_imp_deriv [OF DERIV_mult'] holomorphic_derivI)
 qed
 
 lemma deriv_cmult_at:
   "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. c * f w) z = c * deriv f z"
-by (auto simp: complex_derivative_mult_at)
+  by (auto simp: complex_derivative_mult_at)
 
 lemma deriv_cmult_right_at:
   "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. f w * c) z = deriv f z * c"
-by (auto simp: complex_derivative_mult_at)
+  by (auto simp: complex_derivative_mult_at)
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Complex differentiation of sequences and series\<close>
 
@@ -748,27 +686,16 @@
 proof -
   from assms obtain x l where x: "x \<in> S" and tf: "((\<lambda>n. f n x) \<longlongrightarrow> l) sequentially"
     by blast
-  { fix e::real assume e: "e > 0"
-    then obtain N where N: "\<forall>n\<ge>N. \<forall>x. x \<in> S \<longrightarrow> cmod (f' n x - g' x) \<le> e"
-      by (metis conv)
-    have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
-    proof (rule exI [of _ N], clarify)
-      fix n y h
-      assume "N \<le> n" "y \<in> S"
-      then have "cmod (f' n y - g' y) \<le> e"
-        by (metis N)
-      then have "cmod h * cmod (f' n y - g' y) \<le> cmod h * e"
-        by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2)
-      then show "cmod (f' n y * h - g' y * h) \<le> e * cmod h"
-        by (simp add: norm_mult [symmetric] field_simps)
-    qed
-  } note ** = this
   show ?thesis
     unfolding has_field_derivative_def
   proof (rule has_derivative_sequence [OF cvs _ _ x])
     show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
       by (rule tf)
-  next show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
+  next 
+    have **: "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> \<epsilon> * cmod h"
+      if "\<epsilon> > 0" for \<epsilon>::real 
+      by (metis that left_diff_distrib mult_right_mono norm_ge_zero norm_mult conv)
+    show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
       unfolding eventually_sequentially by (blast intro: **)
   qed (metis has_field_derivative_def df)
 qed
@@ -784,19 +711,17 @@
 proof -
   from assms obtain x l where x: "x \<in> S" and sf: "((\<lambda>n. f n x) sums l)"
     by blast
-  { fix e::real assume e: "e > 0"
+  { fix \<epsilon>::real assume e: "\<epsilon> > 0"
     then obtain N where N: "\<forall>n x. n \<ge> N \<longrightarrow> x \<in> S
-            \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e"
+            \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> \<epsilon>"
       by (metis conv)
-    have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
+    have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> \<epsilon> * cmod h"
     proof (rule exI [of _ N], clarify)
       fix n y h
       assume "N \<le> n" "y \<in> S"
-      then have "cmod ((\<Sum>i<n. f' i y) - g' y) \<le> e"
-        by (metis N)
-      then have "cmod h * cmod ((\<Sum>i<n. f' i y) - g' y) \<le> cmod h * e"
-        by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2)
-      then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> e * cmod h"
+      have "cmod h * cmod ((\<Sum>i<n. f' i y) - g' y) \<le> cmod h * \<epsilon>"
+        by (simp add: N \<open>N \<le> n\<close> \<open>y \<in> S\<close> mult_le_cancel_left)
+      then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> \<epsilon> * cmod h"
         by (simp add: norm_mult [symmetric] field_simps sum_distrib_left)
     qed
   } note ** = this
@@ -818,8 +743,8 @@
 
 lemma sum_Suc_reindex:
   fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
-    shows  "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}"
-by (induct n) auto
+  shows "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}"
+  by (induct n) auto
 
 lemma field_Taylor:
   assumes S: "convex S"
@@ -836,7 +761,7 @@
     assume "u \<in> closed_segment w z"
     then have "u \<in> S"
       by (metis wzs subsetD)
-    have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) +
+    have *: "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) +
                       f (Suc i) u * (z-u)^i / (fact i)) =
               f (Suc n) u * (z-u) ^ n / (fact n)"
     proof (induction n)
@@ -849,7 +774,7 @@
            f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / (fact (Suc n)) -
            f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / (fact (Suc n))"
         using Suc by simp
-      also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n))"
+      also have "\<dots> = f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n))"
       proof -
         have "(fact(Suc n)) *
              (f(Suc n) u *(z-u) ^ n / (fact n) +
@@ -859,29 +784,26 @@
             ((fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / (fact(Suc n))) -
             ((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))"
           by (simp add: algebra_simps del: fact_Suc)
-        also have "... = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) +
+        also have "\<dots> = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) +
                          (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
                          (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
           by (simp del: fact_Suc)
-        also have "... = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
+        also have "\<dots> = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
                          (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
                          (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
           by (simp only: fact_Suc of_nat_mult ac_simps) simp
-        also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
+        also have "\<dots> = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
           by (simp add: algebra_simps)
         finally show ?thesis
         by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact_Suc)
       qed
       finally show ?case .
     qed
-    then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i)))
+    have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i)))
                 has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n))
                (at u within S)"
-      apply (intro derivative_eq_intros)
-      apply (blast intro: assms \<open>u \<in> S\<close>)
-      apply (rule refl)+
-      apply (auto simp: field_simps)
-      done
+      unfolding * [symmetric]
+      by (rule derivative_eq_intros assms \<open>u \<in> S\<close> refl | auto simp: field_simps)+
   } note sum_deriv = this
   { fix u
     assume u: "u \<in> closed_segment w z"
@@ -889,9 +811,9 @@
       by (metis wzs subsetD)
     have "norm (f (Suc n) u) * norm (z - u) ^ n \<le> norm (f (Suc n) u) * norm (u - z) ^ n"
       by (metis norm_minus_commute order_refl)
-    also have "... \<le> norm (f (Suc n) u) * norm (z - w) ^ n"
+    also have "\<dots> \<le> norm (f (Suc n) u) * norm (z - w) ^ n"
       by (metis mult_left_mono norm_ge_zero power_mono segment_bound [OF u])
-    also have "... \<le> B * norm (z - w) ^ n"
+    also have "\<dots> \<le> B * norm (z - w) ^ n"
       by (metis norm_ge_zero zero_le_power mult_right_mono  B [OF us])
     finally have "norm (f (Suc n) u) * norm (z - u) ^ n \<le> B * norm (z - w) ^ n" .
   } note cmod_bound = this
@@ -903,14 +825,14 @@
                 \<le> norm ((\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)) -
                         (\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))"
     by (simp add: norm_minus_commute)
-  also have "... \<le> B * norm (z - w) ^ n / (fact n) * norm (w - z)"
-    apply (rule field_differentiable_bound
-      [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
-         and S = "closed_segment w z", OF convex_closed_segment])
-    apply (auto simp: DERIV_subset [OF sum_deriv wzs]
-                  norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
-    done
-  also have "...  \<le> B * norm (z - w) ^ Suc n / (fact n)"
+  also have "\<dots> \<le> B * norm (z - w) ^ n / (fact n) * norm (w - z)"
+  proof (rule field_differentiable_bound)
+    show "\<And>x. x \<in> closed_segment w z \<Longrightarrow>
+          ((\<lambda>\<xi>. \<Sum>i\<le>n. f i \<xi> * (z - \<xi>) ^ i / fact i) has_field_derivative f (Suc n) x * (z - x) ^ n / fact n)
+           (at x within closed_segment w z)"
+      using DERIV_subset sum_deriv wzs by blast
+  qed (auto simp: norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
+  also have "\<dots>  \<le> B * norm (z - w) ^ Suc n / (fact n)"
     by (simp add: algebra_simps norm_minus_commute)
   finally show ?thesis .
 qed
@@ -921,8 +843,7 @@
       and B: "\<And>x. x \<in> S \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
       and w: "w \<in> S"
       and z: "z \<in> S"
-    shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
-          \<le> B * cmod(z - w)^(Suc n) / fact n"
+    shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i))) \<le> B * cmod(z - w)^(Suc n) / fact n"
   using assms by (rule field_Taylor)
 
 
@@ -932,20 +853,22 @@
   assumes "\<And>u. u \<in> closed_segment w z \<Longrightarrow> (f has_field_derivative f'(u)) (at u)"
     shows "\<exists>u. u \<in> closed_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
 proof -
-  have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
-    by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
+  define \<phi> where "\<phi> \<equiv> \<lambda>t. (1 - t) *\<^sub>R w + t *\<^sub>R z"
+  have twz: "\<And>t. \<phi> t = w + t *\<^sub>R (z - w)"
+    by (simp add: \<phi>_def real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
   note assms[unfolded has_field_derivative_def, derivative_intros]
-  show ?thesis
-    apply (cut_tac mvt_simple
-                     [of 0 1 "Re o f o (\<lambda>t. (1 - t) *\<^sub>R w +  t *\<^sub>R z)"
-                      "\<lambda>u. Re o (\<lambda>h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\<lambda>t. t *\<^sub>R (z - w))"])
-    apply auto
-    apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
-    apply (auto simp: closed_segment_def twz) []
-    apply (intro derivative_eq_intros has_derivative_at_withinI, simp_all)
-    apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
-    apply (force simp: twz closed_segment_def)
-    done
+  have *: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk>
+        \<Longrightarrow> (Re \<circ> f \<circ> \<phi> has_derivative Re \<circ> (*) (f' (\<phi> x)) \<circ> (\<lambda>t. t *\<^sub>R (z - w)))
+            (at x within {0..1})"
+    unfolding \<phi>_def
+    by (intro derivative_eq_intros has_derivative_at_withinI) 
+       (auto simp: in_segment scaleR_right_diff_distrib)
+  obtain x where "0<x" "x<1" "(Re \<circ> f \<circ> \<phi>) 1 -
+       (Re \<circ> f \<circ> \<phi>) 0 = (Re \<circ> (*) (f' (\<phi> x)) \<circ> (\<lambda>t. t *\<^sub>R (z - w))) (1 - 0)"
+    using mvt_simple [OF zero_less_one *] by force
+  then show ?thesis
+    unfolding \<phi>_def
+    by (smt (verit) comp_apply in_segment(1) scaleR_left_distrib scaleR_one scaleR_zero_left)
 qed
 
 lemma complex_Taylor_mvt:
@@ -967,30 +890,27 @@
                  (f (Suc (Suc i)) u * ((z-u) ^ Suc i) - of_nat (Suc i) * (f (Suc i) u * (z-u) ^ i)) /
                  (fact (Suc i)))"
        by (subst sum_Suc_reindex) simp
-    also have "... = f (Suc 0) u -
+    also have "\<dots> = f (Suc 0) u -
              (f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
              (fact (Suc n)) +
              (\<Sum>i = 0..n.
                  f (Suc (Suc i)) u * ((z-u) ^ Suc i) / (fact (Suc i))  -
                  f (Suc i) u * (z-u) ^ i / (fact i))"
       by (simp only: diff_divide_distrib fact_cancel ac_simps)
-    also have "... = f (Suc 0) u -
+    also have "\<dots> = f (Suc 0) u -
              (f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) /
              (fact (Suc n)) +
              f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n)) - f (Suc 0) u"
       by (subst sum_Suc_diff) auto
-    also have "... = f (Suc n) u * (z-u) ^ n / (fact n)"
+    also have "\<dots> = f (Suc n) u * (z-u) ^ n / (fact n)"
       by (simp only: algebra_simps diff_divide_distrib fact_cancel)
-    finally have "(\<Sum>i = 0..n. (f (Suc i) u * (z - u) ^ i
+    finally have *: "(\<Sum>i = 0..n. (f (Suc i) u * (z - u) ^ i
                              - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / (fact i)) =
                   f (Suc n) u * (z - u) ^ n / (fact n)" .
-    then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / (fact i)) has_field_derivative
+    have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / (fact i)) has_field_derivative
                 f (Suc n) u * (z - u) ^ n / (fact n))  (at u)"
-      apply (intro derivative_eq_intros)+
-      apply (force intro: u assms)
-      apply (rule refl)+
-      apply (auto simp: ac_simps)
-      done
+      unfolding * [symmetric]
+      by (rule derivative_eq_intros assms u refl | auto simp: field_simps)+
   }
   then show ?thesis
     apply (cut_tac complex_mvt_line [of w z "\<lambda>u. \<Sum>i = 0..n. f i u * (z-u) ^ i / (fact i)"
diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -437,7 +437,7 @@
     then obtain L where L: "subspace L" "affine_parallel S L"
       using assms affine_parallel_subspace[of S] by auto
     then obtain a where a: "S = ((+) a ` L)"
-      using affine_parallel_def[of L S] affine_parallel_commut by auto
+      using affine_parallel_def[of L S] affine_parallel_commute by auto
     from L have "closed L" using closed_subspace by auto
     then have "closed S"
       using closed_translation a by auto
diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -1692,20 +1692,15 @@
     (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
 
 lemma seq_compactI:
-  assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+  assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
   shows "seq_compact S"
   unfolding seq_compact_def using assms by fast
 
 lemma seq_compactE:
   assumes "seq_compact S" "\<forall>n. f n \<in> S"
-  obtains l r where "l \<in> S" "strict_mono (r :: nat \<Rightarrow> nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
+  obtains l r where "l \<in> S" "strict_mono (r :: nat \<Rightarrow> nat)" "(f \<circ> r) \<longlonglongrightarrow> l"
   using assms unfolding seq_compact_def by fast
 
-lemma closed_sequentially: (* TODO: move upwards *)
-  assumes "closed S" and "\<And>n. f n \<in> S" and "f \<longlonglongrightarrow> l"
-  shows "l \<in> S"
-  by (metis Lim_in_closed_set assms eventually_sequentially trivial_limit_sequentially)
-
 lemma seq_compact_Int_closed:
   assumes "seq_compact S" and "closed T"
   shows "seq_compact (S \<inter> T)"
diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -1373,7 +1373,7 @@
       obtain a where "a \<in> interior (convex hull insert 0 B)"
       proof (rule interior_simplex_nonempty [OF indB])
         show "finite B"
-          by (simp add: indB independent_finite)
+          by (simp add: indB independent_imp_finite)
         show "card B = DIM('N)"
           by (simp add: cardB 2)
       qed
diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -8,9 +8,11 @@
 imports Binary_Product_Measure Function_Topology
 begin
 
-lemma PiE_choice: "(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
-  by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
-     (force intro: exI[of _ "restrict f I" for f])
+lemma Pi_choice: "(\<forall>i\<in>I. \<exists>x\<in>F i. P i x) \<longleftrightarrow> (\<exists>f\<in>Pi I F. \<forall>i\<in>I. P i (f i))"
+  by (metis Pi_iff)
+
+lemma PiE_choice: "(\<forall>i\<in>I. \<exists>x\<in>F i. P i x) \<longleftrightarrow>(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i))"
+  unfolding Pi_choice by (metis Int_iff PiE_def restrict_PiE restrict_apply)
 
 lemma case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
   by auto
@@ -97,7 +99,7 @@
     then show "x \<in> A \<longleftrightarrow> x \<in> B"
       using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S]
       by (auto simp del: PiE_cancel_merge simp add: Un_absorb1 eq)
-  qed (insert sets, auto)
+  qed (use sets in auto)
 qed
 
 lemma restrict_vimage:
@@ -178,7 +180,7 @@
 
 lemma Pi_cong_sets:
     "\<lbrakk>I = J; \<And>x. x \<in> I \<Longrightarrow> M x = N x\<rbrakk> \<Longrightarrow> Pi I M = Pi J N"
-  unfolding Pi_def by auto
+  by auto
 
 lemma PiM_cong:
   assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
@@ -327,17 +329,11 @@
     done
 qed
 proposition prod_algebra_cong:
-  assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
+  assumes "I = J" and "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
   shows "prod_algebra I M = prod_algebra J N"
-proof -
-  have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
-    using sets_eq_imp_space_eq[OF sets] by auto
-  with sets show ?thesis unfolding \<open>I = J\<close>
-    by (intro antisym prod_algebra_mono) auto
-qed
+  by (metis assms prod_algebra_mono sets_eq_imp_space_eq subsetI subset_antisym)
 
-lemma space_in_prod_algebra:
-  "(\<Pi>\<^sub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
+lemma space_in_prod_algebra: "(\<Pi>\<^sub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
 proof cases
   assume "I = {}" then show ?thesis
     by (auto simp add: prod_algebra_def image_iff prod_emb_def)
@@ -346,9 +342,8 @@
   then obtain i where "i \<in> I" by auto
   then have "(\<Pi>\<^sub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
     by (auto simp: prod_emb_def)
-  also have "\<dots> \<in> prod_algebra I M"
-    using \<open>i \<in> I\<close> by (intro prod_algebraI) auto
-  finally show ?thesis .
+  then show ?thesis
+    by (simp add: \<open>i \<in> I\<close> prod_algebraI) 
 qed
 
 lemma space_PiM: "space (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
@@ -383,8 +378,8 @@
   show "A \<in> sigma_sets ?\<Omega> ?R"
   proof cases
     assume "I = {}"
-    with X have "A = {\<lambda>x. undefined}" by (auto simp: prod_emb_def)
-    with \<open>I = {}\<close> show ?thesis by (auto intro!: sigma_sets_top)
+    with X show ?thesis
+      by (metis (no_types, lifting) PiE_cong R.top empty_iff prod_emb_PiE subset_eq)
   next
     assume "I \<noteq> {}"
     with X have "A = (\<Inter>j\<in>J. {f\<in>(\<Pi>\<^sub>E i\<in>I. space (M i)). f j \<in> X j})"
@@ -405,16 +400,25 @@
 qed
 
 lemma sets_PiM_eq_proj:
-  "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
-  apply (simp add: sets_PiM_single)
-  apply (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"])
-  apply auto []
-  apply auto []
-  apply simp
-  apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl])
-  apply (rule sets_vimage_algebra2)
-  apply (auto intro!: arg_cong2[where f=sigma_sets])
-  done
+  assumes "I \<noteq> {}"
+  shows "sets (PiM I M) = sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
+        (is "?lhs = ?rhs")
+proof -
+  have "?lhs = 
+        sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {{f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
+    by (simp add: sets_PiM_single)
+  also have "\<dots> = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
+                (\<Union>x\<in>I. sets (vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>xa. xa x) (M x)))"
+    apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl])
+     apply (rule sets_vimage_algebra2)
+    by (auto intro!: arg_cong2[where f=sigma_sets])
+  also have "... = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
+     (\<Union> (sets ` (\<lambda>i. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i)) ` I))"
+    by simp
+  also have "... = ?rhs"
+    by (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"]) (use assms in auto)
+  finally show ?thesis .
+qed
 
 lemma
   shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
@@ -616,7 +620,7 @@
     by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: if_split_asm)
   then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) \<in> sets (Pi\<^sub>M I M)"
     using \<open>A \<in> sets (M i)\<close> \<open>i \<in> I\<close> by (auto intro!: sets_PiM_I)
-qed (insert \<open>i \<in> I\<close>, auto simp: space_PiM)
+qed (use \<open>i \<in> I\<close> in \<open>auto simp: space_PiM\<close>)
 
 lemma measurable_component_singleton'[measurable_dest]:
   assumes f: "f \<in> measurable N (Pi\<^sub>M I M)"
@@ -696,7 +700,10 @@
     by auto
   then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N"
     using A X by (auto intro!: measurable_sets)
-qed (insert X, auto simp add: PiE_def dest: measurable_space)
+next
+  show "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
+    using X by (auto simp add: PiE_def dest: measurable_space)
+qed 
 
 lemma measurable_abs_UNIV:
   "(\<And>n. (\<lambda>\<omega>. f n \<omega>) \<in> measurable M (N n)) \<Longrightarrow> (\<lambda>\<omega> n. f n \<omega>) \<in> measurable M (PiM UNIV N)"
@@ -708,13 +715,7 @@
 lemma measurable_restrict_subset':
   assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)"
   shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
-proof-
-  from assms(1) have "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
-    by (rule measurable_restrict_subset)
-  also from assms(2) have "measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M) = measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
-    by (intro sets_PiM_cong measurable_cong_sets) simp_all
-  finally show ?thesis .
-qed
+  by (metis (no_types) assms measurable_cong_sets measurable_restrict_subset sets_PiM_cong)
 
 lemma measurable_prod_emb[intro, simp]:
   "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^sub>M L M)"
@@ -754,11 +755,7 @@
 
 lemma sets_in_extensional_aux:
   "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
-proof -
-  have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
-    by (auto simp add: extensional_def space_PiM)
-  then show ?thesis by simp
-qed
+  by (smt (verit) PiE_iff mem_Collect_eq sets.top space_PiM subsetI subset_antisym)
 
 lemma sets_in_extensional[measurable (raw)]:
   "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)"
@@ -772,7 +769,7 @@
   then have "Pi\<^sub>E I E = (\<Inter>i\<in>I. prod_emb I M {i} (Pi\<^sub>E {i} E))"
     using E[THEN sets.sets_into_space] by (auto simp: PiE_iff prod_emb_def fun_eq_iff)
   also have "\<dots> \<in> sets (PiM I M)"
-    using I \<open>I \<noteq> {}\<close> by (safe intro!: sets.countable_INT' measurable_prod_emb sets_PiM_I_finite E)
+    using I \<open>I \<noteq> {}\<close> by (simp add: E sets.countable_INT' sets_PiM_I subset_eq)
   finally show ?thesis .
 qed (simp add: sets_PiM_empty)
 
@@ -805,8 +802,9 @@
     and K: "\<And>i. K i = prod_emb I M (J i) (X i)"
     by (metis Union.IH)
   show ?case
-  proof (intro exI[of _ "\<Union>i. J i"] bexI[of _ "\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i)"] conjI)
-    show "(\<Union>i. J i) \<subseteq> I" "countable (\<Union>i. J i)" using J by auto
+  proof (intro exI bexI conjI)
+    show "(\<Union>i. J i) \<subseteq> I" "countable (\<Union>i. J i)" 
+      using J by auto
     with J show "\<Union>(K ` UNIV) = prod_emb I M (\<Union>i. J i) (\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i))"
       by (simp add: K[abs_def] SUP_upper)
   qed(auto intro: X)
@@ -1010,7 +1008,7 @@
     in_space: "\<And>j. space (M j) = \<Union>(F j)"
     using sigma_finite_countable by (metis subset_eq)
   moreover have "(\<Union>(Pi\<^sub>E I ` Pi\<^sub>E I F)) = space (Pi\<^sub>M I M)"
-    using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2])
+    using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD1])
   ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets (Pi\<^sub>M I M) \<and> \<Union>A = space (Pi\<^sub>M I M) \<and> (\<forall>a\<in>A. emeasure (Pi\<^sub>M I M) a \<noteq> \<infinity>)"
     by (intro exI[of _ "Pi\<^sub>E I ` Pi\<^sub>E I F"])
        (auto intro!: countable_PiE sets_PiM_I_finite
@@ -1042,26 +1040,26 @@
       (\<Prod>i\<in>I \<union> J. emeasure (M i) (A i))"
     by (subst emeasure_distr)
        (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint)
-qed (insert fin, simp_all)
+qed (use fin in simp_all)
 
 proposition (in product_sigma_finite) product_nn_integral_fold:
   assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
   and f[measurable]: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
-  shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
-    (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
+shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
+        (is "?lhs = ?rhs")
 proof -
   interpret I: finite_product_sigma_finite M I by standard fact
   interpret J: finite_product_sigma_finite M J by standard fact
   interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard
   have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
     using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
-  show ?thesis
-    apply (subst distr_merge[OF IJ, symmetric])
-    apply (subst nn_integral_distr[OF measurable_merge])
-    apply measurable []
-    apply (subst J.nn_integral_fst[symmetric, OF P_borel])
-    apply simp
-    done
+  have "?lhs = integral\<^sup>N (distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J)) f"
+    by (simp add: I.finite_index J.finite_index assms(1) distr_merge)
+  also have "... = \<integral>\<^sup>+ x. f (merge I J x) \<partial>(Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
+    by (simp add: nn_integral_distr)
+  also have "... = ?rhs"
+    using P.Fubini P.nn_integral_snd by force
+  finally show ?thesis .
 qed
 
 lemma (in product_sigma_finite) distr_singleton:
@@ -1082,10 +1080,7 @@
 proof -
   interpret I: finite_product_sigma_finite M "{i}" by standard simp
   from f show ?thesis
-    apply (subst distr_singleton[symmetric])
-    apply (subst nn_integral_distr[OF measurable_component_singleton])
-    apply simp_all
-    done
+    by (metis distr_singleton insert_iff measurable_component_singleton nn_integral_distr)
 qed
 
 proposition (in product_sigma_finite) product_nn_integral_insert:
@@ -1118,8 +1113,7 @@
   shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x(i := y)) \<partial>(Pi\<^sub>M I M)) \<partial>(M i))"
   apply (subst product_nn_integral_insert[OF assms])
   apply (rule pair_sigma_finite.Fubini')
-  apply intro_locales []
-  apply (rule sigma_finite[OF I(1)])
+  apply (simp add: local.sigma_finite pair_sigma_finite.intro sigma_finite_measures)
   apply measurable
   done
 
@@ -1139,11 +1133,8 @@
               measurable_comp[OF measurable_component_singleton, unfolded comp_def])
        auto
   then show ?case
-    apply (simp add: product_nn_integral_insert[OF insert(1,2)])
-    apply (simp add: insert(2-) * nn_integral_multc)
-    apply (subst nn_integral_cmult)
-    apply (auto simp add: insert(2-))
-    done
+    using product_nn_integral_insert[OF insert(1,2)]
+    by (simp add: insert(2-) * nn_integral_multc nn_integral_cmult)
 qed (simp add: space_PiM)
 
 proposition (in product_sigma_finite) product_nn_integral_pair:
@@ -1176,7 +1167,8 @@
 lemma (in product_sigma_finite)
   assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^sub>M (I \<union> J) M)"
   shows emeasure_fold_integral:
-    "emeasure (Pi\<^sub>M (I \<union> J) M) A = (\<integral>\<^sup>+x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M)) \<partial>Pi\<^sub>M I M)" (is ?I)
+    "emeasure (Pi\<^sub>M (I \<union> J) M) A = (\<integral>\<^sup>+x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M)) \<partial>Pi\<^sub>M I M)" 
+         (is "?lhs = ?rhs")
     and emeasure_fold_measurable:
     "(\<lambda>x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M))) \<in> borel_measurable (Pi\<^sub>M I M)" (is ?B)
 proof -
@@ -1185,13 +1177,14 @@
   interpret IJ: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
   have merge: "merge I J -` A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) \<in> sets (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
     by (intro measurable_sets[OF _ A] measurable_merge assms)
-
-  show ?I
-    apply (subst distr_merge[symmetric, OF IJ])
-    apply (subst emeasure_distr[OF measurable_merge A])
+  have "?lhs = emeasure (distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J)) A"
+    by (simp add: I.finite_index J.finite_index assms(1) distr_merge)
+  also have "... = emeasure (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (merge I J -` A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M))"
+    by (meson A emeasure_distr measurable_merge)
+  also have "... = ?rhs"
     apply (subst J.emeasure_pair_measure_alt[OF merge])
-    apply (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
-    done
+    by (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
+  finally show "?lhs = ?rhs" .
 
   show ?B
     using IJ.measurable_emeasure_Pair1[OF merge]
@@ -1201,7 +1194,6 @@
 lemma sets_Collect_single:
   "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^sub>M I M). x i \<in> A } \<in> sets (Pi\<^sub>M I M)"
   by simp
-
 lemma pair_measure_eq_distr_PiM:
   fixes M1 :: "'a measure" and M2 :: "'a measure"
   assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
@@ -1282,7 +1274,7 @@
         {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
 proof
   have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
-  proof (auto)
+  proof clarify
     fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
     then have *: "X i \<in> sets (M i)" for i by simp
     define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
@@ -1315,9 +1307,7 @@
   qed
   show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
     unfolding sets_PiM_single
-    apply (rule sigma_sets_mono')
-    apply (auto simp add: PiE_iff *)
-    done
+    by (intro sigma_sets_mono') (auto simp add: PiE_iff *)
 qed
 
 lemma sets_PiM_subset_borel:
@@ -1361,7 +1351,7 @@
     ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
   qed
   have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
-    apply (rule sets.sigma_sets_subset') using ** by auto
+    by (metis "**" mem_Collect_eq open_UNIV sets.sigma_sets_subset' subsetI)
   then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
     unfolding borel_def by auto
 qed (simp add: sets_PiM_subset_borel)
diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -30,9 +30,9 @@
   proof
     have "\<And>u. \<lbrakk>u \<in> S; norm u *\<^sub>R f (u /\<^sub>R norm u) \<notin> T\<rbrakk> \<Longrightarrow> u = 0"
       by (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF \<open>subspace T\<close>] fim image_subset_iff inf_le2 singletonD)
-    then have "g ` (S - {0}) \<subseteq> T"
+    then have "g \<in> (S - {0}) \<rightarrow> T"
       using g_def by blast
-    moreover have "g ` (S - {0}) \<subseteq> UNIV - {0}"
+    moreover have "g \<in> (S - {0}) \<rightarrow> UNIV - {0}"
     proof (clarsimp simp: g_def)
       fix y
       assume "y \<in> S" and f0: "f (y /\<^sub>R norm y) = 0"
@@ -159,30 +159,24 @@
   assumes ST: "subspace S" "subspace T" "dim S < dim T"
       and "S \<subseteq> T"
       and contf: "continuous_on (sphere 0 1 \<inter> S) f"
-      and fim: "f ` (sphere 0 1 \<inter> S) \<subseteq> sphere 0 1 \<inter> T"
+      and fim: "f \<in> (sphere 0 1 \<inter> S) \<rightarrow> sphere 0 1 \<inter> T"
     shows "\<exists>c. homotopic_with_canon (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)"
 proof -
   have [simp]: "\<And>x. \<lbrakk>norm x = 1; x \<in> S\<rbrakk> \<Longrightarrow> norm (f x) = 1"
-    using fim by (simp add: image_subset_iff)
+    using fim by auto
   have "compact (sphere 0 1 \<inter> S)"
     by (simp add: \<open>subspace S\<close> closed_subspace compact_Int_closed)
-  then obtain g where pfg: "polynomial_function g" and gim: "g ` (sphere 0 1 \<inter> S) \<subseteq> T"
+  then obtain g where pfg: "polynomial_function g" and gim: "g \<in> (sphere 0 1 \<inter> S) \<rightarrow> T"
                 and g12: "\<And>x. x \<in> sphere 0 1 \<inter> S \<Longrightarrow> norm(f x - g x) < 1/2"
-    using Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ \<open>subspace T\<close>, of "1/2"] fim by auto
+    using Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ \<open>subspace T\<close>, of "1/2"] fim
+    by (auto simp: image_subset_iff_funcset)
   have gnz: "g x \<noteq> 0" if "x \<in> sphere 0 1 \<inter> S" for x
-  proof -
-    have "norm (f x) = 1"
-      using fim that by (simp add: image_subset_iff)
-    then show ?thesis
-      using g12 [OF that] by auto
-  qed
+    using g12 that by fastforce
   have diffg: "g differentiable_on sphere 0 1 \<inter> S"
     by (metis pfg differentiable_on_polynomial_function)
   define h where "h \<equiv> \<lambda>x. inverse(norm(g x)) *\<^sub>R g x"
   have h: "x \<in> sphere 0 1 \<inter> S \<Longrightarrow> h x \<in> sphere 0 1 \<inter> T" for x
-    unfolding h_def
-    using gnz [of x]
-    by (auto simp: subspace_mul [OF \<open>subspace T\<close>] subsetD [OF gim])
+    unfolding h_def using \<open>subspace T\<close> gim gnz subspace_mul by fastforce
   have diffh: "h differentiable_on sphere 0 1 \<inter> S"
     unfolding h_def using gnz
     by (fastforce intro: derivative_intros diffg differentiable_on_compose [OF diffg])
@@ -205,7 +199,7 @@
       have "convex T"
         by (simp add: \<open>subspace T\<close> subspace_imp_convex)
       then have "convex hull {f x, g x} \<subseteq> T"
-        by (metis IntD2 closed_segment_subset fim gim image_subset_iff segment_convex_hull that)
+        by (metis IntD2 PiE closed_segment_subset fim gim segment_convex_hull that)
       then show ?thesis
         using that non0fg segment_convex_hull by fastforce
     qed
@@ -279,14 +273,9 @@
       then have affS_eq: "aff_dim S = aff_dim (ball 0 1 \<inter> T)"
         using \<open>aff_dim T = aff_dim S\<close> by simp
       have "rel_frontier S homeomorphic rel_frontier(ball 0 1 \<inter> T)"
-      proof (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>])
-        show "convex (ball 0 1 \<inter> T)"
-          by (simp add: \<open>subspace T\<close> convex_Int subspace_imp_convex)
-        show "bounded (ball 0 1 \<inter> T)"
-          by (simp add: bounded_Int)
-        show "aff_dim S = aff_dim (ball 0 1 \<inter> T)"
-          by (rule affS_eq)
-      qed
+        using homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>]
+        by (simp add: \<open>subspace T\<close> affS_eq assms bounded_Int convex_Int 
+            homeomorphic_rel_frontiers_convex_bounded_sets subspace_imp_convex)
       also have "... = frontier (ball 0 1) \<inter> T"
       proof (rule convex_affine_rel_frontier_Int [OF convex_ball])
         show "affine T"
@@ -318,10 +307,8 @@
   then show ?thesis
   proof (cases "T = {}")
     case True
-    then have "rel_frontier S = {}" "rel_frontier T = {}"
-      using fim by fastforce+
     then show ?thesis
-      using that by (simp add: homotopic_on_emptyI)
+      by (smt (verit, best) False affST aff_dim_negative_iff)
   next
     case False
     obtain T':: "'a set"
@@ -383,16 +370,16 @@
   assumes fin: "finite \<F>"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
       and "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>; S \<noteq> T\<rbrakk> \<Longrightarrow> S \<inter> T \<subseteq> K"
-      and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
-   shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g ` (\<Union>\<F>) \<subseteq> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)"
+      and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g \<in> S \<rightarrow> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
+   shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g \<in> (\<Union>\<F>) \<rightarrow> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)"
 using assms
 proof (induction \<F>)
   case empty show ?case by simp
 next
   case (insert S \<F>)
-  then obtain f where contf: "continuous_on (S) f" and fim: "f ` S \<subseteq> T" and feq: "\<forall>x \<in> S \<inter> K. f x = h x"
-    by (meson insertI1)
-  obtain g where contg: "continuous_on (\<Union>\<F>) g" and gim: "g ` \<Union>\<F> \<subseteq> T" and geq: "\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x"
+  then obtain f where contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> T" and feq: "\<forall>x \<in> S \<inter> K. f x = h x"
+    by (metis funcset_image insert_iff)
+  obtain g where contg: "continuous_on (\<Union>\<F>) g" and gim: "g \<in> (\<Union>\<F>) \<rightarrow> T" and geq: "\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x"
     using insert by auto
   have fg: "f x = g x" if "x \<in> T" "T \<in> \<F>" "x \<in> S" for x T
   proof -
@@ -403,38 +390,38 @@
   qed
   moreover have "continuous_on (S \<union> \<Union> \<F>) (\<lambda>x. if x \<in> S then f x else g x)"
     by (auto simp: insert closed_Union contf contg  intro: fg continuous_on_cases)
+  moreover have "S \<union> \<Union> \<F> = \<Union> (insert S \<F>)"
+    by auto
   ultimately show ?case
-    by (smt (verit, del_insts) Int_iff UnE complete_lattice_class.Sup_insert feq fim geq gim image_subset_iff)
+    by (smt (verit) Int_iff Pi_iff UnE feq fim geq gim)
 qed
 
 lemma extending_maps_Union:
   assumes fin: "finite \<F>"
-      and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
-      and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
-      and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; \<not> X \<subseteq> Y; \<not> Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
-    shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g ` (\<Union>\<F>) \<subseteq> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)"
-apply (simp flip: Union_maximal_sets [OF fin])
-apply (rule extending_maps_Union_aux)
-apply (simp_all add: Union_maximal_sets [OF fin] assms)
-by (metis K psubsetI)
-
+    and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g \<in> S \<rightarrow> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
+    and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
+    and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; \<not> X \<subseteq> Y; \<not> Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
+  shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g \<in> (\<Union>\<F>) \<rightarrow> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)"
+proof -
+  have "\<And>S T. \<lbrakk>S \<in> \<F>; \<forall>U\<in>\<F>. \<not> S \<subset> U; T \<in> \<F>; \<forall>U\<in>\<F>. \<not> T \<subset> U; S \<noteq> T\<rbrakk> \<Longrightarrow> S \<inter> T \<subseteq> K"
+    by (metis K psubsetI)
+  then show ?thesis
+    apply (simp flip: Union_maximal_sets [OF fin])
+    apply (rule extending_maps_Union_aux, simp_all add: Union_maximal_sets [OF fin] assms)
+    done
+qed
 
 lemma extend_map_lemma:
   assumes "finite \<F>" "\<G> \<subseteq> \<F>" "convex T" "bounded T"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X < aff_dim T"
       and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S"
-      and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
-  obtains g where "continuous_on (\<Union>\<F>) g" "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
+      and contf: "continuous_on (\<Union>\<G>) f" and fim: "f \<in> (\<Union>\<G>) \<rightarrow> rel_frontier T"
+  obtains g where "continuous_on (\<Union>\<F>) g" "g \<in> (\<Union>\<F>) \<rightarrow> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
 proof (cases "\<F> - \<G> = {}")
   case True
   show ?thesis
-  proof
-    show "continuous_on (\<Union> \<F>) f"
-      using True \<open>\<G> \<subseteq> \<F>\<close> contf by auto
-    show "f ` \<Union> \<F> \<subseteq> rel_frontier T"
-      using True fim by auto
-  qed auto
+    using True assms(2) contf fim that by force
 next
   case False
   then have "0 \<le> aff_dim T"
@@ -467,14 +454,14 @@
       using Suc.IH [OF ple] by auto
     let ?Faces = "{D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D \<le> p}"
     have extendh: "\<exists>g. continuous_on D g \<and>
-                       g ` D \<subseteq> rel_frontier T \<and>
+                       g \<in> D \<rightarrow> rel_frontier T \<and>
                        (\<forall>x \<in> D \<inter> \<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p}). g x = h x)"
       if D: "D \<in> \<G> \<union> ?Faces" for D
     proof (cases "D \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p})")
       case True
       have "continuous_on D h"
         using True conth continuous_on_subset by blast
-      moreover have "h ` D \<subseteq> rel_frontier T"
+      moreover have "h \<in> D \<rightarrow> rel_frontier T"
         using True him by blast
       ultimately show ?thesis
         by blast
@@ -574,7 +561,7 @@
      show ?thesis
        using that
         apply clarsimp
-        by (smt (verit, ccfv_SIG) IntI face_of_aff_dim_lt face_of_imp_convex [of X] face_of_imp_convex [of Y] face_of_trans ff)
+       by (smt (verit) IntI face_of_aff_dim_lt face_of_imp_convex face_of_trans ff inf_commute)
     qed
     obtain g where "continuous_on (\<Union>(\<G> \<union> ?Faces)) g"
                    "g ` \<Union>(\<G> \<union> ?Faces) \<subseteq> rel_frontier T"
@@ -589,23 +576,20 @@
     show "\<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int i}) \<subseteq> \<Union>\<F>"
       using \<open>\<G> \<subseteq> \<F>\<close> face_of_imp_subset by fastforce
     show "\<Union>\<F> \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < i})"
-    proof (rule Union_mono)
-      show "\<F> \<subseteq> \<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int i}"
-        using face by (fastforce simp: aff i)
-    qed
+        using face by (intro Union_mono) (fastforce simp: aff i)
   qed
   have "int i \<le> aff_dim T" by (simp add: i)
   then show ?thesis
-    using extendf [of i] unfolding eq by (metis that)
+    using extendf [of i] that unfolding eq by fastforce
 qed
 
 lemma extend_map_lemma_cofinite0:
   assumes "finite \<F>"
       and "pairwise (\<lambda>S T. S \<inter> T \<subseteq> K) \<F>"
-      and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g ` (S - {a}) \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
+      and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g \<in> (S - {a}) \<rightarrow> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
     shows "\<exists>C g. finite C \<and> disjnt C U \<and> card C \<le> card \<F> \<and>
-                 continuous_on (\<Union>\<F> - C) g \<and> g ` (\<Union>\<F> - C) \<subseteq> T
+                 continuous_on (\<Union>\<F> - C) g \<and> g \<in> (\<Union>\<F> - C) \<rightarrow> T
                   \<and> (\<forall>x \<in> (\<Union>\<F> - C) \<inter> K. g x = h x)"
   using assms
 proof induction
@@ -614,18 +598,18 @@
 next
   case (insert X \<F>)
   then have "closed X" and clo: "\<And>X. X \<in> \<F> \<Longrightarrow> closed X"
-        and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g ` (S - {a}) \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
+        and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g \<in> (S - {a}) \<rightarrow> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
         and pwX: "\<And>Y. Y \<in> \<F> \<and> Y \<noteq> X \<longrightarrow> X \<inter> Y \<subseteq> K \<and> Y \<inter> X \<subseteq> K"
         and pwF: "pairwise (\<lambda> S T. S \<inter> T \<subseteq> K) \<F>"
     by (simp_all add: pairwise_insert)
   obtain C g where C: "finite C" "disjnt C U" "card C \<le> card \<F>"
                and contg: "continuous_on (\<Union>\<F> - C) g"
-               and gim: "g ` (\<Union>\<F> - C) \<subseteq> T"
+               and gim: "g \<in> (\<Union>\<F> - C) \<rightarrow> T"
                and gh:  "\<And>x. x \<in> (\<Union>\<F> - C) \<inter> K \<Longrightarrow> g x = h x"
     using insert.IH [OF pwF \<F> clo] by auto
   obtain a f where "a \<notin> U"
                and contf: "continuous_on (X - {a}) f"
-               and fim: "f ` (X - {a}) \<subseteq> T"
+               and fim: "f \<in> (X - {a}) \<rightarrow> T"
                and fh: "(\<forall>x \<in> X \<inter> K. f x = h x)"
     using insert.prems by (meson insertI1)
   show ?case
@@ -652,19 +636,19 @@
       by (blast intro: continuous_on_subset)
     show "\<forall>x\<in>(\<Union>(insert X \<F>) - insert a C) \<inter> K. (if x \<in> X then f x else g x) = h x"
       using gh by (auto simp: fh)
-    show "(\<lambda>a. if a \<in> X then f a else g a) ` (\<Union>(insert X \<F>) - insert a C) \<subseteq> T"
-      using fim gim by auto force
+    show "(\<lambda>a. if a \<in> X then f a else g a) \<in> (\<Union>(insert X \<F>) - insert a C) \<rightarrow> T"
+      using fim gim Pi_iff by fastforce
   qed
 qed
 
 
 lemma extend_map_lemma_cofinite1:
 assumes "finite \<F>"
-    and \<F>: "\<And>X. X \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (X - {a}) g \<and> g ` (X - {a}) \<subseteq> T \<and> (\<forall>x \<in> X \<inter> K. g x = h x)"
+    and \<F>: "\<And>X. X \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (X - {a}) g \<and> g \<in> (X - {a}) \<rightarrow> T \<and> (\<forall>x \<in> X \<inter> K. g x = h x)"
     and clo: "\<And>X. X \<in> \<F> \<Longrightarrow> closed X"
     and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; \<not> X \<subseteq> Y; \<not> Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
   obtains C g where "finite C" "disjnt C U" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
-                    "g ` (\<Union>\<F> - C) \<subseteq> T"
+                    "g \<in> (\<Union>\<F> - C) \<rightarrow> T"
                     "\<And>x. x \<in> (\<Union>\<F> - C) \<inter> K \<Longrightarrow> g x = h x"
 proof -
   let ?\<F> = "{X \<in> \<F>. \<forall>Y\<in>\<F>. \<not> X \<subset> Y}"
@@ -678,7 +662,7 @@
     by (simp add: \<open>finite \<F>\<close> card_mono)
   moreover
   obtain C g where "finite C \<and> disjnt C U \<and> card C \<le> card ?\<F> \<and>
-                 continuous_on (\<Union>?\<F> - C) g \<and> g ` (\<Union>?\<F> - C) \<subseteq> T
+                 continuous_on (\<Union>?\<F> - C) g \<and> g \<in> (\<Union>?\<F> - C) \<rightarrow> T
                   \<and> (\<forall>x \<in> (\<Union>?\<F> - C) \<inter> K. g x = h x)"
     using extend_map_lemma_cofinite0 [OF fin pw, of U T h] by (fastforce intro!: clo \<F>)
   ultimately show ?thesis
@@ -689,12 +673,12 @@
 lemma extend_map_lemma_cofinite:
   assumes "finite \<F>" "\<G> \<subseteq> \<F>" and T: "convex T" "bounded T"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
-      and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
+      and contf: "continuous_on (\<Union>\<G>) f" and fim: "f \<in> (\<Union>\<G>) \<rightarrow> rel_frontier T"
       and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
       and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T"
   obtains C g where
      "finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
-     "g ` (\<Union> \<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
+     "g \<in> (\<Union> \<F> - C) \<rightarrow> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
 proof -
   define \<H> where "\<H> \<equiv> \<G> \<union> {D. \<exists>C \<in> \<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}"
   have "finite \<G>"
@@ -707,7 +691,7 @@
     by (metis face inf_commute)
   have *: "\<And>X Y. \<lbrakk>X \<in> \<H>; Y \<in> \<H>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
     by (simp add: \<H>_def) (smt (verit) \<open>\<G> \<subseteq> \<F>\<close> DiffE face' face_of_Int_subface in_mono inf.idem)
-  obtain h where conth: "continuous_on (\<Union>\<H>) h" and him: "h ` (\<Union>\<H>) \<subseteq> rel_frontier T"
+  obtain h where conth: "continuous_on (\<Union>\<H>) h" and him: "h \<in> (\<Union>\<H>) \<rightarrow> rel_frontier T"
              and hf: "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> h x = f x" 
   proof (rule extend_map_lemma [OF \<open>finite \<H>\<close> [unfolded \<H>_def] Un_upper1 T])
     show "\<And>X. \<lbrakk>X \<in> \<G> \<union> {D. \<exists>C\<in>\<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}\<rbrakk> \<Longrightarrow> polytope X"
@@ -720,11 +704,11 @@
   then obtain a where a: "a \<notin> \<Union>\<G>"
     by blast
   have \<F>: "\<exists>a g. a \<notin> \<Union>\<G> \<and> continuous_on (D - {a}) g \<and>
-                  g ` (D - {a}) \<subseteq> rel_frontier T \<and> (\<forall>x \<in> D \<inter> \<Union>\<H>. g x = h x)"
+                  g \<in> (D - {a}) \<rightarrow> rel_frontier T \<and> (\<forall>x \<in> D \<inter> \<Union>\<H>. g x = h x)"
        if "D \<in> \<F>" for D
   proof (cases "D \<subseteq> \<Union>\<H>")
     case True
-    then have "h ` (D - {a}) \<subseteq> rel_frontier T" "continuous_on (D - {a}) h"
+    then have "h \<in> (D - {a}) \<rightarrow> rel_frontier T" "continuous_on (D - {a}) h"
       using him by (blast intro!: \<open>a \<notin> \<Union>\<G>\<close> continuous_on_subset [OF conth])+
     then show ?thesis
       using a by blast
@@ -755,7 +739,7 @@
           by (simp add: rel_frontier_retract_of_punctured_affine_hull poly polytope_imp_bounded polytope_imp_convex that brelD)
         then obtain r where relfD: "rel_frontier D \<subseteq> affine hull D - {b}"
                         and contr: "continuous_on (affine hull D - {b}) r"
-                        and rim: "r ` (affine hull D - {b}) \<subseteq> rel_frontier D"
+                        and rim: "r \<in> (affine hull D - {b}) \<rightarrow> rel_frontier D"
                         and rid: "\<And>x. x \<in> rel_frontier D \<Longrightarrow> r x = x"
           by (auto simp: retract_of_def retraction_def)
         show ?thesis
@@ -774,7 +758,7 @@
           have "r ` (D - {b}) \<subseteq> r ` (affine hull D - {b})"
             by (simp add: Diff_mono hull_subset image_mono)
           also have "... \<subseteq> rel_frontier D"
-            by (rule rim)
+            using rim by auto
           also have "... \<subseteq> \<Union>{E. E face_of D \<and> aff_dim E < aff_dim T}"
             using affD
             by (force simp: rel_frontier_of_polyhedron [OF \<open>polyhedron D\<close>] facet_of_def)
@@ -788,7 +772,7 @@
             show "continuous_on (r ` (D - {b})) h"
               by (simp add: Diff_mono hull_subset continuous_on_subset [OF conth rsub])
           qed
-          show "(h \<circ> r) ` (D - {b}) \<subseteq> rel_frontier T"
+          show "(h \<circ> r) \<in> (D - {b}) \<rightarrow> rel_frontier T"
             using brelD him rsub by fastforce
           show "(h \<circ> r) x = h x" if x: "x \<in> D \<inter> \<Union>\<H>" for x
           proof -
@@ -825,7 +809,7 @@
   have clo: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
     by (simp add: poly polytope_imp_closed)
   obtain C g where "finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
-                   "g ` (\<Union>\<F> - C) \<subseteq> rel_frontier T"
+                   "g \<in> (\<Union>\<F> - C) \<rightarrow> rel_frontier T"
                and gh: "\<And>x. x \<in> (\<Union>\<F> - C) \<inter> \<Union>\<H> \<Longrightarrow> g x = h x"
   proof (rule extend_map_lemma_cofinite1 [OF \<open>finite \<F>\<close> \<F> clo])
     show "X \<inter> Y \<subseteq> \<Union>\<H>" if XY: "X \<in> \<F>" "Y \<in> \<F>" and "\<not> X \<subseteq> Y" "\<not> Y \<subseteq> X" for X Y
@@ -856,7 +840,7 @@
       and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
       and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> rel_frontier T"
   obtains g where "continuous_on (\<Union>\<F>) g"
-     "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+     "g \<in> (\<Union>\<F>) \<rightarrow> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
 proof -
   obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g \<in> V \<rightarrow> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
@@ -877,12 +861,12 @@
   proof (rule extend_map_lemma [of \<G> "\<G> \<inter> Pow V" T g])
     show "continuous_on (\<Union>(\<G> \<inter> Pow V)) g"
       by (metis Union_Int_subset Union_Pow_eq \<open>continuous_on V g\<close> continuous_on_subset le_inf_iff)
-  qed (use \<open>finite \<G>\<close> T polyG affG faceG gim in fastforce)+
+  qed (use \<open>finite \<G>\<close> T polyG affG faceG gim image_subset_iff_funcset in auto)
   show ?thesis
   proof
     show "continuous_on (\<Union>\<F>) h"
       using \<open>\<Union>\<G> = \<Union>\<F>\<close> conth by auto
-    show "h ` \<Union>\<F> \<subseteq> rel_frontier T"
+    show "h \<in> \<Union>\<F> \<rightarrow> rel_frontier T"
       using \<open>\<Union>\<G> = \<Union>\<F>\<close> him by auto
     show "h x = f x" if "x \<in> S" for x
     proof -
@@ -910,7 +894,7 @@
       and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
       and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> rel_frontier T"
   obtains C g where "finite C" "disjnt C S" "continuous_on (\<Union>\<F> - C) g"
-     "g ` (\<Union>\<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+     "g \<in> (\<Union>\<F> - C) \<rightarrow> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
 proof -
   obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g \<in> V \<rightarrow> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
@@ -926,15 +910,15 @@
     by (rule cell_complex_subdivision_exists [OF \<open>d>0\<close> \<open>finite \<F>\<close> poly aff face]) auto
   obtain C h where "finite C" and dis: "disjnt C (\<Union>(\<G> \<inter> Pow V))"
                and card: "card C \<le> card \<G>" and conth: "continuous_on (\<Union>\<G> - C) h"
-               and him: "h ` (\<Union>\<G> - C) \<subseteq> rel_frontier T"
+               and him: "h \<in> (\<Union>\<G> - C) \<rightarrow> rel_frontier T"
                and hg: "\<And>x. x \<in> \<Union>(\<G> \<inter> Pow V) \<Longrightarrow> h x = g x"
   proof (rule extend_map_lemma_cofinite [of \<G> "\<G> \<inter> Pow V" T g])
     show "continuous_on (\<Union>(\<G> \<inter> Pow V)) g"
       by (metis Union_Int_subset Union_Pow_eq \<open>continuous_on V g\<close> continuous_on_subset le_inf_iff)
-    show "g ` \<Union>(\<G> \<inter> Pow V) \<subseteq> rel_frontier T"
+    show "g \<in> \<Union>(\<G> \<inter> Pow V) \<rightarrow> rel_frontier T"
       using gim by force
   qed (auto intro: \<open>finite \<G>\<close> T polyG affG dest: faceG)
-  have Ssub: "S \<subseteq> \<Union>(\<G> \<inter> Pow V)"
+  have "S \<subseteq> \<Union>(\<G> \<inter> Pow V)"
   proof
     fix x
     assume "x \<in> S"
@@ -948,23 +932,8 @@
     then show "x \<in> \<Union>(\<G> \<inter> Pow V)"
       using \<open>X \<in> \<G>\<close> \<open>x \<in> X\<close> by blast
   qed
-  show ?thesis
-  proof
-    show "continuous_on (\<Union>\<F>-C) h"
-      using \<open>\<Union>\<G> = \<Union>\<F>\<close> conth by auto
-    show "h ` (\<Union>\<F> - C) \<subseteq> rel_frontier T"
-      using \<open>\<Union>\<G> = \<Union>\<F>\<close> him by auto
-    show "h x = f x" if "x \<in> S" for x
-    proof -
-      have "h x = g x"
-        using Ssub hg that by blast
-      also have "... = f x"
-        by (simp add: gf that)
-      finally show "h x = f x" .
-    qed
-    show "disjnt C S"
-      using dis Ssub  by (meson disjnt_iff subset_eq)
-  qed (intro \<open>finite C\<close>)
+  then show ?thesis
+    by (metis PowI Union_Pow_eq \<open>\<Union> \<G> = \<Union> \<F>\<close> \<open>finite C\<close> conth dis disjnt_Union2 gf hg him subsetD that)
 qed
 
 
@@ -1021,7 +990,7 @@
       by (metis aff aff_dim_subset inf_commute inf_le1 order_trans)
     obtain K g where K: "finite K" "disjnt K S"
                  and contg: "continuous_on (\<Union>{bbox \<inter> T} - K) g"
-                 and gim: "g ` (\<Union>{bbox \<inter> T} - K) \<subseteq> rel_frontier U"
+                 and gim: "g \<in> (\<Union>{bbox \<inter> T} - K) \<rightarrow> rel_frontier U"
                  and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     proof (rule extend_map_cell_complex_to_sphere_cofinite
               [OF _ Ssub _ \<open>convex U\<close> \<open>bounded U\<close> _ _ _ contf fim])
@@ -1090,7 +1059,7 @@
       have "(g \<circ> closest_point (cbox (- c) c \<inter> T)) ` (T - K) \<subseteq> g ` (\<Union>{bbox \<inter> T} - K)"
         by (metis image_comp image_mono cpt_subset)
       also have "... \<subseteq> rel_frontier U"
-        by (rule gim)
+        using gim by blast
       finally show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) \<in> (T - K) \<rightarrow> rel_frontier U"
         by blast
       show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) x = f x" if "x \<in> S" for x
@@ -1112,7 +1081,7 @@
               order_trans [OF \<open>S \<subseteq> T\<close> hull_subset [of T affine]])
   then obtain K g where "finite K" "disjnt K S"
                and contg: "continuous_on (T - K) g"
-               and gim:  "g ` (T - K) \<subseteq> rel_frontier U"
+               and gim:  "g \<in> (T - K) \<rightarrow> rel_frontier U"
                and gf:   "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     by (rule_tac K=K and g=g in that) (auto simp: hull_inc elim: continuous_on_subset)
   then show ?thesis
@@ -1195,7 +1164,7 @@
     ultimately have "frontier (cball a d) \<inter> U retract_of (U - {a})"
       by metis
     then obtain r where contr: "continuous_on (U - {a}) r"
-                    and rim: "r ` (U - {a}) \<subseteq> sphere a d"  "r ` (U - {a}) \<subseteq> U"
+                    and rim: "r \<in> (U - {a}) \<rightarrow> sphere a d"  "r \<in> (U - {a}) \<rightarrow> U"
                     and req: "\<And>x. x \<in> sphere a d \<inter> U \<Longrightarrow> r x = x"
       using \<open>affine U\<close> by (force simp: retract_of_def retraction_def hull_same)
     define j where "j \<equiv> \<lambda>x. if x \<in> ball a d then r x else x"
@@ -1212,8 +1181,7 @@
         using rim by auto
       then show "j y \<in> S \<union> C - ball a d"
         unfolding j_def
-        using \<open>r y \<in> sphere a d\<close> \<open>y \<in> U - {a}\<close> \<open>y \<in> S \<union> (C - {a})\<close> d rim
-        by (metis Diff_iff Int_iff Un_iff subsetD cball_diff_eq_sphere image_subset_iff)
+        using \<open>y \<in> S \<union> (C - {a})\<close> \<open>y \<in> U - {a}\<close> d rim(2) by auto
     qed
     have contj: "continuous_on (U - {a}) j"
       unfolding j_def Uaeq
@@ -1437,7 +1405,7 @@
                and gim: "g \<in> (T - K) \<rightarrow> rel_frontier U"
                and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
      using assms extend_map_affine_to_sphere_cofinite_simple by metis
-  have "(\<exists>y C. C \<in> components (T - S) \<and> x \<in> C \<and> y \<in> C \<and> y \<in> L)" if "x \<in> K" for x
+  have "\<exists>y C. C \<in> components (T - S) \<and> x \<in> C \<and> y \<in> C \<and> y \<in> L" if "x \<in> K" for x
   proof -
     have "x \<in> T-S"
       using \<open>K \<subseteq> T\<close> \<open>disjnt K S\<close> disjnt_def that by fastforce
@@ -1446,7 +1414,7 @@
     with ovlap [of C] show ?thesis
       by blast
   qed
-  then obtain \<xi> where \<xi>: "\<And>x. x \<in> K \<Longrightarrow> \<exists>C. C \<in> components (T - S) \<and> x \<in> C \<and> \<xi> x \<in> C \<and> \<xi> x \<in> L"
+  then obtain \<xi> where \<xi>: "\<And>x. x \<in> K \<Longrightarrow> \<exists>C. C \<in> components (T - S) \<and> x \<in> C \<and> \<xi> x \<in> C \<and> \<xi> x \<in> L" 
     by metis
   obtain h where conth: "continuous_on (T - \<xi> ` K) h"
              and him: "h \<in> (T - \<xi> ` K) \<rightarrow> rel_frontier U"
@@ -1525,7 +1493,7 @@
   define LU where "LU \<equiv> L \<union> (\<Union> {C \<in> components (T - S). \<not>bounded C} - cbox (-(b+One)) (b+One))"
   obtain K g where "finite K" "K \<subseteq> LU" "K \<subseteq> T" "disjnt K S"
                and contg: "continuous_on (T - K) g"
-               and gim: "g ` (T - K) \<subseteq> rel_frontier U"
+               and gim: "g \<in> (T - K) \<rightarrow> rel_frontier U"
                and gf:  "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   proof (rule extend_map_affine_to_sphere2 [OF SUT aff contf fim])
     show "C \<inter> LU \<noteq> {}" if "C \<in> components (T - S)" for C
@@ -1577,7 +1545,7 @@
     proof (cases "x \<in> cbox (- c) c")
       case True
       with \<open>x \<in> T\<close> show ?thesis
-        using cbsub(3) Knot  by (force simp: closest_point_self)
+        using cbsub(3) Knot by (force simp: closest_point_self)
     next
       case False
       have clo_in_rf: "closest_point (cbox (- c) c \<inter> T) x \<in> rel_frontier (cbox (- c) c \<inter> T)"
@@ -1617,7 +1585,7 @@
       by (intro continuous_on_compose continuous_on_closest_point continuous_on_subset [OF contg]; force)
     have "g (closest_point (cbox (- c) c \<inter> T) x) \<in> rel_frontier U"
          if "x \<in> T" "x \<in> K \<longrightarrow> x \<notin> cbox (- b - One) (b + One)" for x
-      using gim [THEN subsetD] that cloTK by blast
+      using cloTK gim that by auto
     then show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) \<in> (T - K \<inter> cbox (- (b + One)) (b + One))
                \<rightarrow> rel_frontier U"
       by force
@@ -1663,8 +1631,7 @@
       and "\<And>C. \<lbrakk>C \<in> components(- S); bounded C\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
   obtains K g where "finite K" "K \<subseteq> L" "disjnt K S" "continuous_on (- K) g"
                     "g \<in> (- K) \<rightarrow> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-  using extend_map_affine_to_sphere_cofinite
-        [OF \<open>compact S\<close> affine_UNIV subset_UNIV] assms
+  using assms extend_map_affine_to_sphere_cofinite [OF \<open>compact S\<close> affine_UNIV subset_UNIV] 
   by (metis Compl_eq_Diff_UNIV aff_dim_UNIV of_nat_le_iff)
 
 corollary extend_map_UNIV_to_sphere_no_bounded_component:
@@ -1789,14 +1756,7 @@
     by auto
   moreover
   have "connected (- S) = connected (- sphere a r)"
-  proof (rule homotopy_eqv_separation)
-    show "S homotopy_eqv sphere a r"
-      using hom homeomorphic_imp_homotopy_eqv by blast
-    show "compact (sphere a r)"
-      by simp
-    then show " compact S"
-      using hom homeomorphic_compactness by blast
-  qed
+    by (meson hom compact_sphere homeomorphic_compactness homeomorphic_imp_homotopy_eqv homotopy_eqv_separation)
   ultimately show ?thesis
     using connected_Int_frontier [of "- sphere a r" "ball a r"] by (auto simp: \<open>0 < r\<close>)
 qed
@@ -1831,7 +1791,7 @@
       using S by (auto simp: homeomorphic_def)
     show "connected (- T)" if "closed T" "T \<subset> S" for T
     proof -
-      have "f ` T \<subseteq> sphere a r"
+      have "f \<in> T \<rightarrow> sphere a r"
         using \<open>T \<subset> S\<close> hom homeomorphism_image1 by blast
       moreover have "f ` T \<noteq> sphere a r"
         using \<open>T \<subset> S\<close> hom
@@ -1844,7 +1804,7 @@
       moreover then have "compact (f ` T)"
         by (meson compact_continuous_image continuous_on_subset hom homeomorphism_def psubsetE \<open>T \<subset> S\<close>)
       moreover have "T homotopy_eqv f ` T"
-        by (meson \<open>f ` T \<subseteq> sphere a r\<close> dual_order.strict_implies_order hom homeomorphic_def homeomorphic_imp_homotopy_eqv homeomorphism_of_subsets \<open>T \<subset> S\<close>)
+        by (meson hom homeomorphic_def homeomorphic_imp_homotopy_eqv homeomorphism_of_subsets order.refl psubsetE that(2))
       ultimately show ?thesis
         using homotopy_eqv_separation [of T "f`T"] by blast
     qed
@@ -1986,7 +1946,7 @@
 
 lemma inv_of_domain_ss0:
   fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
-  assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
+  assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f \<in> U \<rightarrow> S"
       and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)"
       and ope: "openin (top_of_set S) U"
     shows "openin (top_of_set S) (f ` U)"
@@ -2019,19 +1979,20 @@
     show "open (k ` U)"
       by (simp add: ope_iff homeomorphism_imp_open_map [OF homkh ope])
     show "inj_on (k \<circ> f \<circ> h) (k ` U)"
-      by (smt (verit) comp_apply inj_on_def \<open>U \<subseteq> S\<close> fim homeomorphism_apply2 homhk image_iff injf subsetD)
+      unfolding inj_on_def 
+      by (smt (verit, ccfv_threshold) PiE \<open>U \<subseteq> S\<close> assms(3) comp_apply homeomorphism_def homhk imageE inj_on_def injf subset_eq)
   qed
   moreover
   have eq: "f ` U = h ` (k \<circ> f \<circ> h \<circ> k) ` U"
     unfolding image_comp [symmetric] using \<open>U \<subseteq> S\<close> fim
-    by (metis homeomorphism_image2 homeomorphism_of_subsets homkh subset_image_iff)
+    by (metis homeomorphism_image2 homeomorphism_of_subsets homhk homkh image_subset_iff_funcset top_greatest)
   ultimately show ?thesis
     by (metis (no_types, opaque_lifting) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
 qed
 
 lemma inv_of_domain_ss1:
   fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
-  assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
+  assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f \<in> U \<rightarrow> S"
       and "subspace S"
       and ope: "openin (top_of_set S) U"
     shows "openin (top_of_set S) (f ` U)"
@@ -2045,7 +2006,7 @@
     show "continuous_on (U \<times> S') g"
       unfolding  g_def
       by (auto intro!: continuous_intros continuous_on_compose2 [OF contf continuous_on_fst])
-    show "g ` (U \<times> S') \<subseteq> S \<times> S'"
+    show "g \<in> (U \<times> S') \<rightarrow> S \<times> S'"
       using fim  by (auto simp: g_def)
     show "inj_on g (U \<times> S')"
       using injf by (auto simp: g_def inj_on_def)
@@ -2073,7 +2034,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes ope: "openin (top_of_set U) S"
       and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
-      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+      and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> V"
       and injf: "inj_on f S"
     shows "openin (top_of_set V) (f ` S)"
 proof -
@@ -2087,7 +2048,7 @@
   have eq: "f ` S = k ` (h \<circ> f) ` S"
   proof -
     have "k ` h ` f ` S = f ` S"
-      by (meson fim homeomorphism_def homeomorphism_of_subsets homhk subset_refl)
+      by (meson equalityD2 fim funcset_image homeomorphism_image2 homeomorphism_of_subsets homhk)
     then show ?thesis
       by (simp add: image_comp)
   qed
@@ -2101,11 +2062,11 @@
     moreover have "openin (top_of_set U) ((h \<circ> f) ` S)"
     proof (rule inv_of_domain_ss1)
       show "continuous_on S (h \<circ> f)"
-        by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
+        by (meson contf continuous_on_compose continuous_on_subset fim funcset_image homeomorphism_cont2 homkh)
       show "inj_on (h \<circ> f) S"
-        by (smt (verit, ccfv_SIG) comp_apply fim inj_on_def homeomorphism_apply2 [OF homkh] image_subset_iff injf)
-      show "(h \<circ> f) ` S \<subseteq> U"
-        using \<open>V' \<subseteq> U\<close> hfV' by auto
+        by (smt (verit, ccfv_SIG) Pi_iff comp_apply fim homeomorphism_apply2 homkh inj_on_def injf)
+      show "h \<circ> f \<in> S \<rightarrow> U"
+        using \<open>V' \<subseteq> U\<close> hfV' by blast
       qed (auto simp: assms)
     ultimately show "openin (top_of_set V') ((h \<circ> f) ` S)"
       using openin_subset_trans \<open>V' \<subseteq> U\<close> by force
@@ -2116,7 +2077,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes ope: "openin (top_of_set U) S"
       and "subspace U" "subspace V"
-      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+      and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> V"
       and injf: "inj_on f S" and "S \<noteq> {}"
     shows "dim U \<le> dim V"
 proof -
@@ -2130,11 +2091,12 @@
     then obtain h k where homhk: "homeomorphism V T h k"
       using homeomorphic_def  by blast
     have "continuous_on S (h \<circ> f)"
-      by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
+      by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_def homhk image_subset_iff_funcset)
     moreover have "(h \<circ> f) ` S \<subseteq> U"
       using \<open>T \<subseteq> U\<close> fim homeomorphism_image1 homhk by fastforce
     moreover have "inj_on (h \<circ> f) S"
-      by (smt (verit, best) comp_apply inj_on_def fim homeomorphism_apply1 homhk image_subset_iff injf)
+      unfolding inj_on_def
+      by (metis Pi_iff comp_apply fim homeomorphism_def homhk inj_on_def injf)
     ultimately have ope_hf: "openin (top_of_set U) ((h \<circ> f) ` S)"
       using invariance_of_domain_subspaces [OF ope \<open>subspace U\<close> \<open>subspace U\<close>] by blast
     have "(h \<circ> f) ` S \<subseteq> T"
@@ -2155,7 +2117,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes ope: "openin (top_of_set U) S"
       and aff: "affine U" "affine V" "aff_dim V \<le> aff_dim U"
-      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+      and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> V"
       and injf: "inj_on f S"
     shows "openin (top_of_set V) (f ` S)"
 proof (cases "S = {}")
@@ -2177,7 +2139,7 @@
       by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
     show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
       by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
-    show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
+    show "(+) (- b) \<circ> f \<circ> (+) a \<in> (+) (- a) ` S \<rightarrow> (+) (- b) ` V"
       using fim by auto
     show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
       by (auto simp: inj_on_def) (meson inj_onD injf)
@@ -2190,7 +2152,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes ope: "openin (top_of_set U) S"
       and aff: "affine U" "affine V"
-      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+      and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> V"
       and injf: "inj_on f S" and "S \<noteq> {}"
     shows "aff_dim U \<le> aff_dim V"
 proof -
@@ -2206,7 +2168,7 @@
       by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace_subtract \<open>affine V\<close> cong: image_cong_simp)
     show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
       by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
-    show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
+    show "(+) (- b) \<circ> f \<circ> (+) a \<in> (+) (- a) ` S \<rightarrow> (+) (- b) ` V"
       using fim by auto
     show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
       by (auto simp: inj_on_def) (meson inj_onD injf)
@@ -2227,7 +2189,7 @@
 corollary continuous_injective_image_subspace_dim_le:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "subspace S" "subspace T"
-      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
+      and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> T"
       and injf: "inj_on f S"
     shows "dim S \<le> dim T"
   using invariance_of_dimension_subspaces [of S S _ f] assms by (auto simp: subspace_affine)
@@ -2235,7 +2197,7 @@
 lemma invariance_of_dimension_convex_domain:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "convex S"
-      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> affine hull T"
+      and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> affine hull T"
       and injf: "inj_on f S"
     shows "aff_dim S \<le> aff_dim T"
 proof (cases "S = {}")
@@ -2249,7 +2211,7 @@
       by (simp add: openin_rel_interior)
     show "continuous_on (rel_interior S) f"
       using contf continuous_on_subset rel_interior_subset by blast
-    show "f ` rel_interior S \<subseteq> affine hull T"
+    show "f \<in> rel_interior S \<rightarrow> affine hull T"
       using fim rel_interior_subset by blast
     show "inj_on f (rel_interior S)"
       using inj_on_subset injf rel_interior_subset by blast
@@ -2271,8 +2233,8 @@
   proof (rule invariance_of_dimension_convex_domain [OF \<open>convex S\<close>])
     show "continuous_on S h"
       using homeomorphism_def homhk by blast
-    show "h ` S \<subseteq> affine hull T"
-      by (metis homeomorphism_def homhk hull_subset)
+    show "h \<in> S \<rightarrow> affine hull T"
+      using homeomorphism_image1 homhk hull_subset by fastforce
     show "inj_on h S"
       by (meson homeomorphism_apply1 homhk inj_on_inverseI)
   qed
@@ -2342,13 +2304,13 @@
 lemma continuous_image_subset_interior:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
-  shows "f ` (interior S) \<subseteq> interior(f ` S)"
+  shows "f \<in> (interior S) \<rightarrow> interior(f ` S)"
 proof -
   have "open (f ` interior S)"
     using assms
     by (intro invariance_of_domain_gen) (auto simp: subset_inj_on interior_subset continuous_on_subset)
   then show ?thesis
-    by (simp add: image_mono interior_maximal interior_subset)
+    by (simp add: image_mono interiorI interior_subset)
 qed
 
 lemma homeomorphic_interiors_same_dimension:
@@ -2363,9 +2325,9 @@
      and contf: "continuous_on S f" and contg: "continuous_on T g"
   then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
     by (auto simp: inj_on_def intro: rev_image_eqI) metis+
-  have fim: "f ` interior S \<subseteq> interior T"
+  have fim: "f \<in> interior S \<rightarrow> interior T"
     using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
-  have gim: "g ` interior T \<subseteq> interior S"
+  have gim: "g \<in> interior T \<rightarrow> interior S"
     using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
   show "homeomorphism (interior S) (interior T) f g"
     unfolding homeomorphism_def
@@ -2437,16 +2399,14 @@
      and contf: "continuous_on S f" and contg: "continuous_on T g"
   then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
     by (auto simp: inj_on_def intro: rev_image_eqI) metis+
-  have "g ` interior T \<subseteq> interior S"
+  have "g \<in> interior T \<rightarrow> interior S"
     using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
   then have fim: "f ` frontier S \<subseteq> frontier T"
-    unfolding frontier_def
-    using continuous_image_subset_interior assms(2) assms(3) S by auto
-  have "f ` interior S \<subseteq> interior T"
+    unfolding frontier_def using Pi_mem S assms by fastforce
+  have "f \<in> interior S \<rightarrow> interior T"
     using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
   then have gim: "g ` frontier T \<subseteq> frontier S"
-    unfolding frontier_def
-    using continuous_image_subset_interior T assms(2) assms(3) by auto
+    unfolding frontier_def using Pi_mem T assms by fastforce
   show "homeomorphism (frontier S) (frontier T) f g"
     unfolding homeomorphism_def
   proof (intro conjI ballI)
@@ -2500,9 +2460,10 @@
 
 lemma continuous_image_subset_rel_interior:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f \<in> S \<rightarrow> T"
       and TS: "aff_dim T \<le> aff_dim S"
-  shows "f ` (rel_interior S) \<subseteq> rel_interior(f ` S)"
+    shows "f \<in> (rel_interior S) \<rightarrow> rel_interior(f ` S)"
+unfolding image_subset_iff_funcset [symmetric]
 proof (rule rel_interior_maximal)
   show "f ` rel_interior S \<subseteq> f ` S"
     by(simp add: image_mono rel_interior_subset)
@@ -2511,9 +2472,9 @@
     show "openin (top_of_set (affine hull S)) (rel_interior S)"
       by (simp add: openin_rel_interior)
     show "aff_dim (affine hull f ` S) \<le> aff_dim (affine hull S)"
-      by (metis aff_dim_affine_hull aff_dim_subset fim TS order_trans)
-    show "f ` rel_interior S \<subseteq> affine hull f ` S"
-      by (meson \<open>f ` rel_interior S \<subseteq> f ` S\<close> hull_subset order_trans)
+      by (metis TS aff_dim_affine_hull aff_dim_subset fim image_subset_iff_funcset order_trans)
+    show "f \<in> rel_interior S \<rightarrow> affine hull f ` S"
+      using \<open>f ` rel_interior S \<subseteq> f ` S\<close> hull_subset by fastforce
     show "continuous_on (rel_interior S) f"
       using contf continuous_on_subset rel_interior_subset by blast
     show "inj_on f (rel_interior S)"
@@ -2533,10 +2494,10 @@
      and contf: "continuous_on S f" and contg: "continuous_on T g"
   then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
     by (auto simp: inj_on_def intro: rev_image_eqI) metis+
-  have fim: "f ` rel_interior S \<subseteq> rel_interior T"
-    by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
-  have gim: "g ` rel_interior T \<subseteq> rel_interior S"
-    by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
+  have fim: "f \<in> rel_interior S \<rightarrow> rel_interior T"
+    by (smt (verit, best) PiE Pi_I S \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST)
+  have gim: "g \<in> rel_interior T \<rightarrow> rel_interior S"
+    by (metis T \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior dual_order.refl funcsetI gTS)
   show "homeomorphism (rel_interior S) (rel_interior T) f g"
     unfolding homeomorphism_def
   proof (intro conjI ballI)
@@ -2553,7 +2514,7 @@
         by (metis fg \<open>x \<in> rel_interior T\<close> imageI)
     qed
     moreover have "f ` rel_interior S \<subseteq> rel_interior T"
-      by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
+      using fim by blast
     ultimately show "f ` rel_interior S = rel_interior T"
       by blast
     show "continuous_on (rel_interior S) f"
@@ -2587,8 +2548,8 @@
   proof (rule invariance_of_dimension_affine_sets)
     show "continuous_on (rel_interior S) f"
       using contf continuous_on_subset rel_interior_subset by blast
-    show "f ` rel_interior S \<subseteq> affine hull T"
-      by (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
+    show "f \<in> rel_interior S \<rightarrow> affine hull T"
+      by (simp add: S hull_inc mem_rel_interior_ball)
     show "inj_on f (rel_interior S)"
       by (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
   qed (simp_all add: openin_rel_interior assms)
@@ -2625,10 +2586,10 @@
      and contf: "continuous_on S f" and contg: "continuous_on T g"
   then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
     by (auto simp: inj_on_def intro: rev_image_eqI) metis+
-  have fim: "f ` rel_interior S \<subseteq> rel_interior T"
-    by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
-  have gim: "g ` rel_interior T \<subseteq> rel_interior S"
-    by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
+  have fim: "f \<in> rel_interior S \<rightarrow> rel_interior T"
+    by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior dual_order.refl fST image_subset_iff_funcset)
+  have gim: "g \<in> rel_interior T \<rightarrow> rel_interior S"
+    by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior dual_order.refl gTS image_subset_iff_funcset)
   show "homeomorphism (S - rel_interior S) (T - rel_interior T) f g"
     unfolding homeomorphism_def
   proof (intro conjI ballI)
@@ -2637,11 +2598,11 @@
     show fg: "\<And>y. y \<in> T - rel_interior T \<Longrightarrow> f (g y) = y"
       using T mem_rel_interior_ball by blast
     show "f ` (S - rel_interior S) = T - rel_interior T"
-      using S fST fim gim by auto
+      using S fST fim gim image_subset_iff_funcset by fastforce
     show "continuous_on (S - rel_interior S) f"
       using contf continuous_on_subset rel_interior_subset by blast
     show "g ` (T - rel_interior T) = S - rel_interior S"
-      using T gTS gim fim by auto
+      using T gTS gim fim image_subset_iff_funcset by fastforce
     show "continuous_on (T - rel_interior T) g"
       using contg continuous_on_subset rel_interior_subset by blast
   qed
@@ -2744,7 +2705,7 @@
                           (q \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))"
 proof -
   obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
-             and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
+             and him: "h \<in> ({0..1} \<times> {0..1}) \<rightarrow> S"
              and h0: "(\<forall>x. h (0, x) = p x)"
              and h1: "(\<forall>x. h (1, x) = q x)"
              and h01: "(\<forall>t\<in>{0..1}. h (t, 1) = h (t, 0)) "
@@ -2795,13 +2756,13 @@
 lemma simply_connected_eq_homotopic_circlemaps1:
   fixes f :: "complex \<Rightarrow> 'a::topological_space" and g :: "complex \<Rightarrow> 'a"
   assumes S: "simply_connected S"
-      and contf: "continuous_on (sphere 0 1) f" and fim: "f ` (sphere 0 1) \<subseteq> S"
-      and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
+      and contf: "continuous_on (sphere 0 1) f" and fim: "f \<in> (sphere 0 1) \<rightarrow> S"
+      and contg: "continuous_on (sphere 0 1) g" and gim: "g \<in> (sphere 0 1) \<rightarrow> S"
     shows "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
 proof -
   let ?h = "(\<lambda>t. complex_of_real (2 * pi * t) * \<i>)"
   have "homotopic_loops S (f \<circ> exp \<circ> ?h) (f \<circ> exp \<circ> ?h) \<and> homotopic_loops S (g \<circ> exp \<circ> ?h) (g \<circ> exp \<circ> ?h)"
-    by (simp add: homotopic_circlemaps_imp_homotopic_loops contf fim contg gim)
+    by (simp add: homotopic_circlemaps_imp_homotopic_loops contf fim contg gim image_subset_iff_funcset)
   then have "homotopic_loops S (f \<circ> exp \<circ> ?h) (g \<circ> exp \<circ> ?h)"
     using S simply_connected_homotopic_loops by blast
   then show ?thesis
@@ -2812,19 +2773,19 @@
 
 lemma simply_connected_eq_homotopic_circlemaps2a:
   fixes h :: "complex \<Rightarrow> 'a::topological_space"
-  assumes conth: "continuous_on (sphere 0 1) h" and him: "h ` (sphere 0 1) \<subseteq> S"
+  assumes conth: "continuous_on (sphere 0 1) h" and him: "h \<in> sphere 0 1 \<rightarrow> S"
       and hom: "\<And>f g::complex \<Rightarrow> 'a.
-                \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
-                continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
+                \<lbrakk>continuous_on (sphere 0 1) f; f \<in> (sphere 0 1) \<rightarrow> S;
+                continuous_on (sphere 0 1) g; g \<in> (sphere 0 1) \<rightarrow> S\<rbrakk>
                 \<Longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
             shows "\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
-  by (metis conth continuous_on_const him hom image_subset_iff)
+  by (metis conth continuous_on_const him hom image_subset_iff image_subset_iff_funcset)
 
 lemma simply_connected_eq_homotopic_circlemaps2b:
   fixes S :: "'a::real_normed_vector set"
   assumes "\<And>f g::complex \<Rightarrow> 'a.
-                \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
-                continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
+                \<lbrakk>continuous_on (sphere 0 1) f; f \<in> (sphere 0 1) \<rightarrow> S;
+                continuous_on (sphere 0 1) g; g \<in> (sphere 0 1) \<rightarrow> S\<rbrakk>
                 \<Longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
   shows "path_connected S"
 proof (clarsimp simp add: path_connected_eq_homotopic_points)
@@ -2869,10 +2830,10 @@
   fixes S :: "'a::real_normed_vector set"
   shows "simply_connected S \<longleftrightarrow>
          (\<forall>f g::complex \<Rightarrow> 'a.
-              continuous_on (sphere 0 1) f \<and> f ` (sphere 0 1) \<subseteq> S \<and>
-              continuous_on (sphere 0 1) g \<and> g ` (sphere 0 1) \<subseteq> S
+              continuous_on (sphere 0 1) f \<and> f \<in> (sphere 0 1) \<rightarrow> S \<and>
+              continuous_on (sphere 0 1) g \<and> g \<in> (sphere 0 1) \<rightarrow> S
               \<longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g)"
-  by (metis simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a 
+  by (metis image_subset_iff_funcset simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a
       simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3)
 
 proposition simply_connected_eq_contractible_circlemap:
@@ -2882,7 +2843,7 @@
          (\<forall>f::complex \<Rightarrow> 'a.
               continuous_on (sphere 0 1) f \<and> f `(sphere 0 1) \<subseteq> S
               \<longrightarrow> (\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)))"
-  by (metis simply_connected_eq_homotopic_circlemaps simply_connected_eq_homotopic_circlemaps2a 
+  by (metis image_subset_iff_funcset simply_connected_eq_homotopic_circlemaps simply_connected_eq_homotopic_circlemaps2a 
       simply_connected_eq_homotopic_circlemaps3 simply_connected_imp_path_connected)
 
 corollary homotopy_eqv_simple_connectedness:
@@ -2966,12 +2927,7 @@
   then obtain f g where hom: "homeomorphism S T f g"
     using homeomorphic_def by blast
   show "dim S = dim T"
-  proof (rule order_antisym)
-    show "dim S \<le> dim T"
-      by (metis assms dual_order.refl inj_onI homeomorphism_cont1 [OF hom] homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] continuous_injective_image_subspace_dim_le)
-    show "dim T \<le> dim S"
-      by (metis assms dual_order.refl inj_onI homeomorphism_cont2 [OF hom] homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] continuous_injective_image_subspace_dim_le)
-  qed
+    by (metis \<open>S homeomorphic T\<close> aff_dim_subspace assms homeomorphic_convex_sets of_nat_eq_iff subspace_imp_convex)
 next
   assume "dim S = dim T"
   then show "S homeomorphic T"
@@ -3034,11 +2990,11 @@
   qed
 qed
 
-subsection\<open>more invariance of domain\<close>(*FIX ME title? *)
+subsection\<open>more invariance of domain\<close>  (*FIX ME title? *)
 
 proposition invariance_of_domain_sphere_affine_set_gen:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f \<in> S \<rightarrow> T"
       and U: "bounded U" "convex U"
       and "affine T" and affTU: "aff_dim T < aff_dim U"
       and ope: "openin (top_of_set (rel_frontier U)) S"
@@ -3085,8 +3041,8 @@
     qed (use contf continuous_on_subset hgsub in blast)
     show "inj_on (f \<circ> h) (g ` (S - {b}))"
       by (smt (verit, del_insts) SU homeomorphism_def inj_on_def injf gh Diff_iff comp_apply imageE subset_iff)
-    show "(f \<circ> h) ` g ` (S - {b}) \<subseteq> T"
-      by (metis fim image_comp image_mono hgsub subset_trans)
+    show "f \<circ> h \<in> g ` (S - {b}) \<rightarrow> T"
+      using fim hgsub by fastforce
   qed (auto simp: assms)
   moreover
   have "openin (top_of_set T) ((f \<circ> k) ` j ` (S - {c}))"
@@ -3100,20 +3056,15 @@
     qed (use contf continuous_on_subset kjsub in blast)
     show "inj_on (f \<circ> k) (j ` (S - {c}))"
       by (smt (verit, del_insts) SU homeomorphism_def inj_on_def injf jk Diff_iff comp_apply imageE subset_iff)
-    show "(f \<circ> k) ` j ` (S - {c}) \<subseteq> T"
-      by (metis fim image_comp image_mono kjsub subset_trans)
+    show "f \<circ> k \<in> j ` (S - {c}) \<rightarrow> T"
+      using fim kjsub by fastforce
   qed (auto simp: assms)
   ultimately have "openin (top_of_set T) ((f \<circ> h) ` g ` (S - {b}) \<union> ((f \<circ> k) ` j ` (S - {c})))"
     by (rule openin_Un)
   moreover have "(f \<circ> h) ` g ` (S - {b}) = f ` (S - {b})"
   proof -
     have "h ` g ` (S - {b}) = (S - {b})"
-    proof
-      show "h ` g ` (S - {b}) \<subseteq> S - {b}"
-        using homeomorphism_apply1 [OF gh] SU by (fastforce simp add: image_iff image_subset_iff)
-      show "S - {b} \<subseteq> h ` g ` (S - {b})"
-        by (metis Diff_mono SU gh homeomorphism_image2 homeomorphism_of_subsets set_eq_subset)
-    qed
+      by (meson Diff_mono Diff_subset SU gh homeomorphism_def homeomorphism_of_subsets subset_singleton_iff)
     then show ?thesis
       by (metis image_comp)
   qed
@@ -3134,7 +3085,7 @@
 
 lemma invariance_of_domain_sphere_affine_set:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f \<in> S \<rightarrow> T"
       and "r \<noteq> 0" "affine T" and affTU: "aff_dim T < DIM('a)"
       and ope: "openin (top_of_set (sphere a r)) S"
    shows "openin (top_of_set T) (f ` S)"
@@ -3166,9 +3117,10 @@
     then have "\<not> open (f ` sphere a r)"
       using compact_open
       by (metis assms(3) image_is_empty not_less_iff_gr_or_eq sphere_eq_empty)
-    then show False
-      using invariance_of_domain_sphere_affine_set [OF contf injf subset_UNIV] \<open>r > 0\<close>
-      by (metis aff_dim_UNIV affine_UNIV less_irrefl of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that)
+    then have "r=0"
+      by (metis Pi_I UNIV_I aff_dim_UNIV affine_UNIV contf injf invariance_of_domain_sphere_affine_set
+               of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that)
+    with \<open>r>0\<close> show False by auto
   qed
   then show ?thesis
     using not_less by blast
@@ -3712,10 +3664,10 @@
   assume L: ?lhs
   then obtain g where contg: "continuous_on S g" and g: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
     using inessential_imp_continuous_logarithm_circle by blast
-  have "f ` S \<subseteq> sphere 0 1"
-    by (metis L homotopic_with_imp_subset1)
+  have "f \<in> S \<rightarrow> sphere 0 1"
+    by (metis L image_subset_iff_funcset homotopic_with_imp_subset1)
   then have "\<And>x. x \<in> S \<Longrightarrow> Re (g x) = 0"
-    using g by auto
+    using g by (simp add: Pi_iff)
   then show ?rhs
     by (rule_tac x="Im \<circ> g" in exI) (auto simp: Euler g intro: contg continuous_intros)
 next
@@ -3747,7 +3699,7 @@
     shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x * h x) (\<lambda>x. g x * h x)"
 proof -
   obtain k where contk: "continuous_on ({0..1::real} \<times> S) k"
-             and kim: "k ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
+             and kim: "k \<in> ({0..1} \<times> S) \<rightarrow> sphere 0 1"
              and k0:  "\<And>x. k(0, x) = f x"
              and k1: "\<And>x. k(1, x) = g x"
     using hom by (auto simp: homotopic_with_def)
@@ -3760,8 +3712,8 @@
 proposition homotopic_circlemaps_divide:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
     shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
-           continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
-           continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
+           continuous_on S f \<and> f \<in> S \<rightarrow> sphere 0 1 \<and>
+           continuous_on S g \<and> g \<in> S \<rightarrow> sphere 0 1 \<and>
            (\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c))"
 proof -
   have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
@@ -3780,8 +3732,8 @@
                 homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
     by auto
   have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
-           continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
-           continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
+           continuous_on S f \<and> f \<in> S \<rightarrow> sphere 0 1 \<and>
+           continuous_on S g \<and> g \<in> S \<rightarrow> sphere 0 1 \<and>
            homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
         (is "?lhs \<longleftrightarrow> ?rhs")
   proof
@@ -3802,7 +3754,7 @@
       using homotopic_with_eq [OF homotopic_with_sphere_times [OF L cont]]
       by (auto simp: divide_inverse norm_inverse)
     with L show ?rhs
-      by (simp add: homotopic_with_imp_continuous homotopic_with_imp_subset1 homotopic_with_imp_subset2)
+      by (simp add: homotopic_with_imp_continuous homotopic_with_imp_funspace1)
   next
     assume ?rhs then show ?lhs
       by (elim conjE homotopic_with_eq [OF homotopic_with_sphere_times]; force)
@@ -3882,7 +3834,7 @@
 qed
 
 lemma open_map_iff_lower_hemicontinuous_preimage:
-  assumes "f ` S \<subseteq> T"
+  assumes "f \<in> S \<rightarrow> T"
     shows "((\<forall>U. openin (top_of_set S) U
                  \<longrightarrow> openin (top_of_set T) (f ` U)) \<longleftrightarrow>
             (\<forall>U. closedin (top_of_set S) U
@@ -3913,7 +3865,7 @@
 qed
 
 lemma closed_map_iff_upper_hemicontinuous_preimage:
-  assumes "f ` S \<subseteq> T"
+  assumes "f \<in> S \<rightarrow> T"
     shows "((\<forall>U. closedin (top_of_set S) U
                  \<longrightarrow> closedin (top_of_set T) (f ` U)) \<longleftrightarrow>
             (\<forall>U. openin (top_of_set S) U
@@ -4519,11 +4471,11 @@
   assume contf: "continuous_on (S \<union> T) f" and 0: "\<forall>i\<in>S \<union> T. f i \<noteq> 0"
   then have contfS: "continuous_on S f" and contfT: "continuous_on T f"
     using continuous_on_subset by auto
-  have "\<lbrakk>continuous_on S f; f ` S \<subseteq> -{0}\<rbrakk> \<Longrightarrow> \<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))"
+  have "\<lbrakk>continuous_on S f; f \<in> S \<rightarrow> -{0}\<rbrakk> \<Longrightarrow> \<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))"
     using BS by (auto simp: Borsukian_continuous_logarithm)
   then obtain g where contg: "continuous_on S g" and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
     using "0" contfS by force
-  have "\<lbrakk>continuous_on T f; f ` T \<subseteq> -{0}\<rbrakk> \<Longrightarrow> \<exists>g. continuous_on T g \<and> (\<forall>x \<in> T. f x = exp(g x))"
+  have "\<lbrakk>continuous_on T f; f \<in> T \<rightarrow> -{0}\<rbrakk> \<Longrightarrow> \<exists>g. continuous_on T g \<and> (\<forall>x \<in> T. f x = exp(g x))"
     using BT by (auto simp: Borsukian_continuous_logarithm)
   then obtain h where conth: "continuous_on T h" and fh: "\<And>x. x \<in> T \<Longrightarrow> f x = exp(h x)"
     using "0" contfT by force
@@ -4718,12 +4670,12 @@
     proof (rule upper_lower_hemicontinuous_explicit [of T "\<lambda>y. {z \<in> S. f z = y}" S])
       show "\<And>U. openin (top_of_set S) U
                  \<Longrightarrow> openin (top_of_set T) {x \<in> T. {z \<in> S. f z = x} \<subseteq> U}"
-        using closed_map_iff_upper_hemicontinuous_preimage [OF fim [THEN equalityD1]]
-        by (simp add: Abstract_Topology_2.continuous_imp_closed_map \<open>compact S\<close> contf fim)
+        using closed_map_iff_upper_hemicontinuous_preimage [of f S T] fim contf \<open>compact S\<close>
+        using Abstract_Topology_2.continuous_imp_closed_map by blast
       show "\<And>U. closedin (top_of_set S) U \<Longrightarrow>
                  closedin (top_of_set T) {x \<in> T. {z \<in> S. f z = x} \<subseteq> U}"
-        using ope open_map_iff_lower_hemicontinuous_preimage [OF fim [THEN equalityD1]]
-        by meson
+        using ope open_map_iff_lower_hemicontinuous_preimage[of f S T] fim [THEN equalityD1]
+        by blast
       show "bounded {z \<in> S. f z = y}"
         by (metis (no_types, lifting) compact_imp_bounded [OF \<open>compact S\<close>] bounded_subset mem_Collect_eq subsetI)
     qed (use \<open>y \<in> T\<close> \<open>0 < d\<close> fk kTS in \<open>force+\<close>)
@@ -4918,7 +4870,7 @@
     assume "connected U" "connected V" and T: "T = U \<union> V"
       and cloU: "closedin (top_of_set T) U"
       and cloV: "closedin (top_of_set T) V"
-    have "f ` (g ` U \<inter> g ` V) \<subseteq> U" "f ` (g ` U \<inter> g ` V) \<subseteq> V"
+    have "f \<in> (g ` U \<inter> g ` V) \<rightarrow> U" "f \<in> (g ` U \<inter> g ` V) \<rightarrow> V"
       using gf fim T by auto (metis UnCI image_iff)+
     moreover have "U \<inter> V \<subseteq> f ` (g ` U \<inter> g ` V)"
       using gf fim by (force simp: image_iff T)
@@ -5393,14 +5345,8 @@
 lemma nonseparation_by_component_eq:
   fixes S :: "'a :: euclidean_space set"
   assumes "open S \<or> closed S"
-  shows "((\<forall>C \<in> components S. connected(-C)) \<longleftrightarrow> connected(- S))" (is "?lhs = ?rhs")
-proof
-  assume ?lhs with assms show ?rhs
-    by (meson separation_by_component_closed separation_by_component_open)
-next
-  assume ?rhs with assms show ?lhs
-    using component_complement_connected by force
-qed
+  shows "((\<forall>C \<in> components S. connected(-C)) \<longleftrightarrow> connected(- S))" 
+  by (metis assms component_complement_connected double_complement separation_by_component_closed separation_by_component_open)
 
 
 text\<open>Another interesting equivalent of an inessential mapping into C-{0}\<close>
@@ -5421,7 +5367,7 @@
     case False
     have anr: "ANR (-{0::complex})"
       by (simp add: ANR_delete open_Compl open_imp_ANR)
-    obtain g where contg: "continuous_on UNIV g" and gim: "g ` UNIV \<subseteq> -{0}"
+    obtain g where contg: "continuous_on UNIV g" and gim: "g \<in> UNIV \<rightarrow> -{0}"
                    and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     proof (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ homotopic_with_symD [OF a]])
       show "closedin (top_of_set UNIV) S"
@@ -5456,13 +5402,7 @@
         by (auto intro: continuous_on_subset [OF contj] simp flip: homeomorphism_image2 [OF hk])
     qed
     show "f x = exp ((j \<circ> k) x)" if "x \<in> S" for x
-    proof -
-      have "f x = (g \<circ> h) (k x)"
-        by (simp add: gf that)
-      also have "... = exp (j (k x))"
-        by (metis rangeI homeomorphism_image2 [OF hk] j)
-      finally show ?thesis by simp
-    qed
+      by (metis UNIV_I comp_apply gf hk homeomorphism_def image_eqI j that)
   qed
   then show ?lhs
     by (simp add: inessential_eq_continuous_logarithm)
@@ -5487,7 +5427,7 @@
     and ope: "openin (top_of_set (\<Union>\<F>)) C"
     and "homotopic_with_canon (\<lambda>x. True) C T f (\<lambda>x. a)"
     using assms by blast
-  with \<open>C \<noteq> {}\<close> have "f ` C \<subseteq> T" "a \<in> T"
+  with \<open>C \<noteq> {}\<close> have "f \<in> C \<rightarrow> T" "a \<in> T"
     using homotopic_with_imp_subset1 homotopic_with_imp_subset2 by blast+
   have "homotopic_with_canon (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
   proof (rule homotopic_on_clopen_Union)
@@ -5514,15 +5454,9 @@
 
 proposition Janiszewski_dual:
   fixes S :: "complex set"
-  assumes
-   "compact S" "compact T" "connected S" "connected T" "connected(- (S \<union> T))"
+  assumes "compact S" "compact T" "connected S" "connected T" "connected(- (S \<union> T))"
  shows "connected(S \<inter> T)"
-proof -
-  have ST: "compact (S \<union> T)"
-    by (simp add: assms compact_Un)
-  with Borsukian_imp_unicoherent [of "S \<union> T"] ST assms
-  show ?thesis
-    by (simp add: Borsukian_separation_compact closed_subset compact_imp_closed unicoherentD)
-qed
+  by (meson Borsukian_imp_unicoherent Borsukian_separation_compact assms closed_subset compact_Un 
+      compact_imp_closed sup_ge1 sup_ge2 unicoherentD)
 
 end
diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -2950,11 +2950,11 @@
   obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
              and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
              and "independent B" "finite B" "card B = dim S" "span B = S"
-    by (metis orthonormal_basis_subspace [OF S] independent_finite)
+    by (metis orthonormal_basis_subspace [OF S] independent_imp_finite)
   obtain C where "C \<subseteq> T" and Corth: "pairwise orthogonal C"
              and C1:"\<And>x. x \<in> C \<Longrightarrow> norm x = 1"
              and "independent C" "finite C" "card C = dim T" "span C = T"
-    by (metis orthonormal_basis_subspace [OF T] independent_finite)
+    by (metis orthonormal_basis_subspace [OF T] independent_imp_finite)
   obtain fb where "fb ` B \<subseteq> C" "inj_on fb B"
     by (metis \<open>card B = dim S\<close> \<open>card C = dim T\<close> \<open>finite B\<close> \<open>finite C\<close> card_le_inj d)
   then have pairwise_orth_fb: "pairwise (\<lambda>v j. orthogonal (fb v) (fb j)) B"
@@ -3003,11 +3003,11 @@
   obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
              and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
              and "independent B" "finite B" "card B = dim S" "span B = S"
-    by (metis orthonormal_basis_subspace [OF S] independent_finite)
+    by (metis orthonormal_basis_subspace [OF S] independent_imp_finite)
   obtain C where "C \<subseteq> T" and Corth: "pairwise orthogonal C"
              and C1:"\<And>x. x \<in> C \<Longrightarrow> norm x = 1"
              and "independent C" "finite C" "card C = dim T" "span C = T"
-    by (metis orthonormal_basis_subspace [OF T] independent_finite)
+    by (metis orthonormal_basis_subspace [OF T] independent_imp_finite)
   obtain fb where "bij_betw fb B C"
     by (metis \<open>finite B\<close> \<open>finite C\<close> bij_betw_iff_card \<open>card B = dim S\<close> \<open>card C = dim T\<close> d)
   then have pairwise_orth_fb: "pairwise (\<lambda>v j. orthogonal (fb v) (fb j)) B"
diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -102,13 +102,11 @@
 
 lemma sets_Collect_single':
   "i \<in> I \<Longrightarrow> {x\<in>space (M i). P x} \<in> sets (M i) \<Longrightarrow> {x\<in>space (PiM I M). P (x i)} \<in> sets (PiM I M)"
-  using sets_Collect_single[of i I "{x\<in>space (M i). P x}" M]
-  by (simp add: space_PiM PiE_iff cong: conj_cong)
+  by auto
 
 lemma (in finite_product_prob_space) finite_measure_PiM_emb:
   "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> measure (PiM I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))"
-  using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets.sets_into_space, of I A M]
-  by auto
+  by (rule prob_times)
 
 lemma (in product_prob_space) PiM_component:
   assumes "i \<in> I"
diff -r 1425a366fe7f -r 56a408fa2440 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Topological_Spaces.thy	Sat Aug 12 10:09:29 2023 +0100
@@ -1220,6 +1220,11 @@
   "f \<longlonglongrightarrow> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
   unfolding tendsto_def eventually_sequentially by auto
 
+lemma closed_sequentially:
+  assumes "closed S" and "\<And>n. f n \<in> S" and "f \<longlonglongrightarrow> l"
+  shows "l \<in> S"
+  by (metis Lim_in_closed_set assms eventually_sequentially trivial_limit_sequentially)
+
 
 subsection \<open>Monotone sequences and subsequences\<close>