# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1691342949 -3600
# Node ID b22f39c54e8cd4e80c92b4dd7982201f9ea26401
# Parent  37abfe400ae69e6286009751da0ffffa1fc430e3
Tidied up more messy proofs

diff -r 37abfe400ae6 -r b22f39c54e8c src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Fri Aug 04 19:17:49 2023 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Sun Aug 06 18:29:09 2023 +0100
@@ -30,70 +30,66 @@
 interpretation vec: vector_space "(*s) "
   by unfold_locales (vector algebra_simps)+
 
-lemma independent_cart_basis:
-  "vec.independent (cart_basis)"
+lemma independent_cart_basis: "vec.independent (cart_basis)"
 proof (rule vec.independent_if_scalars_zero)
   show "finite (cart_basis)" using finite_cart_basis .
   fix f::"('a, 'b) vec \<Rightarrow> 'a" and x::"('a, 'b) vec"
   assume eq_0: "(\<Sum>x\<in>cart_basis. f x *s x) = 0" and x_in: "x \<in> cart_basis"
   obtain i where x: "x = axis i 1" using x_in unfolding cart_basis_def by auto
   have sum_eq_0: "(\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i)) = 0"
-  proof (rule sum.neutral, rule ballI)
-    fix xa assume xa: "xa \<in> cart_basis - {x}"
-    obtain a where a: "xa = axis a 1" and a_not_i: "a \<noteq> i"
-      using xa x unfolding cart_basis_def by auto
-    have "xa $ i = 0" unfolding a axis_def using a_not_i by auto
-    thus "f xa * xa $ i = 0" by simp
+  proof (intro sum.neutral ballI)
+    fix y assume y: "y \<in> cart_basis - {x}"
+    obtain a where a: "y = axis a 1" and a_not_i: "a \<noteq> i"
+      using y x unfolding cart_basis_def by auto
+    have "y $ i = 0" unfolding a axis_def using a_not_i by auto
+    thus "f y * y $ i = 0" by simp
   qed
   have "0 = (\<Sum>x\<in>cart_basis. f x *s x) $ i" using eq_0 by simp
-  also have "... = (\<Sum>x\<in>cart_basis. (f x *s x) $ i)" unfolding sum_component ..
-  also have "... = (\<Sum>x\<in>cart_basis. f x * (x $ i))" unfolding vector_smult_component ..
-  also have "... = f x * (x $ i) + (\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i))"
+  also have "\<dots> = (\<Sum>x\<in>cart_basis. (f x *s x) $ i)" unfolding sum_component ..
+  also have "\<dots> = (\<Sum>x\<in>cart_basis. f x * (x $ i))" unfolding vector_smult_component ..
+  also have "\<dots> = f x * (x $ i) + (\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i))"
     by (rule sum.remove[OF finite_cart_basis x_in])
-  also have "... =  f x * (x $ i)" unfolding sum_eq_0 by simp
-  also have "... = f x" unfolding x axis_def by auto
+  also have "\<dots> =  f x * (x $ i)" unfolding sum_eq_0 by simp
+  also have "\<dots> = f x" unfolding x axis_def by auto
   finally show "f x = 0" ..
 qed
 
-lemma span_cart_basis:
-  "vec.span (cart_basis) = UNIV"
-proof (auto)
-  fix x::"('a, 'b) vec"
-  let ?f="\<lambda>v. x $ (THE i. v = axis i 1)"
-  show "x \<in> vec.span (cart_basis)"
-    apply (unfold vec.span_finite[OF finite_cart_basis])
-    apply (rule image_eqI[of _ _ ?f])
-     apply (subst  vec_eq_iff)
-     apply clarify
+lemma span_cart_basis [simp]: "vec.span (cart_basis) = UNIV"
+proof -
+  have "x \<in> vec.span cart_basis" for x :: "('a, 'b) vec"
   proof -
-    fix i::'b
-    let ?w = "axis i (1::'a)"
-    have the_eq_i: "(THE a. ?w = axis a 1) = i"
-      by (rule the_equality, auto simp: axis_eq_axis)
-    have sum_eq_0: "(\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i) = 0"
-    proof (rule sum.neutral, rule ballI)
-      fix xa::"('a, 'b) vec"
-      assume xa: "xa \<in> cart_basis - {?w}"
-      obtain j where j: "xa = axis j 1" and i_not_j: "i \<noteq> j" using xa unfolding cart_basis_def by auto
-      have the_eq_j: "(THE i. xa = axis i 1) = j"
-      proof (rule the_equality)
-        show "xa = axis j 1" using j .
-        show "\<And>i. xa = axis i 1 \<Longrightarrow> i = j" by (metis axis_eq_axis j zero_neq_one)
+    let ?f="\<lambda>v. x $ (THE i. v = axis i 1)"
+    have "x $ i = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i" for i::'b
+    proof -
+      let ?w = "axis i (1::'a)"
+      have the_eq_i: "(THE a. ?w = axis a 1) = i"
+        by (rule the_equality, auto simp: axis_eq_axis)
+      have sum_eq_0: "(\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i) = 0"
+      proof (intro sum.neutral ballI)
+        fix y:: "('a, 'b) vec"
+        assume y: "y \<in> cart_basis - {?w}"
+        obtain j where j: "y = axis j 1" and i_not_j: "i \<noteq> j" 
+          using y unfolding cart_basis_def by auto
+        have the_eq_j: "(THE i. y = axis i 1) = j"
+          by (simp add: axis_eq_axis j)
+        show "x $ (THE i. y = axis i 1) * y $ i = 0"
+          by (simp add: axis_def i_not_j j)
       qed
-      show "x $ (THE i. xa = axis i 1) * xa $ i = 0"
-        apply (subst (2) j)
-        unfolding the_eq_j unfolding axis_def using i_not_j by simp
+      have "(\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i 
+           = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) * v $ i)"
+        by force
+      also have "\<dots> = x $ (THE a. ?w = axis a 1) * ?w $ i + (\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i)"
+        by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def)
+      also have "\<dots> = x $ (THE a. ?w = axis a 1) * ?w $ i" 
+        unfolding sum_eq_0 by simp
+      also have "\<dots> = x $ i" 
+        unfolding the_eq_i unfolding axis_def by auto
+      finally show ?thesis by simp
     qed
-    have "(\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i =
-  (\<Sum>v\<in>cart_basis. (x $ (THE i. v = axis i 1) *s v) $ i)" unfolding sum_component ..
-    also have "... = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) * v $ i)"
-      unfolding vector_smult_component ..
-    also have "... = x $ (THE a. ?w = axis a 1) * ?w $ i + (\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i)"
-      by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def)
-    also have "... = x $ (THE a. ?w = axis a 1) * ?w $ i" unfolding sum_eq_0 by simp
-    also have "... = x $ i" unfolding the_eq_i unfolding axis_def by auto
-    finally show "x $ i = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i" by simp
-  qed simp
+    then show "x \<in> vec.span (cart_basis)"
+      by (metis (no_types, lifting) vec.span_base vec.span_scale vec.span_sum vec_eq_iff)
+  qed
+  then show ?thesis by auto
 qed
 
 (*Some interpretations:*)
@@ -138,10 +134,12 @@
 lemma matrix_works:
   assumes lf: "Vector_Spaces.linear (*s) (*s) f"
   shows "matrix f *v x = f (x::'a::field ^ 'n)"
-  apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
-  apply clarify
-  apply (rule linear_componentwise[OF lf, symmetric])
-  done
+proof -
+  have "\<forall>i. (\<Sum>j\<in>UNIV. x $ j * f (axis j 1) $ i) = f x $ i"
+    by (simp add: Cartesian_Space.linear_componentwise lf)
+  then show ?thesis
+    by (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
+qed
 
 lemma matrix_of_matrix_vector_mul[simp]: "matrix(\<lambda>x. A *v (x :: 'a::field ^ 'n)) = A"
   by (simp add: matrix_eq matrix_works)
@@ -190,44 +188,27 @@
 next
   assume "inj ((*v) A)"
   from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
-  obtain g where "Vector_Spaces.linear (*s) (*s) g" and g: "g \<circ> (*v) A = id"
+  obtain g where "Vector_Spaces.linear (*s) (*s) g" and "g \<circ> (*v) A = id"
     by blast
-  have "matrix g ** A = mat 1"
-    by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear (*s) (*s) g\<close> g matrix_compose_gen
-        matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
+  then have "matrix g ** A = mat 1"
+    by (metis matrix_compose_gen matrix_id_mat_1 matrix_of_matrix_vector_mul vec.linear_axioms)
   then show "\<exists>B. B ** A = mat 1"
     by metis
 qed
 
 lemma matrix_left_invertible_ker:
   "(\<exists>B. (B::'a::{field} ^'m^'n) ** (A::'a::{field}^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"
-  unfolding matrix_left_invertible_injective
-  using vec.inj_on_iff_eq_0[OF vec.subspace_UNIV, of A]
-  by (simp add: inj_on_def)
+  by (simp add: matrix_left_invertible_injective vec.inj_iff_eq_0)
 
 lemma matrix_right_invertible_surjective:
   "(\<exists>B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
 proof -
-  { fix B :: "'a ^'m^'n"
-    assume AB: "A ** B = mat 1"
-    { fix x :: "'a ^ 'm"
-      have "A *v (B *v x) = x"
-        by (simp add: matrix_vector_mul_assoc AB) }
-    hence "surj ((*v) A)" unfolding surj_def by metis }
-  moreover
-  { assume sf: "surj ((*v) A)"
-    from vec.linear_surjective_right_inverse[OF _ this]
-    obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear (*s) (*s) g" "(*v) A \<circ> g = id"
-      by blast
-
-    have "A ** (matrix g) = mat 1"
-      unfolding matrix_eq  matrix_vector_mul_lid
-        matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
-      using g(2) unfolding o_def fun_eq_iff id_def
-      .
-    hence "\<exists>B. A ** (B::'a^'m^'n) = mat 1" by blast
-  }
-  ultimately show ?thesis unfolding surj_def by blast
+  have "\<And>B x. A ** B = mat 1 \<Longrightarrow> \<exists>y. x = A *v y"
+    by (metis matrix_vector_mul_assoc matrix_vector_mul_lid)
+  moreover have "\<forall>x. \<exists>xa. x = A *v xa \<Longrightarrow> \<exists>B. A ** B = mat 1"
+    by (metis (mono_tags, lifting) matrix_compose_gen matrix_id_mat_1 matrix_of_matrix_vector_mul surj_def vec.linear_axioms vec.linear_surjective_right_inverse)
+  ultimately show ?thesis
+    by (auto simp: image_def set_eq_iff)
 qed
 
 lemma matrix_left_invertible_independent_columns:
@@ -237,33 +218,20 @@
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof -
   let ?U = "UNIV :: 'n set"
-  { assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"
-    { fix c i
-      assume c: "sum (\<lambda>i. c i *s column i A) ?U = 0" and i: "i \<in> ?U"
-      let ?x = "\<chi> i. c i"
-      have th0:"A *v ?x = 0"
-        using c
-        by (vector matrix_mult_sum)
-      from k[rule_format, OF th0] i
-      have "c i = 0" by (vector vec_eq_iff)}
-    hence ?rhs by blast }
-  moreover
-  { assume H: ?rhs
-    { fix x assume x: "A *v x = 0"
-      let ?c = "\<lambda>i. ((x$i ):: 'a)"
-      from H[rule_format, of ?c, unfolded matrix_mult_sum[symmetric], OF x]
-      have "x = 0" by vector }
-  }
-  ultimately show ?thesis unfolding matrix_left_invertible_ker by auto
+  have "c i = 0"
+    if "\<forall>x. A *v x = 0 \<longrightarrow> x = 0" "sum (\<lambda>i. c i *s column i A) ?U = 0" for c i
+    by (metis (no_types) UNIV_I matrix_mult_sum vec_lambda_eta vec_nth_cases zero_vec_def that)
+  moreover have "x = 0" if "A *v x = 0" ?rhs for x
+    by (metis (full_types) matrix_mult_sum that vec_eq_iff zero_index)
+  ultimately show ?thesis 
+    unfolding matrix_left_invertible_ker by auto
 qed
 
 lemma matrix_right_invertible_independent_rows:
   fixes A :: "'a::{field}^'n^'m"
   shows "(\<exists>(B::'a^'m^'n). A ** B = mat 1) \<longleftrightarrow>
-    (\<forall>c. sum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
-  unfolding left_invertible_transpose[symmetric]
-    matrix_left_invertible_independent_columns
-  by (simp add:)
+         (\<forall>c. sum (\<lambda>i::'m. c i *s row i A) UNIV = 0 \<longrightarrow> (\<forall>i. c i = 0))"
+  by (simp add: matrix_left_invertible_independent_columns flip: left_invertible_transpose)
 
 lemma matrix_right_invertible_span_columns:
   "(\<exists>(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \<longleftrightarrow>
@@ -277,14 +245,10 @@
   have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast
   { assume h: ?lhs
     { fix x:: "'a ^'n"
-      from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m"
-        where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
-      have "x \<in> vec.span (columns A)"
-        unfolding y[symmetric] scalar_mult_eq_scaleR
-      proof (rule vec.span_sum [OF vec.span_scale])
-        show "column i A \<in> vec.span (columns A)" for i
-          using columns_def vec.span_superset by auto
-      qed
+      obtain y :: "'a ^'m" where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x"
+        using h lhseq by blast
+      then have "x \<in> vec.span (columns A)"
+        by (metis (mono_tags, lifting) columns_def mem_Collect_eq vec.span_base vec.span_scale vec.span_sum)
     }
     then have ?rhs unfolding rhseq by blast }
   moreover
@@ -313,14 +277,14 @@
             using i(1) by (simp add: field_simps)
           have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
               else (x$xa) * ((column xa A$j))) ?U = sum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U"
-            by (rule sum.cong[OF refl]) (use th in blast)
+            using th by force
           also have "\<dots> = sum (\<lambda>xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
             by (simp add: sum.distrib)
           also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
-            unfolding sum.delta[OF fU]
-            using i(1) by simp
+            unfolding sum.delta[OF fU] using i(1) by simp
           finally show "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
-            else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
+                                            else (x$xa) * ((column xa A$j))) ?U 
+                      = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
         qed
       qed
     }
@@ -331,10 +295,7 @@
 
 lemma matrix_left_invertible_span_rows_gen:
   "(\<exists>(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \<longleftrightarrow> vec.span (rows A) = UNIV"
-  unfolding right_invertible_transpose[symmetric]
-  unfolding columns_transpose[symmetric]
-  unfolding matrix_right_invertible_span_columns
-  ..
+  by (metis columns_transpose matrix_right_invertible_span_columns right_invertible_transpose)
 
 lemma matrix_left_invertible_span_rows:
   "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
@@ -348,17 +309,13 @@
     assume AA': "A ** A' = mat 1"
     have sA: "surj ((*v) A)"
       using AA' matrix_right_invertible_surjective by auto
-    from vec.linear_surjective_isomorphism[OF matrix_vector_mul_linear_gen sA]
     obtain f' :: "'a ^'n \<Rightarrow> 'a ^'n"
-      where f': "Vector_Spaces.linear (*s) (*s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
-    have th: "matrix f' ** A = mat 1"
-      by (simp add: matrix_eq matrix_works[OF f'(1)]
-          matrix_vector_mul_assoc[symmetric] f'(2)[rule_format])
-    hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp
-    hence "matrix f' = A'"
-      by (simp add: matrix_mul_assoc[symmetric] AA')
-    hence "matrix f' ** A = A' ** A" by simp
-    hence "A' ** A = mat 1" by (simp add: th)
+      where f': "Vector_Spaces.linear (*s) (*s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x"
+      using sA vec.linear_surjective_isomorphism by blast 
+    have "matrix f' ** A = mat 1"
+      by (metis f' matrix_eq matrix_vector_mul_assoc matrix_vector_mul_lid matrix_works)
+    hence "A' ** A = mat 1"
+      by (metis AA' matrix_mul_assoc matrix_mul_lid)
   }
   then show ?thesis by blast
 qed
@@ -382,22 +339,12 @@
     using inv_A unfolding invertible_def by blast
   obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1" 
     using inv_B unfolding invertible_def by blast
-  show ?thesis
-  proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI)
-    have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))" 
-      using matrix_mul_assoc[of A B "(B' ** A')", symmetric] .
-    also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] ..
-    also have "... = A ** (mat 1 ** A')" unfolding BB' ..
-    also have "... = A ** A'" unfolding matrix_mul_lid ..
-    also have "... = mat 1" unfolding AA' ..
-    finally show "A ** B ** (B' ** A') = mat (1::'a)" .    
-    have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] .
-    also have "... =  B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] ..
-    also have "... =  B' ** (mat 1 ** B)" unfolding A'A ..
-    also have "... = B' ** B"  unfolding matrix_mul_lid ..
-    also have "... = mat 1" unfolding B'B ..
-    finally show "B' ** A' ** (A ** B) = mat 1" .
-  qed
+  have "A ** B ** (B' ** A') = mat 1"
+    by (metis AA' BB' matrix_mul_assoc matrix_mul_rid)
+  moreover have "B' ** A' ** (A ** B) = mat 1"
+    by (metis A'A B'B matrix_mul_assoc matrix_mul_rid)
+  ultimately show ?thesis
+    using invertible_def by blast
 qed
 
 lemma transpose_invertible:
@@ -409,12 +356,7 @@
 lemma vector_matrix_mul_assoc:
   fixes v :: "('a::comm_semiring_1)^'n"
   shows "(v v* M) v* N = v v* (M ** N)"
-proof -
-  from matrix_vector_mul_assoc
-  have "transpose N *v (transpose M *v v) = (transpose N ** transpose M) *v v" by fast
-  thus "(v v* M) v* N = v v* (M ** N)"
-    by (simp add: matrix_transpose_mul [symmetric])
-qed
+  by (metis (no_types, opaque_lifting) matrix_transpose_mul matrix_vector_mul_assoc transpose_matrix_vector)
 
 lemma matrix_scaleR_vector_ac:
   fixes A :: "real^('m::finite)^'n"
@@ -426,8 +368,7 @@
   shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v"
   by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR)
 
-(*Finally, some interesting theorems and interpretations that don't appear in any file of the
-  library.*)
+subsection \<open>Some interesting theorems and interpretations\<close>
 
 locale linear_first_finite_dimensional_vector_space =
   l?: Vector_Spaces.linear scaleB scaleC f +
@@ -438,25 +379,10 @@
   and f :: "('b=>'c)"
 
 lemma vec_dim_card: "vec.dim (UNIV::('a::{field}^'n) set) = CARD ('n)"
-proof -
-  let ?f="\<lambda>i::'n. axis i (1::'a)"
-  have "vec.dim (UNIV::('a::{field}^'n) set) = card (cart_basis::('a^'n) set)"
-    unfolding vec.dim_UNIV ..
-  also have "... = card ({i. i\<in> UNIV}::('n) set)"
-    proof (rule bij_betw_same_card[of ?f, symmetric], unfold bij_betw_def, auto)
-      show "inj (\<lambda>i::'n. axis i (1::'a))"  by (simp add: inj_on_def axis_eq_axis)
-      fix i::'n
-      show "axis i 1 \<in> cart_basis" unfolding cart_basis_def by auto
-      fix x::"'a^'n"
-      assume "x \<in> cart_basis"
-      thus "x \<in> range (\<lambda>i. axis i 1)" unfolding cart_basis_def by auto
-    qed
-  also have "... = CARD('n)" by auto
-  finally show ?thesis .
-qed
+  by (simp add: card_cart_basis)
 
 interpretation vector_space_over_itself: vector_space "(*) :: 'a::field \<Rightarrow> 'a \<Rightarrow> 'a"
-by unfold_locales (simp_all add: algebra_simps)
+  by unfold_locales (simp_all add: algebra_simps)
 
 lemmas [simp del] = vector_space_over_itself.scale_scale
 
@@ -484,24 +410,12 @@
   by (simp add: matrix_vector_mult_def inner_vec_def)
 
 lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
-  apply (rule adjoint_unique)
-  apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
-    sum_distrib_right sum_distrib_left)
-  apply (subst sum.swap)
-  apply (simp add:  ac_simps)
-  done
+  by (metis adjoint_unique dot_lmul_matrix vector_transpose_matrix)
 
-lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
+lemma matrix_adjoint: 
+  assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
   shows "matrix(adjoint f) = transpose(matrix f)"
-proof -
-  have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))"
-    by (simp add: lf)
-  also have "\<dots> = transpose(matrix f)"
-    unfolding adjoint_matrix matrix_of_matrix_vector_mul
-    apply rule
-    done
-  finally show ?thesis .
-qed
+  by (metis adjoint_matrix assms matrix_of_matrix_vector_mul matrix_vector_mul(2))
 
 
 subsection\<open> Rank of a matrix\<close>
@@ -511,10 +425,8 @@
 lemma matrix_vector_mult_in_columnspace_gen:
   fixes A :: "'a::field^'n^'m"
   shows "(A *v x) \<in> vec.span(columns A)"
-  apply (simp add: matrix_vector_column columns_def transpose_def column_def)
-  apply (intro vec.span_sum vec.span_scale)
-  apply (force intro: vec.span_base)
-  done
+  unfolding columns_def
+  by (metis (mono_tags, lifting) matrix_mult_sum mem_Collect_eq vec.span_base vec.span_scale vec.span_sum)
 
 lemma matrix_vector_mult_in_columnspace:
   fixes A :: "real^'n^'m"
@@ -576,9 +488,7 @@
     then have ind: "independent ((*v) A ` B)"
       by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>])
     have "dim (span (rows A)) \<le> card ((*v) A ` B)"
-      unfolding B(2)[symmetric]
-      using inj
-      by (auto simp: card_image inj_on_subset span_superset)
+      by (metis B(2) card_image inj inj_on_subset order.refl span_superset)
     also have "\<dots> \<le> dim (span (columns A))"
       using _ ind
       by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace)
@@ -613,13 +523,7 @@
   fixes A :: "real^'n^'m"
   shows "rank A = dim(range (\<lambda>x. A *v x))"
   unfolding column_rank_def
-proof (rule span_eq_dim)
-  have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r")
-    by (simp add: columns_image_basis image_subsetI span_mono)
-  then show "?l = ?r"
-    by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace
-        span_eq span_span)
-qed
+  by (smt (verit, best) columns_image_basis dim_span image_subset_iff iso_tuple_UNIV_I matrix_vector_mult_in_columnspace span_eq)
 
 lemma rank_bound:
   fixes A :: "real^'n^'m"
@@ -636,8 +540,7 @@
 lemma full_rank_surjective:
   fixes A :: "real^'n^'m"
   shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)"
-  by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
-                matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
+  by (metis (no_types, opaque_lifting) dim_eq_full dim_vec_eq rank_dim_range span_vec_eq vec.span_UNIV vec.span_image vec_dim_card)
 
 lemma rank_I: "rank(mat 1::real^'n^'n) = CARD('n)"
   by (simp add: full_rank_injective inj_on_def)
@@ -645,7 +548,7 @@
 lemma less_rank_noninjective:
   fixes A :: "real^'n^'m"
   shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)"
-using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
+  using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
 
 lemma matrix_nonfull_linear_equations_eq:
   fixes A :: "real^'n^'m"
@@ -680,9 +583,10 @@
   shows "x = 1 \<or> x = 2"
 proof (induct x)
   case (of_int z)
-  then have "0 \<le> z" and "z < 2" by simp_all
-  then have "z = 0 | z = 1" by arith
-  then show ?case by auto
+  then have "z = 0 | z = 1"
+    by fastforce
+  then show ?case 
+    by auto
 qed
 
 lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
@@ -693,8 +597,7 @@
   shows "x = 1 \<or> x = 2 \<or> x = 3"
 proof (induct x)
   case (of_int z)
-  then have "0 \<le> z" and "z < 3" by simp_all
-  then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
+  then have "z = 0 \<or> z = 1 \<or> z = 2" by fastforce
   then show ?case by auto
 qed
 
@@ -706,8 +609,7 @@
   shows "x = 1 \<or> x = 2 \<or> x = 3 \<or> x = 4"
 proof (induct x)
   case (of_int z)
-  then have "0 \<le> z" and "z < 4" by simp_all
-  then have "z = 0 \<or> z = 1 \<or> z = 2 \<or> z = 3" by arith
+  then have "z = 0 \<or> z = 1 \<or> z = 2 \<or> z = 3" by fastforce
   then show ?case by auto
 qed
 
@@ -744,10 +646,7 @@
   by (simp add: vec_eq_iff)
 
 lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
-  apply auto
-  apply (erule_tac x= "x$1" in allE)
-  apply (simp only: vector_one[symmetric])
-  done
+  by (metis vector_one)
 
 lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
   by (simp add: norm_vec_def)
@@ -791,7 +690,7 @@
   shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a))
          (at ((vec a)::real^1) within vec ` S)"
     using der_g
-    apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
+    apply (clarsimp simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
     apply (drule tendsto_at_within_vector_1, vector)
     apply (auto simp: algebra_simps eventually_at tendsto_def)
     done
@@ -817,46 +716,33 @@
   by (metis vector_1 vector_one)
 
 lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
-  apply auto
-  apply (erule_tac x="v$1" in allE)
-  apply (erule_tac x="v$2" in allE)
-  apply (subgoal_tac "vector [v$1, v$2] = v")
-  apply simp
-  apply (vector vector_def)
-  apply (simp add: forall_2)
-  done
+proof -
+  have "P v" if "\<And>x y. P (vector [x, y])" for v
+  proof -
+    have "vector [v$1, v$2] = v"
+      by (smt (verit, best) exhaust_2 vec_eq_iff vector_2)
+    then show ?thesis
+      by (metis that)
+  qed
+  then show ?thesis by auto
+qed
 
 lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
-  apply auto
-  apply (erule_tac x="v$1" in allE)
-  apply (erule_tac x="v$2" in allE)
-  apply (erule_tac x="v$3" in allE)
-  apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
-  apply simp
-  apply (vector vector_def)
-  apply (simp add: forall_3)
-  done
+proof -
+  have "P v" if "\<And>x y z. P (vector [x, y, z])" for v
+  proof -
+    have "vector [v$1, v$2, v$3] = v"
+      by (smt (verit, best) exhaust_3 vec_eq_iff vector_3)
+    then show ?thesis
+      by (metis that)
+  qed
+  then show ?thesis by auto
+qed
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>lambda skolemization on cartesian products\<close>
 
-lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
-   (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
-proof -
-  let ?S = "(UNIV :: 'n set)"
-  { assume H: "?rhs"
-    then have ?lhs by auto }
-  moreover
-  { assume H: "?lhs"
-    then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
-    let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
-    { fix i
-      from f have "P i (f i)" by metis
-      then have "P i (?x $ i)" by auto
-    }
-    hence "\<forall>i. P i (?x$i)" by metis
-    hence ?rhs by metis }
-  ultimately show ?thesis by metis
-qed
+lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))"
+  by (metis vec_lambda_beta)
 
 
 text \<open>The same result in terms of square matrices.\<close>
@@ -885,8 +771,7 @@
   fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
   shows "(A *v x) \<bullet> (B *v y) =
       (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
-  unfolding dot_matrix_product transpose_columnvector[symmetric]
-    dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
+  by (metis dot_lmul_matrix dot_matrix_product dot_rowvector_columnvector matrix_mul_assoc vector_transpose_matrix)
 
 
 lemma dim_substandard_cart: "vec.dim {x::'a::field^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d"
@@ -931,7 +816,7 @@
   hence "m *s x = y - c" by (simp add: field_simps)
   hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
   then show "x = inverse m *s y + - (inverse m *s c)"
-    using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
+    by (simp add: m0 vec.scale_right_diff_distrib)
 next
   assume h: "x = inverse m *s y + - (inverse m *s c)"
   show "m *s x + c = y" unfolding h
@@ -940,8 +825,7 @@
 
 lemma vector_eq_affinity:
     "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"
-  using vector_affinity_eq[where m=m and x=x and y=y and c=c]
-  by metis
+  by (metis vector_affinity_eq)
 
 lemma vector_cart:
   fixes f :: "real^'n \<Rightarrow> real"
@@ -1017,14 +901,9 @@
       by blast
   }
   moreover
-  {
-    assume lf: "Vector_Spaces.linear (*s) (*s) f" and om: "orthogonal_matrix ?mf"
-    from lf om have ?lhs
-      unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
-      apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul)
-      apply (simp add: dot_matrix_product linear_def scalar_mult_eq_scaleR)
-      done
-  }
+  have ?lhs if "Vector_Spaces.linear (*s) (*s) f" and "orthogonal_matrix ?mf"
+    using that unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
+      by (metis dot_matrix_product dot_matrix_vector_mul linear_matrix_vector_mul_eq matrix_mul_lid matrix_vector_mul(2))
   ultimately show ?thesis
     by (auto simp: linear_def scalar_mult_eq_scaleR)
 qed
@@ -1052,7 +931,7 @@
           (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
   using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
 
-proposition  orthogonal_matrix_exists_basis:
+proposition orthogonal_matrix_exists_basis:
   fixes a :: "real^'n"
   assumes "norm a = 1"
   obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
@@ -1084,16 +963,13 @@
   assumes "norm a = 1" "norm b = 1"
   obtains f where "orthogonal_transformation f" "f a = b"
 proof -
-  obtain k::'n where True
-    by simp
-  obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
+  obtain k A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
     using orthogonal_matrix_exists_basis assms by metis
   let ?f = "\<lambda>x. (B ** transpose A) *v x"
   show thesis
   proof
     show "orthogonal_transformation ?f"
-      by (subst orthogonal_transformation_matrix)
-        (auto simp: AB orthogonal_matrix_mul)
+      by (simp add: AB orthogonal_matrix_mul orthogonal_transformation_matrix)
   next
     show "?f a = b"
       using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def
@@ -1101,7 +977,7 @@
   qed
 qed
 
-proposition  orthogonal_transformation_exists:
+proposition orthogonal_transformation_exists:
   fixes a b :: "real^'n"
   assumes "norm a = norm b"
   obtains f where "orthogonal_transformation f" "f a = b"
@@ -1114,16 +990,7 @@
   then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
     by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"])
   show ?thesis
-  proof
-    interpret linear f
-      using f by (simp add: orthogonal_transformation_linear)
-    have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)"
-      by (simp add: scale)
-    also have "\<dots> = b /\<^sub>R norm a"
-      by (simp add: eq assms [symmetric])
-    finally show "f a = b"
-      using False by auto
-  qed (use f in auto)
+    using False assms eq f orthogonal_transformation_scaleR that by fastforce
 qed
 
 
@@ -1157,9 +1024,7 @@
 proposition  orthogonal_transformation_isometry:
   "orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
   unfolding orthogonal_transformation
-  apply (auto simp: linear_0 isometry_linear)
-   apply (metis (no_types, opaque_lifting) dist_norm linear_diff)
-  by (metis dist_0_norm)
+  by (metis dist_0_norm dist_norm isometry_linear linear_0 linear_diff)
 
 
 text \<open>Can extend an isometry from unit sphere:\<close>
@@ -1369,10 +1234,7 @@
       apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong)
       done
     show ?thesis
-      apply (subst eq)
-      apply (intro mult idplus that)
-       apply (auto intro: diagonal)
-      done
+      unfolding eq by (intro mult idplus that) (auto intro: diagonal)
   qed
   show ?thesis
     by (rule induct_matrix_elementary) (auto intro: assms *)
diff -r 37abfe400ae6 -r b22f39c54e8c src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Fri Aug 04 19:17:49 2023 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Sun Aug 06 18:29:09 2023 +0100
@@ -115,7 +115,6 @@
     "\<And>i. ereal (l i) < c"
     "(\<lambda>x. ereal (l x)) \<longlonglongrightarrow> a"
     by auto
-  { fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp }
   have "einterval a b = (\<Union>i. {l i .. u i})"
   proof (auto simp: einterval_iff)
     fix x assume "a < ereal x" "ereal x < b"
@@ -134,8 +133,9 @@
     show "a < ereal x" "ereal x < b"
       by (auto simp flip: ereal_less_eq(3))
   qed
-  show thesis
-    by (intro that) fact+
+  moreover { fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp }
+  ultimately show thesis
+    by (simp add: l that u)
 qed
 
 (* TODO: in this definition, it would be more natural if einterval a b included a and b when
@@ -191,9 +191,9 @@
 lemma interval_lebesgue_integral_add [intro, simp]:
   fixes M a b f
   assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g"
-  shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" and
-    "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) =
-   interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
+  shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)"
+    and "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) =
+         interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
 using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
     field_simps)
 
@@ -291,11 +291,8 @@
 next
   case (le a b) 
   have "LBINT x:{x. - x \<in> einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)"
-    unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def
-    apply (rule Bochner_Integration.integral_cong [OF refl])
-    by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
-             simp flip: uminus_ereal.simps
-             split: split_indicator)
+    unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def einterval_def
+    by (metis (lifting) ereal_less_uminus_reorder ereal_uminus_less_reorder indicator_simps mem_Collect_eq uminus_ereal.simps(1))
   then show ?case
     unfolding interval_lebesgue_integral_def 
     by (subst set_integral_reflect) (simp add: le)
@@ -333,27 +330,12 @@
   assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x"
   shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
   using assms
-proof (induct a b rule: linorder_wlog)
-  case (sym a b) then show ?case
-    by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
-next
-  case (le a b) then show ?case
-    by (auto simp: interval_lebesgue_integral_def max_def min_def
-             intro!: set_lebesgue_integral_cong_AE)
-qed
+  by (auto simp: interval_lebesgue_integral_def max_def min_def intro!: set_lebesgue_integral_cong_AE)
 
 lemma interval_integral_cong:
   assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x"
   shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
-  using assms
-proof (induct a b rule: linorder_wlog)
-  case (sym a b) then show ?case
-    by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
-next
-  case (le a b) then show ?case
-    by (auto simp: interval_lebesgue_integral_def max_def min_def
-             intro!: set_lebesgue_integral_cong)
-qed
+  using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_cong)
 
 lemma interval_lebesgue_integrable_cong_AE:
     "f \<in> borel_measurable lborel \<Longrightarrow> g \<in> borel_measurable lborel \<Longrightarrow>
@@ -369,7 +351,7 @@
   shows  "f \<in> borel_measurable lborel \<Longrightarrow>
     interval_lebesgue_integrable lborel a b (\<lambda>x. \<bar>f x\<bar>) = interval_lebesgue_integrable lborel a b f"
   unfolding interval_lebesgue_integrable_def
-  by (subst (1 2) set_integrable_abs_iff') simp_all
+  by (simp add: set_integrable_abs_iff')
 
 lemma interval_integral_Icc:
   fixes a b :: real
@@ -646,35 +628,29 @@
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
     "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
     by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
-  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
+  have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
     by (rule order_less_le_trans, rule approx, force)
-  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
+  have lessb[simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
     by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
+  have cf: "\<And>i. continuous_on {min (l i) (u i)..max (l i) (u i)} f"
+    using approx f by (intro continuous_at_imp_continuous_on strip) auto
   have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
-    using assms approx apply (intro interval_integral_FTC_finite)
-    apply (auto simp: less_imp_le min_def max_def
-      has_real_derivative_iff_has_vector_derivative[symmetric])
-    apply (rule continuous_at_imp_continuous_on, auto intro!: f)
-    by (rule DERIV_subset [OF F], auto)
+    apply (intro interval_integral_FTC_finite cf DERIV_subset [OF F])
+    by (smt (verit) F aless approx(4) has_real_derivative_iff_has_vector_derivative has_vector_derivative_at_within lessb)
   have 1: "\<And>i. set_integrable lborel {l i..u i} f"
-  proof -
-    fix i show "set_integrable lborel {l i .. u i} f"
-      using \<open>a < l i\<close> \<open>u i < b\<close> unfolding set_integrable_def
-      by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
-         (auto simp flip: ereal_less_eq)
-  qed
+    by (meson aless lessb assms(3) atLeastAtMost_iff borel_integrable_atLeastAtMost' continuous_at_imp_continuous_on)
   have 2: "set_borel_measurable lborel (einterval a b) f"
     unfolding set_borel_measurable_def
     by (auto simp del: real_scaleR_def intro!: borel_measurable_continuous_on_indicator
              simp: continuous_on_eq_continuous_at einterval_iff f)
-  have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
-    apply (subst FTCi)
-    apply (intro tendsto_intros)
+  have "(\<lambda>x. F (l x)) \<longlonglongrightarrow> A"
+    using A approx unfolding tendsto_at_iff_sequentially comp_def
+    by (force elim!: allE[of _ "\<lambda>i. ereal (l i)"])
+  moreover have "(\<lambda>x. F (u x)) \<longlonglongrightarrow> B"
     using B approx unfolding tendsto_at_iff_sequentially comp_def
-    using tendsto_at_iff_sequentially[where 'a=real]
-    apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
-    using A approx unfolding tendsto_at_iff_sequentially comp_def
-    by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
+    by (force elim!: allE[of _ "\<lambda>i. ereal (u i)"])
+  ultimately have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
+    by (simp add: FTCi tendsto_diff)
   show "(LBINT x=a..b. f x) = B - A"
     by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
   show "set_integrable lborel (einterval a b) f"
@@ -820,11 +796,11 @@
       by (metis antiderivative_continuous atLeastAtMost_iff image_subset_iff set_eq_subset)
   have contfg: "continuous_on {a..b} (\<lambda>x. f (g x))"
     by (blast intro: continuous_on_compose2 contf contg)
-  have "LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
-    apply (rule integral_FTC_atLeastAtMost
-                [OF \<open>a \<le> b\<close> vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def]])
-    apply (auto intro!: continuous_on_scaleR contg' contfg)
-    done
+  have "continuous_on {a..b} (\<lambda>x. g' x *\<^sub>R f (g x))"
+    by (auto intro!: continuous_on_scaleR contg' contfg)
+  then have "LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
+    using integral_FTC_atLeastAtMost [OF \<open>a \<le> b\<close> vector_diff_chain_within[OF v_derivg derivF]]
+    by force
   then have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
     by (simp add: assms interval_integral_Icc set_lebesgue_integral_def)
   moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)"
@@ -924,12 +900,11 @@
          apply (auto intro!: continuous_at_imp_continuous_on contf contg')
     done
   have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
-    apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
-    by (rule assms)
+    using approx(4) \<open>a < b\<close> integrable interval_integral_Icc_approx_integrable by fastforce
   hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
     by (simp add: eq1)
   have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
-    apply (auto simp: incseq_def)
+    apply (clarsimp simp: incseq_def, intro conjI)
     using lessb lle approx(5) g_nondec le_less_trans apply blast
     by (force intro: less_le_trans)
   have "(\<lambda>i. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f)
@@ -988,13 +963,11 @@
   have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   proof -
     have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
-      using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
-      by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
+      using A by (force simp: einterval_def tendsto_at_iff_sequentially comp_def elim!: allE[where x = "\<lambda>i. ereal (l i)"])
     hence A3: "\<And>i. g (l i) \<ge> A"
       by (intro decseq_ge, auto simp: decseq_def)
     have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
-      using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
-      by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
+      using B by (force simp: einterval_def tendsto_at_iff_sequentially comp_def elim!: allE[where x = "\<lambda>i. ereal (u i)"])
     hence B3: "\<And>i. g (u i) \<le> B"
       by (intro incseq_le, auto simp: incseq_def)
     have "ereal (g (l 0)) \<le> ereal (g (u 0))"
@@ -1013,9 +986,7 @@
       show "einterval A B \<subseteq> (\<Union>i. {g (l i)<..<g (u i)})"
         by (auto simp: einterval_def AB)
       show "(\<Union>i. {g (l i)<..<g (u i)}) \<subseteq> einterval A B"
-        apply (clarsimp simp: einterval_def, intro conjI)
-        using A3 le_ereal_less apply blast
-        using B3 ereal_le_less by blast
+        using A3 B3 by (force simp: einterval_def intro: le_ereal_less ereal_le_less)
     qed
   qed
     (* finally, the main argument *)
@@ -1030,7 +1001,7 @@
       by (simp add: ac_simps)
   qed
   have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
-    apply (clarsimp simp add: incseq_def, intro conjI)
+    apply (clarsimp simp: incseq_def, intro conjI)
     apply (meson llb antimono_def approx(3) approx(5) g_nondec le_less_trans)
     using alu uleu approx(6) g_nondec less_le_trans by blast
   have img: "\<exists>c \<ge> l i. c \<le> u i \<and> x = g c" if "g (l i) \<le> x" "x \<le> g (u i)" for x i
@@ -1041,8 +1012,7 @@
       using IVT' [of g] approx(4) dual_order.strict_implies_order by blast
   qed
   have "continuous_on {g (l i)..g (u i)} f" for i
-    apply (intro continuous_intros continuous_at_imp_continuous_on)
-    using contf img by force
+    using contf img by (force simp add: intro!: continuous_at_imp_continuous_on)
   then have int_f: "\<And>i. set_integrable lborel {g (l i)<..<g (u i)} f"
     by (rule set_integrable_subset [OF borel_integrable_atLeastAtMost']) (auto intro: less_imp_le)
   have integrable: "set_integrable lborel (\<Union>i. {g (l i)<..<g (u i)}) f"
diff -r 37abfe400ae6 -r b22f39c54e8c src/HOL/Analysis/Jordan_Curve.thy
--- a/src/HOL/Analysis/Jordan_Curve.thy	Fri Aug 04 19:17:49 2023 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy	Sun Aug 06 18:29:09 2023 +0100
@@ -42,9 +42,9 @@
                      (\<forall>x\<in>S \<union> T. (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b)) = exp (\<i>*complex_of_real (g x)))"
   proof (cases "S \<inter> T = {}")
     case True
-    have "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else h x)"
-      apply (rule continuous_on_cases_local [OF clo contg conth])
-      using True by auto
+    then have "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else h x)"
+      using continuous_on_cases_local [OF clo contg conth]
+      by (meson disjoint_iff)
     then show ?thesis
       by (rule_tac x="(\<lambda>x. if x \<in> S then g x else h x)" in exI) (auto simp: g h)
   next
@@ -54,11 +54,10 @@
       have "exp (\<i>* of_real (g x)) = exp (\<i>* of_real (h x))"
         using that by (simp add: g h)
       then obtain n where "complex_of_real (g x) = complex_of_real (h x) + 2* of_int n*complex_of_real pi"
-        apply (auto simp: exp_eq)
+        apply (simp add: exp_eq)
         by (metis complex_i_not_zero distrib_left mult.commute mult_cancel_left)
       then show ?thesis
-        apply (rule_tac x=n in exI)
-        using of_real_eq_iff by fastforce
+        using of_real_eq_iff by (fastforce intro!: exI [where x=n])
     qed
     have contgh: "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
       by (intro continuous_intros continuous_on_subset [OF contg] continuous_on_subset [OF conth]) auto
@@ -99,16 +98,16 @@
     show ?thesis
     proof (intro exI conjI)
       show "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else z + h x)"
-        apply (intro continuous_intros continuous_on_cases_local [OF clo contg] conth)
-        using z by fastforce
+        by (intro continuous_intros continuous_on_cases_local [OF clo contg] conth) (use z in force)
     qed (auto simp: g h algebra_simps exp_add)
   qed
-  ultimately have *: "homotopic_with_canon (\<lambda>x. True) (S \<union> T) (sphere 0 1)
+  ultimately have "homotopic_with_canon (\<lambda>x. True) (S \<union> T) (sphere 0 1)
                           (\<lambda>x. (x - a) /\<^sub>R cmod (x - a))  (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
     by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle)
-  show ?thesis
-    apply (rule Borsuk_maps_homotopic_in_connected_component_eq [THEN iffD1])
-    using assms by (auto simp: *)
+  moreover have "compact (S \<union> T)"
+    using assms by blast
+  ultimately show ?thesis
+    using assms Borsuk_maps_homotopic_in_connected_component_eq by fastforce
 qed
 
 
@@ -122,13 +121,8 @@
     by (simp add: \<open>closed T\<close> ccT open_Compl open_path_connected_component)
   then obtain g where g: "path g" "path_image g \<subseteq> - T" "pathstart g = a" "pathfinish g = b"
     by (auto simp: path_component_def)
-  obtain C where C: "compact C" "connected C" "a \<in> C" "b \<in> C" "C \<inter> T = {}"
-  proof
-    show "compact (path_image g)"
-      by (simp add: \<open>path g\<close> compact_path_image)
-    show "connected (path_image g)"
-      by (simp add: \<open>path g\<close> connected_path_image)
-  qed (use g in auto)
+  then obtain C where C: "compact C" "connected C" "a \<in> C" "b \<in> C" "C \<inter> T = {}"
+    by fastforce
   obtain r where "0 < r" and r: "C \<union> S \<subseteq> ball 0 r"
     by (metis \<open>compact C\<close> \<open>compact S\<close> bounded_Un compact_imp_bounded bounded_subset_ballD)
   have "connected_component (- (S \<union> (T \<inter> cball 0 r \<union> sphere 0 r))) a b"
@@ -160,10 +154,9 @@
 lemma Janiszewski_connected:
   fixes S :: "complex set"
   assumes ST: "compact S" "closed T" "connected(S \<inter> T)"
-      and notST: "connected (- S)" "connected (- T)"
-    shows "connected(- (S \<union> T))"
-using Janiszewski [OF ST]
-by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
+    and notST: "connected (- S)" "connected (- T)"
+  shows "connected(- (S \<union> T))"
+  using Janiszewski [OF ST] by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
 
 
 subsection\<open>The Jordan Curve theorem\<close>
@@ -214,8 +207,8 @@
         by (auto simp: path_image_subpath image_iff Bex_def)
     qed
     show "path_image (subpath 0 v h) \<union> path_image (subpath v 1 h) = path_image g"
-      using v apply (simp add: path_image_subpath pihg [symmetric])
-      using path_image_def by fastforce
+      using v path_image_subpath pihg path_image_def
+      by (metis (full_types) image_Un ivl_disj_un_two_touch(4))
   qed
 qed
 
@@ -257,7 +250,7 @@
       by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image outer open_Compl open_components)
     show "connected outer"
       using in_components_connected outer by blast
-    show "inner \<inter> outer = {}"
+    show inner_outer: "inner \<inter> outer = {}"
       by (meson \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>connected outer\<close> bounded_subset components_maximal in_components_subset inner outer)
     show fro_inner: "frontier inner = path_image c"
       by (simp add: Jordan_Brouwer_frontier [OF hom inner])
@@ -267,14 +260,13 @@
     proof -
       have "frontier middle = path_image c"
         by (simp add: Jordan_Brouwer_frontier [OF hom] that)
-      have middle: "open middle" "connected middle" "middle \<noteq> {}"
-        apply (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image m open_Compl open_components)
-        using in_components_connected in_components_nonempty m by blast+
+      obtain middle: "open middle" "connected middle" "middle \<noteq> {}"
+        by (metis fro_inner frontier_closed in_components_maximal m open_Compl open_components)
       obtain a0 b0 where "a0 \<in> path_image c" "b0 \<in> path_image c" "a0 \<noteq> b0"
         using simple_path_image_uncountable [OF \<open>simple_path c\<close>]
         by (metis Diff_cancel countable_Diff_eq countable_empty insert_iff subsetI subset_singleton_iff)
       obtain a b g where ab: "a \<in> path_image c" "b \<in> path_image c" "a \<noteq> b"
-                     and "arc g" "pathstart g = a" "pathfinish g = b"
+                     and g: "arc g" "pathstart g = a" "pathfinish g = b"
                      and pag_sub: "path_image g - {a,b} \<subseteq> middle"
       proof (rule dense_accessible_frontier_point_pairs [OF \<open>open middle\<close> \<open>connected middle\<close>, of "path_image c \<inter> ball a0 (dist a0 b0)" "path_image c \<inter> ball b0 (dist a0 b0)"])
         show "openin (top_of_set (frontier middle)) (path_image c \<inter> ball a0 (dist a0 b0))"
@@ -303,22 +295,21 @@
         show "closed (path_image d \<union> path_image g)"
           by (simp add: \<open>arc d\<close> \<open>arc g\<close> closed_Un closed_arc_image)
         show "connected ((path_image u \<union> path_image g) \<inter> (path_image d \<union> path_image g))"
-          by (metis Un_Diff_cancel \<open>arc g\<close> \<open>path_image u \<inter> path_image d = {a, b}\<close> \<open>pathfinish g = b\<close> \<open>pathstart g = a\<close> connected_arc_image insert_Diff1 pathfinish_in_path_image pathstart_in_path_image sup_bot.right_neutral sup_commute sup_inf_distrib1)
+          using ud_ab
+          by (metis Un_insert_left g connected_arc_image insert_absorb pathfinish_in_path_image pathstart_in_path_image sup_bot_left sup_commute sup_inf_distrib1)
         show "connected_component (- (path_image u \<union> path_image g)) x y"
           unfolding connected_component_def
         proof (intro exI conjI)
           have "connected ((inner \<union> (path_image c - path_image u)) \<union> (outer \<union> (path_image c - path_image u)))"
           proof (rule connected_Un)
             show "connected (inner \<union> (path_image c - path_image u))"
-              apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
-              using fro_inner [symmetric]  apply (auto simp: closure_subset frontier_def)
-              done
+              using connected_intermediate_closure [OF \<open>connected inner\<close>]
+              by (metis Diff_subset closure_Un_frontier dual_order.refl fro_inner sup.mono sup_ge1)
             show "connected (outer \<union> (path_image c - path_image u))"
-              apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
-              using fro_outer [symmetric]  apply (auto simp: closure_subset frontier_def)
-              done
+              using connected_intermediate_closure [OF \<open>connected outer\<close>]
+              by (simp add: Diff_eq closure_Un_frontier fro_outer sup_inf_distrib1)
             have "(inner \<inter> outer) \<union> (path_image c - path_image u) \<noteq> {}"
-              by (metis \<open>arc d\<close>  ud_ab Diff_Int Diff_cancel Un_Diff \<open>inner \<inter> outer = {}\<close> \<open>pathfinish d = a\<close> \<open>pathstart d = b\<close> arc_simple_path insert_commute nonempty_simple_path_endless sup_bot_left ud_Un)
+              using \<open>arc d\<close> \<open>pathfinish d = a\<close> \<open>pathstart d = b\<close> arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
             then show "(inner \<union> (path_image c - path_image u)) \<inter> (outer \<union> (path_image c - path_image u)) \<noteq> {}"
               by auto
           qed
@@ -344,13 +335,11 @@
           have "connected ((inner \<union> (path_image c - path_image d)) \<union> (outer \<union> (path_image c - path_image d)))"
           proof (rule connected_Un)
             show "connected (inner \<union> (path_image c - path_image d))"
-              apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
-              using fro_inner [symmetric]  apply (auto simp: closure_subset frontier_def)
-              done
+              using connected_intermediate_closure [OF \<open>connected inner\<close>] fro_inner
+              by (simp add: closure_Un_frontier sup.coboundedI2)
             show "connected (outer \<union> (path_image c - path_image d))"
-              apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
-              using fro_outer [symmetric]  apply (auto simp: closure_subset frontier_def)
-              done
+              using connected_intermediate_closure [OF \<open>connected outer\<close>]
+              by (simp add: closure_Un_frontier fro_outer sup.coboundedI2)
             have "(inner \<inter> outer) \<union> (path_image c - path_image d) \<noteq> {}"
               using \<open>arc u\<close> \<open>pathfinish u = b\<close> \<open>pathstart u = a\<close> arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
             then show "(inner \<union> (path_image c - path_image d)) \<inter> (outer \<union> (path_image c - path_image d)) \<noteq> {}"
@@ -393,8 +382,8 @@
 corollary\<^marker>\<open>tag unimportant\<close> Jordan_disconnected:
   fixes c :: "real \<Rightarrow> complex"
   assumes "simple_path c" "pathfinish c = pathstart c"
-    shows "\<not> connected(- path_image c)"
-using Jordan_curve [OF assms]
+  shows "\<not> connected(- path_image c)"
+  using Jordan_curve [OF assms]
   by (metis Jordan_Brouwer_separation assms homeomorphic_simple_path_image_circle zero_less_one)
 
 
@@ -484,7 +473,7 @@
     using Jordan_inside_outside [of "c1 +++ reversepath c"]
     using Jordan_inside_outside [of "c2 +++ reversepath c"] assms
               apply (simp_all add: path_image_join closed_Un closed_simple_path_image open_inside open_outside)
-      apply (blast elim: | metis connected_simple_path_endless)+
+      apply (blast | metis connected_simple_path_endless)+
     done
   have inout_12: "inside (?\<Theta>1 \<union> ?\<Theta>2) \<inter> (?\<Theta> - {pathstart c, pathfinish c}) \<noteq> {}"
     by (metis (no_types, lifting) c c1c ne_12 Diff_Int_distrib Diff_empty Int_empty_right Int_left_commute inf_sup_absorb inf_sup_aci(1) inside_no_overlap)
@@ -494,9 +483,8 @@
     then show False
       using connectedD [OF co_c, of "inside(?\<Theta>1 \<union> ?\<Theta>2)" "outside(?\<Theta>1 \<union> ?\<Theta>2)"]
       using c c1c2 pa_c op_in12 op_out12 inout_12
-      apply auto
-      apply (metis Un_Diff_cancel2 Un_iff compl_sup disjoint_insert(1) inf_commute inf_compl_bot_left2 inside_Un_outside mk_disjoint_insert sup_inf_absorb)
-      done
+      apply clarsimp
+      by (smt (verit, ccfv_threshold) Diff_Int_distrib Diff_cancel Diff_empty Int_assoc inf_sup_absorb inf_sup_aci(1) outside_no_overlap)
   qed
   have out_sub12: "outside(?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)" "outside(?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
     by (metis Un_commute pi_disjoint outside_Un_outside_Un)+
@@ -507,10 +495,11 @@
       by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
     have 2: "outside (?\<Theta> \<union> ?\<Theta>2) \<inter> ?\<Theta> = {}"
       by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
-    have "outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
-      apply (subst Un_commute, rule outside_Un_outside_Un)
+    have "path_image c1 \<inter> outside (path_image c2 \<union> path_image c) = {}"
       using connectedD [OF co_c1, of "inside(?\<Theta>2 \<union> ?\<Theta>)" "outside(?\<Theta>2 \<union> ?\<Theta>)"]
         pa_c1 op_in2c op_out2c ne c1 c2c 1 2 by (auto simp: inf_sup_aci)
+    then have "outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
+      by (metis outside_Un_outside_Un sup_commute)
     with out_sub12
     have "outside(?\<Theta>1 \<union> ?\<Theta>2) = outside(?\<Theta>2 \<union> ?\<Theta>)" by blast
     then have "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = frontier(outside(?\<Theta>2 \<union> ?\<Theta>))"
@@ -548,9 +537,8 @@
     then have xnot: "x \<notin> ?\<Theta>"
       by (simp add: inside_def)
     obtain z where zim: "z \<in> ?\<Theta>1" and zout: "z \<in> outside(?\<Theta>2 \<union> ?\<Theta>)"
-      apply (auto simp: outside_inside)
-      using nonempty_simple_path_endless [OF \<open>simple_path c1\<close>]
-      by (metis Diff_Diff_Int Diff_iff ex_in_conv c1 c1c c1c2 pa1_disj_in2)
+      unfolding outside_inside
+      using nonempty_simple_path_endless [OF \<open>simple_path c1\<close>] c1 c1c c1c2 pa1_disj_in2 by auto
     obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
       using zout op_out2c open_contains_ball_eq by blast
     have "z \<in> frontier (inside (?\<Theta>1 \<union> ?\<Theta>))"
@@ -560,11 +548,8 @@
     then have w2: "w \<in> outside (?\<Theta>2 \<union> ?\<Theta>)"
       by (metis e dist_commute mem_ball subsetCE)
     then have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) z w"
-      apply (simp add: connected_component_def)
-      apply (rule_tac x = "outside(?\<Theta>2 \<union> ?\<Theta>)" in exI)
-      using zout apply (auto simp: co_out2c)
-       apply (simp_all add: outside_inside)
-      done
+      unfolding connected_component_def
+      by (metis co_out2c compl_sup inside_Un_outside sup_ge2 zout)
     moreover have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) w x"
       unfolding connected_component_def
       using pa2_disj_in1 co_in1c x w1 union_with_outside by fastforce
@@ -581,9 +566,8 @@
     then have xnot: "x \<notin> ?\<Theta>"
       by (simp add: inside_def)
     obtain z where zim: "z \<in> ?\<Theta>2" and zout: "z \<in> outside(?\<Theta>1 \<union> ?\<Theta>)"
-      apply (auto simp: outside_inside)
-      using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>]
-      by (metis (no_types, opaque_lifting) Diff_Diff_Int Diff_iff c1c2 c2 c2c ex_in_conv pa2_disj_in1)
+      unfolding outside_inside
+      using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>] c1c2 c2 c2c pa2_disj_in1 by auto
     obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)"
       using zout op_out1c open_contains_ball_eq by blast
     have "z \<in> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))"
@@ -593,11 +577,8 @@
     then have w1: "w \<in> outside (?\<Theta>1 \<union> ?\<Theta>)"
       by (metis e dist_commute mem_ball subsetCE)
     then have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) z w"
-      apply (simp add: connected_component_def)
-      apply (rule_tac x = "outside(?\<Theta>1 \<union> ?\<Theta>)" in exI)
-      using zout apply (auto simp: co_out1c)
-       apply (simp_all add: outside_inside)
-      done
+      unfolding connected_component_def
+      by (metis Compl_Un co_out1c inside_Un_outside sup_ge2 zout)
     moreover have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) w x"
       unfolding connected_component_def
       using pa1_disj_in2 co_in2c x w2 union_with_outside by fastforce
@@ -614,8 +595,8 @@
     have *: "outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
     proof (rule components_maximal)
       show out_in: "outside (?\<Theta>1 \<union> ?\<Theta>2) \<in> components (- (?\<Theta>1 \<union> ?\<Theta>2))"
-        apply (simp only: outside_in_components co_out12c)
-        by (metis bounded_empty fr_out(1) frontier_empty unbounded_outside)
+        unfolding outside_in_components co_out12c
+        using co_out12c fr_out(1) by force
       have conn_U: "connected (- (closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<union> closure (inside (?\<Theta>2 \<union> ?\<Theta>))))"
       proof (rule Janiszewski_connected, simp_all)
         show "bounded (inside (?\<Theta>1 \<union> ?\<Theta>))"
@@ -661,9 +642,10 @@
     show "inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta> - {a, b}) = inside (?\<Theta>1 \<union> ?\<Theta>2)"
       (is "?lhs = ?rhs")
     proof
-      show "?lhs \<subseteq> ?rhs"
-        apply (simp add: in_sub_in1 in_sub_in2)
+      have " path_image c - {a, b} \<subseteq> inside (path_image c1 \<union> path_image c2)"
         using c1c c2c inside_outside pi_disjoint by fastforce
+      then show "?lhs \<subseteq> ?rhs"
+        by (simp add: in_sub_in1 in_sub_in2)
       have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta>)"
         using Compl_anti_mono [OF *] by (force simp: inside_outside)
       moreover have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> -{a,b}"
diff -r 37abfe400ae6 -r b22f39c54e8c src/HOL/Analysis/Locally.thy
--- a/src/HOL/Analysis/Locally.thy	Fri Aug 04 19:17:49 2023 +0200
+++ b/src/HOL/Analysis/Locally.thy	Sun Aug 06 18:29:09 2023 +0100
@@ -44,24 +44,18 @@
 lemma open_neighbourhood_base_of:
   "(\<forall>S. P S \<longrightarrow> openin X S)
         \<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow> (\<forall>W x. openin X W \<and> x \<in> W \<longrightarrow> (\<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> W))"
-  apply (simp add: neighbourhood_base_of, safe, blast)
-  by meson
+  by (smt (verit) neighbourhood_base_of subsetD)
 
 lemma neighbourhood_base_of_open_subset:
    "\<lbrakk>neighbourhood_base_of P X; openin X S\<rbrakk>
         \<Longrightarrow> neighbourhood_base_of P (subtopology X S)"
-  apply (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt image_def)
-  apply (rename_tac x V)
-  apply (drule_tac x="S \<inter> V" in spec)
-  apply (simp add: Int_ac)
-  by (metis IntI le_infI1 openin_Int)
+  by (smt (verit, ccfv_SIG) neighbourhood_base_of openin_open_subtopology subset_trans)
 
 lemma neighbourhood_base_of_topology_base:
    "openin X = arbitrary union_of (\<lambda>W. W \<in> \<B>)
         \<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow>
              (\<forall>W x. W \<in> \<B> \<and> x \<in> W  \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W))"
-  apply (auto simp: openin_topology_base_unique neighbourhood_base_of)
-  by (meson subset_trans)
+  by (smt (verit, del_insts) neighbourhood_base_of openin_topology_base_unique subset_trans)
 
 lemma neighbourhood_base_at_unlocalized:
   assumes "\<And>S T. \<lbrakk>P S; openin X T; x \<in> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> P T"
@@ -86,9 +80,7 @@
 lemma neighbourhood_base_at_with_subset:
    "\<lbrakk>openin X U; x \<in> U\<rbrakk>
         \<Longrightarrow> (neighbourhood_base_at x P X \<longleftrightarrow> neighbourhood_base_at x (\<lambda>T. T \<subseteq> U \<and> P T) X)"
-  apply (simp add: neighbourhood_base_at_def)
-  apply (metis IntI Int_subset_iff openin_Int)
-  done
+  unfolding neighbourhood_base_at_def by (metis IntI Int_subset_iff openin_Int)
 
 lemma neighbourhood_base_of_with_subset:
    "neighbourhood_base_of P X \<longleftrightarrow> neighbourhood_base_of (\<lambda>t. t \<subseteq> topspace X \<and> P t) X"
@@ -140,9 +132,8 @@
     qed
   qed
   moreover have ?Q if ?R
-    using that
-    apply (simp add: open_neighbourhood_base_of)
-    by (metis mem_Collect_eq openin_subset path_component_of_refl path_connectedin_path_component_of path_connectedin_subtopology that topspace_subtopology_subset)
+    by (smt (verit) mem_Collect_eq open_neighbourhood_base_of openin_subset path_component_of_refl 
+        path_connectedin_path_component_of path_connectedin_subtopology that topspace_subtopology_subset)
   ultimately show "?P = ?Q" "?P = ?R"
     by blast+
 qed
@@ -154,23 +145,24 @@
 
 lemma locally_path_connected_space_open_path_components:
    "locally_path_connected_space X \<longleftrightarrow>
-        (\<forall>U c. openin X U \<and> c \<in> path_components_of(subtopology X U) \<longrightarrow> openin X c)"
-  apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def)
-  by (metis imageI inf.absorb_iff2 openin_closedin_eq)
+        (\<forall>U C. openin X U \<and> C \<in> path_components_of(subtopology X U) \<longrightarrow> openin X C)"
+  apply (simp add: locally_path_connected_space_eq_open_path_component_of path_components_of_def)
+  by (smt (verit, ccfv_threshold) Int_iff image_iff openin_subset subset_iff)
 
 lemma openin_path_component_of_locally_path_connected_space:
    "locally_path_connected_space X \<Longrightarrow> openin X (Collect (path_component_of X x))"
-  apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
-  by (metis openin_empty openin_topspace path_component_of_eq_empty subtopology_topspace)
+  using locally_path_connected_space_eq_open_path_component_of openin_subopen path_component_of_eq_empty 
+  by fastforce
 
 lemma openin_path_components_of_locally_path_connected_space:
-   "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> openin X c"
-  apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
-  by (metis (no_types, lifting) imageE openin_topspace path_components_of_def subtopology_topspace)
+   "\<lbrakk>locally_path_connected_space X; C \<in> path_components_of X\<rbrakk> \<Longrightarrow> openin X C"
+  using locally_path_connected_space_open_path_components by force
 
 lemma closedin_path_components_of_locally_path_connected_space:
-   "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> closedin X c"
-  by (simp add: closedin_def complement_path_components_of_Union openin_path_components_of_locally_path_connected_space openin_clauses(3) path_components_of_subset)
+   "\<lbrakk>locally_path_connected_space X; C \<in> path_components_of X\<rbrakk> \<Longrightarrow> closedin X C"
+  unfolding closedin_def
+  by (metis Diff_iff complement_path_components_of_Union openin_clauses(3) openin_closedin_eq 
+      openin_path_components_of_locally_path_connected_space)
 
 lemma closedin_path_component_of_locally_path_connected_space:
   assumes "locally_path_connected_space X"
@@ -193,8 +185,7 @@
          (is "?lhs = ?rhs")
 proof
   assume ?lhs then show ?rhs
-    apply (simp add: weakly_locally_path_connected_at_def neighbourhood_base_at_def)
-    by (meson order_trans subsetD)
+    by (smt (verit) neighbourhood_base_at_def subset_iff weakly_locally_path_connected_at_def)
 next
   have *: "\<exists>V. path_connectedin X V \<and> U \<subseteq> V \<and> V \<subseteq> W"
     if "(\<forall>y\<in>U. \<exists>C. path_connectedin X C \<and> C \<subseteq> W \<and> x \<in> C \<and> y \<in> C)"
@@ -218,18 +209,22 @@
       (\<forall>V x. openin X V \<and> x \<in> V
              \<longrightarrow> (\<exists>U. openin X U \<and>
                     x \<in> U \<and> U \<subseteq> V \<and>
-                    (\<forall>y \<in> U. \<exists>c. path_connectedin X c \<and>
-                                c \<subseteq> V \<and> x \<in> c \<and> y \<in> c)))"
-  apply (simp add: locally_path_connected_space_def neighbourhood_base_of_def)
-  apply (simp add: weakly_locally_path_connected_at flip: weakly_locally_path_connected_at_def)
-  using openin_subset apply force
-  done
+                    (\<forall>y \<in> U. \<exists>C. path_connectedin X C \<and>
+                                C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))"
+         (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (metis locally_path_connected_space)
+  assume ?rhs
+  then show ?lhs
+    unfolding locally_path_connected_space_def neighbourhood_base_of
+    by (metis neighbourhood_base_at_def weakly_locally_path_connected_at weakly_locally_path_connected_at_def)
+qed
 
 lemma locally_path_connected_space_open_subset:
-   "\<lbrakk>locally_path_connected_space X; openin X s\<rbrakk>
-        \<Longrightarrow> locally_path_connected_space (subtopology X s)"
-  apply (simp add: locally_path_connected_space_def neighbourhood_base_of openin_open_subtopology path_connectedin_subtopology)
-  by (meson order_trans)
+   "\<lbrakk>locally_path_connected_space X; openin X S\<rbrakk>
+        \<Longrightarrow> locally_path_connected_space (subtopology X S)"
+  by (smt (verit, best) locally_path_connected_space openin_open_subtopology path_connectedin_subtopology subset_trans)
 
 lemma locally_path_connected_space_quotient_map_image:
   assumes f: "quotient_map X Y f" and X: "locally_path_connected_space X"
@@ -247,19 +242,20 @@
     let ?T = "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)"
     show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace X. f x \<in> C}"
     proof (intro exI conjI)
-      have "\<exists>U. openin X U \<and> ?T \<in> path_components_of (subtopology X U)"
+      have *: "\<exists>U. openin X U \<and> ?T \<in> path_components_of (subtopology X U)"
       proof (intro exI conjI)
         show "openin X ({z \<in> topspace X. f z \<in> V})"
           using V f openin_subset quotient_map_def by fastforce
-        show "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)
-        \<in> path_components_of (subtopology X {z \<in> topspace X. f z \<in> V})"
-          by (metis (no_types, lifting) Int_iff \<open>f x \<in> C\<close> c mem_Collect_eq path_component_in_path_components_of path_components_of_subset topspace_subtopology topspace_subtopology_subset x)
+        have "x \<in> topspace (subtopology X {z \<in> topspace X. f z \<in> V})"
+          using \<open>f x \<in> C\<close> c path_components_of_subset x by force
+        then show "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)
+            \<in> path_components_of (subtopology X {z \<in> topspace X. f z \<in> V})"
+          by (meson path_component_in_path_components_of)
       qed
       with X show "openin X ?T"
         using locally_path_connected_space_open_path_components by blast
       show x: "x \<in> ?T"
-        using V \<open>f x \<in> C\<close> c openin_subset path_component_of_equiv path_components_of_subset topspace_subtopology topspace_subtopology_subset x
-        by fastforce
+        using * nonempty_path_components_of path_component_of_eq path_component_of_eq_empty by fastforce
       have "f ` ?T \<subseteq> C"
       proof (rule path_components_of_maximal)
         show "C \<in> path_components_of (subtopology Y V)"
@@ -285,12 +281,9 @@
 lemma homeomorphic_locally_path_connected_space:
   assumes "X homeomorphic_space Y"
   shows "locally_path_connected_space X \<longleftrightarrow> locally_path_connected_space Y"
-proof -
-  obtain f g where "homeomorphic_maps X Y f g"
-    using assms homeomorphic_space_def by fastforce
-  then show ?thesis
-    by (metis (no_types) homeomorphic_map_def homeomorphic_maps_map locally_path_connected_space_quotient_map_image)
-qed
+  using assms
+    unfolding homeomorphic_space_def homeomorphic_map_def homeomorphic_maps_map
+    by (metis locally_path_connected_space_quotient_map_image)
 
 lemma locally_path_connected_space_retraction_map_image:
    "\<lbrakk>retraction_map X Y r; locally_path_connected_space X\<rbrakk>
@@ -314,14 +307,21 @@
 
 lemma path_component_eq_connected_component_of:
   assumes "locally_path_connected_space X"
-  shows "(path_component_of_set X x = connected_component_of_set X x)"
+  shows "path_component_of_set X x = connected_component_of_set X x"
 proof (cases "x \<in> topspace X")
   case True
-  then show ?thesis
-    using connectedin_connected_component_of [of X x]
-    apply (clarsimp simp add: connectedin_def connected_space_clopen_in topspace_subtopology_subset cong: conj_cong)
-    apply (drule_tac x="path_component_of_set X x" in spec)
-    by (metis assms closedin_closed_subtopology closedin_connected_component_of closedin_path_component_of_locally_path_connected_space inf.absorb_iff2 inf.orderE openin_path_component_of_locally_path_connected_space openin_subtopology path_component_of_eq_empty path_component_subset_connected_component_of)
+  have "path_component_of_set X x \<subseteq> connected_component_of_set X x"
+    by (simp add: path_component_subset_connected_component_of)
+  moreover have "closedin X (path_component_of_set X x)"
+    by (simp add: assms closedin_path_component_of_locally_path_connected_space)
+  moreover have "openin X (path_component_of_set X x)"
+    by (simp add: assms openin_path_component_of_locally_path_connected_space)
+  moreover have "path_component_of_set X x \<noteq> {}"
+    by (meson True path_component_of_eq_empty)
+  ultimately show ?thesis
+    using connectedin_connected_component_of [of X x] unfolding connectedin_def
+    by (metis closedin_subset_topspace connected_space_clopen_in  
+        subset_openin_subtopology topspace_subtopology_subset)
 next
   case False
   then show ?thesis
@@ -356,8 +356,7 @@
     obtain U C where U: "openin (product_topology X I) U"
       and V: "path_connectedin (product_topology X I) C"
       and "z \<in> U" "U \<subseteq> C" and Csub: "C \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
-      using L apply (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of)
-      by (metis openin_topspace topspace_product_topology z)
+      by (metis L locally_path_connected_space openin_topspace topspace_product_topology z)
     then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}"
       and XV: "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (V i)" and "z \<in> Pi\<^sub>E I V" and subU: "Pi\<^sub>E I V \<subseteq> U"
       by (force simp: openin_product_topology_alt)
@@ -366,8 +365,7 @@
       have "path_connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
       proof -
         have pc: "path_connectedin (X i) ((\<lambda>x. x i) ` C)"
-          apply (rule path_connectedin_continuous_map_image [OF _ V])
-          by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>)
+          by (metis V continuous_map_product_projection path_connectedin_continuous_map_image that(1))
         moreover have "((\<lambda>x. x i) ` C) = topspace (X i)"
         proof
           show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)"
@@ -388,8 +386,7 @@
         using finite_subset by blast
     next
       show "locally_path_connected_space (X i)" if "i \<in> I" for i
-        apply (rule locally_path_connected_space_quotient_map_image [OF _ L, where f = "\<lambda>x. x i"])
-        by (metis False Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection that)
+        by (meson False L locally_path_connected_space_quotient_map_image quotient_map_product_projection that)
     qed
   qed
   moreover have ?lhs if R: ?rhs
@@ -407,20 +404,12 @@
       fix i assume "i \<in> I"
       have "locally_path_connected_space (X i)"
         by (simp add: R \<open>i \<in> I\<close>)
-      moreover have "openin (X i) (W i) " "z i \<in> W i"
+      moreover have *:"openin (X i) (W i) " "z i \<in> W i"
         using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto
       ultimately obtain U C where UC: "openin (X i) U" "path_connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i"
         using \<open>i \<in> I\<close> by (force simp: locally_path_connected_space_def neighbourhood_base_of)
       show "?\<Phi> i"
-      proof (cases "W i = topspace (X i) \<and> path_connected_space(X i)")
-        case True
-        then show ?thesis
-          using \<open>z i \<in> W i\<close> path_connectedin_topspace by blast
-      next
-        case False
-        then show ?thesis
-          by (meson UC)
-      qed
+        by (metis UC * openin_subset path_connectedin_topspace)
     qed
     then obtain U C where
       *: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i) \<and> path_connectedin (X i) (C i) \<and> z i \<in> (U i) \<and> (U i) \<subseteq> (C i) \<and> (C i) \<subseteq> W i \<and>
@@ -434,15 +423,12 @@
       by (simp add: that finW)
     ultimately have "finite {i \<in> I. U i \<noteq> topspace (X i)}"
       using finite_subset by auto
-    then have "openin (product_topology X I) (Pi\<^sub>E I U)"
-      using * by (simp add: openin_PiE_gen)
+    with * have "openin (product_topology X I) (Pi\<^sub>E I U)"
+      by (simp add: openin_PiE_gen)
     then show "\<exists>U. openin (product_topology X I) U \<and>
-            (\<exists>V. path_connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
-      apply (rule_tac x="PiE I U" in exI, simp)
-      apply (rule_tac x="PiE I C" in exI)
-      using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> *
-      apply (simp add: path_connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans)
-      done
+              (\<exists>V. path_connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
+      by (metis (no_types, opaque_lifting) subsetI \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> * path_connectedin_PiE 
+          PiE_iff PiE_mono order.trans)
   qed
   ultimately show ?thesis
     using False by blast
@@ -507,7 +493,7 @@
       show "\<exists>U V. openin (prod_topology X Y) U \<and> path_connectedin (prod_topology X Y) V \<and> (x, y) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> UV"
         apply (rule_tac x="C \<times> D" in exI)
         apply (rule_tac x="K \<times> L" in exI)
-        apply (auto simp: openin_prod_Times_iff path_connectedin_Times)
+        apply (fastforce simp: openin_prod_Times_iff path_connectedin_Times)
         done
     qed
   qed
@@ -555,10 +541,10 @@
   where "locally_connected_space X \<equiv> neighbourhood_base_of (connectedin X) X"
 
 
-lemma locally_connected_A: "(\<forall>U x. openin X U \<and> x \<in> U
-              \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))
+lemma locally_connected_A: "(\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))
        \<Longrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> connectedin X U) X"
-  by (smt (verit, best) connected_component_of_refl connectedin_connected_component_of connectedin_subtopology mem_Collect_eq neighbourhood_base_of openin_subset topspace_subtopology_subset)
+  unfolding neighbourhood_base_of
+  by (metis (full_types) connected_component_of_refl connectedin_connected_component_of connectedin_subtopology mem_Collect_eq openin_subset topspace_subtopology_subset)
 
 lemma locally_connected_B: "locally_connected_space X \<Longrightarrow> 
           (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))"
@@ -594,12 +580,12 @@
 lemma locally_connected_space_open_connected_components:
   "locally_connected_space X \<longleftrightarrow>
    (\<forall>U C. openin X U \<and> C \<in> connected_components_of(subtopology X U) \<longrightarrow> openin X C)"
-  apply (simp add: locally_connected_space_eq_open_connected_component_of connected_components_of_def)
-  by (smt (verit) imageE image_eqI inf.orderE inf_commute openin_subset)
+  unfolding connected_components_of_def locally_connected_space_eq_open_connected_component_of
+  by (smt (verit, best) image_iff openin_subset topspace_subtopology_subset)
 
 lemma openin_connected_component_of_locally_connected_space:
    "locally_connected_space X \<Longrightarrow> openin X (connected_component_of_set X x)"
-  by (metis connected_component_of_eq_empty locally_connected_space_eq_open_connected_component_of openin_empty openin_topspace subtopology_topspace)
+  by (metis connected_component_of_eq_empty locally_connected_B openin_empty openin_topspace subtopology_topspace)
 
 lemma openin_connected_components_of_locally_connected_space:
    "\<lbrakk>locally_connected_space X; C \<in> connected_components_of X\<rbrakk> \<Longrightarrow> openin X C"
@@ -651,8 +637,8 @@
 
 lemma locally_connected_space_open_subset:
    "\<lbrakk>locally_connected_space X; openin X S\<rbrakk> \<Longrightarrow> locally_connected_space (subtopology X S)"
-  apply (simp add: locally_connected_space_def)
-  by (smt (verit, ccfv_threshold) connectedin_subtopology neighbourhood_base_of openin_open_subtopology subset_trans)
+  unfolding locally_connected_space_def neighbourhood_base_of
+  by (smt (verit) connectedin_subtopology openin_open_subtopology subset_trans)
 
 lemma locally_connected_space_quotient_map_image:
   assumes X: "locally_connected_space X" and f: "quotient_map X Y f"
@@ -731,9 +717,8 @@
   by (simp add: locally_connected_at_def locally_path_connected_at_def neighbourhood_base_at_mono path_connectedin_imp_connectedin)
 
 lemma weakly_locally_path_connected_imp_weakly_locally_connected_at:
-   "weakly_locally_path_connected_at x X
-             \<Longrightarrow> weakly_locally_connected_at x X"
-  by (simp add: neighbourhood_base_at_mono path_connectedin_imp_connectedin weakly_locally_connected_at_def weakly_locally_path_connected_at_def)
+   "weakly_locally_path_connected_at x X \<Longrightarrow> weakly_locally_connected_at x X"
+  by (metis path_connectedin_imp_connectedin weakly_locally_connected_at weakly_locally_path_connected_at)
 
 
 lemma interior_of_locally_connected_subspace_component:
@@ -859,8 +844,7 @@
       have "connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
       proof -
         have pc: "connectedin (X i) ((\<lambda>x. x i) ` C)"
-          apply (rule connectedin_continuous_map_image [OF _ V])
-          by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>)
+          by (metis V connectedin_continuous_map_image continuous_map_product_projection that(1))
         moreover have "((\<lambda>x. x i) ` C) = topspace (X i)"
         proof
           show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)"
@@ -899,20 +883,12 @@
       fix i assume "i \<in> I"
       have "locally_connected_space (X i)"
         by (simp add: R \<open>i \<in> I\<close>)
-      moreover have "openin (X i) (W i) " "z i \<in> W i"
+      moreover have *: "openin (X i) (W i)" "z i \<in> W i"
         using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto
-      ultimately obtain U C where UC: "openin (X i) U" "connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i"
+      ultimately obtain U C where "openin (X i) U" "connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i"
         using \<open>i \<in> I\<close> by (force simp: locally_connected_space_def neighbourhood_base_of)
-      show "?\<Phi> i"
-      proof (cases "W i = topspace (X i) \<and> connected_space(X i)")
-        case True
-        then show ?thesis
-          using \<open>z i \<in> W i\<close> connectedin_topspace by blast
-      next
-        case False
-        then show ?thesis
-          by (meson UC)
-      qed
+      then show "?\<Phi> i"
+        by (metis * connectedin_topspace openin_subset)
     qed
     then obtain U C where
       *: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i) \<and> connectedin (X i) (C i) \<and> z i \<in> (U i) \<and> (U i) \<subseteq> (C i) \<and> (C i) \<subseteq> W i \<and>
@@ -930,11 +906,8 @@
       using * by (simp add: openin_PiE_gen)
     then show "\<exists>U. openin (product_topology X I) U \<and>
             (\<exists>V. connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
-      apply (rule_tac x="PiE I U" in exI, simp)
-      apply (rule_tac x="PiE I C" in exI)
       using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> *
-      apply (simp add: connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans)
-      done
+      by (metis (no_types, opaque_lifting) PiE_iff PiE_mono connectedin_PiE subset_iff)
   qed
   ultimately show ?thesis
     using False by blast
@@ -990,27 +963,17 @@
   shows "m \<le> n \<longrightarrow> X dim_le n"
   using assms
 proof (induction arbitrary: n rule: dimension_le.induct)
-  case (1 m X)
-  show ?case
-  proof (intro strip dimension_le.intros)
-    show "-1 \<le> n" if "m \<le> n" for n :: int using that using "1.hyps" by fastforce    
-    show "\<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and> subtopology X (X frontier_of U) dim_le n-1"
-      if "m \<le> n" and "openin X V" and "a \<in> V" for n V a
-      using that by (meson "1.IH" diff_right_mono)
-  qed
-qed
+qed (smt (verit) dimension_le.simps)
 
 inductive_simps dim_le_minus2 [simp]: "X dim_le -2"
 
 lemma dimension_le_eq_empty [simp]:
    "X dim_le -1 \<longleftrightarrow> X = trivial_topology"
 proof
-  assume L: "X dim_le (-1)"
-  show "X = trivial_topology"
-    by (force intro: dimension_le.cases [OF L])
+  show "X dim_le (-1) \<Longrightarrow> X = trivial_topology"
+    by (force intro: dimension_le.cases)
 next
-  assume "X = trivial_topology"
-  then show "X dim_le (-1)"
+  show "X = trivial_topology \<Longrightarrow> X dim_le (-1)"
     using dimension_le.simps openin_subset by fastforce
 qed
 
@@ -1144,7 +1107,8 @@
 proof (cases "n \<ge> -1")
   case True
   then show ?thesis
-    using homeomorphic_space_dimension_le_aux [of _ _ "nat(n+1)"] by (smt (verit) assms homeomorphic_space_sym nat_eq_iff)
+    using homeomorphic_space_dimension_le_aux [of _ _ "nat(n+1)"] 
+    by (smt (verit) assms homeomorphic_space_sym nat_eq_iff)
 next
   case False
   then show ?thesis