diff -r b52e57ed7e29 -r d35d355f7330 src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Fri Apr 11 22:17:06 2025 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy	Sat Apr 12 22:42:32 2025 +0100
@@ -90,10 +90,7 @@
 end
 
 lemma module_prod_scale_eq_scaleR: "module_prod.scale (*\<^sub>R) (*\<^sub>R) = scaleR"
-  apply (rule ext) apply (rule ext)
-  apply (subst module_prod.scale_def)
-  subgoal by unfold_locales
-  by (simp add: scaleR_prod_def)
+  using module_pair_axioms module_prod.scale_def module_prod_def by fastforce
 
 interpretation real_vector?: vector_space_prod "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector"
   rewrites "scale = ((*\<^sub>R)::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
@@ -166,8 +163,8 @@
       then have \<open>\<forall>\<^sub>F ((x'1, y1), (x'2, y2)) in uniformity \<times>\<^sub>F uniformity. (x'1,x'2) = x \<longrightarrow> (y1,y2) \<in> U\<close>
         by (simp add: uniformity_prod_def eventually_filtermap case_prod_unfold)
       then obtain UA UB where \<open>eventually UA uniformity\<close> and \<open>eventually UB uniformity\<close>
-               and UA_UB_U: \<open>UA (a1, a2) \<Longrightarrow> UB (b1, b2) \<Longrightarrow> (a1, b1) = x \<Longrightarrow> (a2, b2) \<in> U\<close> for a1 a2 b1 b2
-        apply atomize_elim by (simp add: case_prod_beta eventually_prod_filter)
+           and UA_UB_U: \<open>UA (a1, a2) \<Longrightarrow> UB (b1, b2) \<Longrightarrow> (a1, b1) = x \<Longrightarrow> (a2, b2) \<in> U\<close> for a1 a2 b1 b2
+         by (force simp: case_prod_beta eventually_prod_filter)
       have \<open>eventually (\<lambda>a. UA (fst x, a)) (nhds (fst x))\<close>
         using \<open>eventually UA uniformity\<close> eventually_mono eventually_nhds_uniformity by fastforce
       then obtain A where \<open>open A\<close> and A_UA: \<open>A \<subseteq> {a. UA (fst x, a)}\<close> and \<open>fst x \<in> A\<close>
@@ -190,11 +187,13 @@
     by (metis surj_pair uniformity_refl)
 next
   show \<open>eventually E uniformity \<Longrightarrow> \<forall>\<^sub>F (x::'a\<times>'b, y) in uniformity. E (y, x)\<close> for E
-    apply (simp only: uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter)
-    apply (erule exE, erule exE, rename_tac Pf Pg)
-    apply (rule_tac x=\<open>\<lambda>(x,y). Pf (y,x)\<close> in exI)
-    apply (rule_tac x=\<open>\<lambda>(x,y). Pg (y,x)\<close> in exI)
-    by (auto simp add: uniformity_sym)
+    unfolding uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter
+    apply clarify
+    subgoal for Pf Pg
+      apply (rule_tac x=\<open>\<lambda>(x,y). Pf (y,x)\<close> in exI)
+      apply (rule_tac x=\<open>\<lambda>(x,y). Pg (y,x)\<close> in exI)
+      by (auto simp add: uniformity_sym)
+    done
 next
   show \<open>\<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x::'a\<times>'b, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))\<close> 
     if \<open>eventually E uniformity\<close> for E
@@ -224,11 +223,11 @@
 proof -
   have *: "eventually P (filtercomap (\<lambda>y. (x, y)) F) \<longleftrightarrow>
            eventually (\<lambda>z. fst z = x \<longrightarrow> P (snd z)) F" for P :: "'a \<Rightarrow> bool" and F
-    unfolding eventually_filtercomap  
-    by (smt (verit) eventually_elim2 fst_conv prod.collapse snd_conv)
+    unfolding eventually_filtercomap
+    by (smt (verit, best) eventually_mono split_pairs2)  
   thus ?thesis
-    unfolding filter_eq_iff
-    by (subst *) (auto simp: eventually_nhds_uniformity case_prod_unfold)
+    unfolding filter_eq_iff *
+    by (auto simp: eventually_nhds_uniformity case_prod_unfold)
 qed
 
 lemma uniformity_of_uniform_continuous_invariant:
@@ -356,8 +355,7 @@
     have 1: \<open>\<exists>e\<in>{0<..}.
               {(x,y). dist x y < e} \<subseteq> {(x,y). dist x y < a} \<and>
               {(x,y). dist x y < e} \<subseteq> {(x,y). dist x y < b}\<close> if \<open>a>0\<close> \<open>b>0\<close> for a b
-      apply (rule bexI[of _ \<open>min a b\<close>])
-      using that by auto
+      using that by (auto intro: bexI[of _ \<open>min a b\<close>])
     have 2: \<open>mono (\<lambda>P. eventually (\<lambda>x. P (Q x)) F)\<close> for F :: \<open>'z filter\<close> and Q :: \<open>'z \<Rightarrow> 'y\<close>
       unfolding mono_def using eventually_mono le_funD by fastforce
     have \<open>\<forall>\<^sub>F ((x1::'a,y1),(x2::'b,y2)) in uniformity \<times>\<^sub>F uniformity. dist x1 y1 < e/2 \<and> dist x2 y2 < e/2\<close> if \<open>e>0\<close> for e
@@ -383,17 +381,18 @@
     have \<open>e > 0\<close>
       using \<open>0 < e1\<close> \<open>0 < e2\<close> e_def by auto
     have \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> dist x1 y1 < e1\<close> for x1 y1 :: 'a and x2 y2 :: 'b
-      unfolding dist_prod_def e_def apply auto
-      by (smt (verit, best) real_sqrt_sum_squares_ge1)
+      unfolding dist_prod_def e_def
+      by (metis real_sqrt_sum_squares_ge1 fst_conv min_less_iff_conj order_le_less_trans snd_conv)
     moreover have \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> dist x2 y2 < e2\<close> for x1 y1 :: 'a and x2 y2 :: 'b
-      unfolding dist_prod_def e_def apply auto
-      by (smt (verit, best) real_sqrt_sum_squares_ge1)
+      unfolding dist_prod_def e_def
+      using real_sqrt_sum_squares_ge1 [of "dist x1 y1" "dist x2 y2"]
+      by (metis min_less_iff_conj order_le_less_trans real_sqrt_sum_squares_ge2 snd_conv)
     ultimately have *: \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> P ((x1, x2), (y1, y2))\<close> for x1 y1 x2 y2
       using e1P1 e2P2 P1P2P by auto
 
     show \<open>eventually P (INF e\<in>{0<..}. principal {(x, y). dist x y < e})\<close>
-       apply (rule eventually_INF1[where i=e])
-      using \<open>e > 0\<close> * by (auto simp: eventually_principal)
+      using \<open>e > 0\<close> * 
+      by (auto simp: eventually_principal intro: eventually_INF1)
   qed
 qed
 end
@@ -421,8 +420,8 @@
   fix x y z :: "'a \<times> 'b"
   show "dist x y \<le> dist x z + dist y z"
     unfolding dist_prod_def
-    by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]
-        real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist)
+    by (meson add_mono dist_triangle2 order_trans power_mono real_sqrt_le_iff
+        real_sqrt_sum_squares_triangle_ineq zero_le_dist)
 next
   fix S :: "('a \<times> 'b) set"
   have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
@@ -525,8 +524,8 @@
     by auto
   show \<open>\<exists>d>0. \<forall>x\<in>S\<times>T. \<forall>y\<in>S\<times>T. dist y x < d \<longrightarrow> dist (f y) (f x) < e\<close>
     apply (rule exI[of _ d])
-    using \<open>d>0\<close> d[rule_format] apply auto
-    by (smt (verit, del_insts) dist_fst_le dist_snd_le fst_conv snd_conv)
+    by (metis SigmaE \<open>0 < d\<close> d dist_fst_le dist_snd_le fst_eqD order_le_less_trans
+        snd_conv)
 next
   fix e :: real 
   assume \<open>e > 0\<close> and \<open>\<forall>e>0. \<exists>d>0. \<forall>x\<in>S\<times>T. \<forall>x'\<in>S\<times>T. dist x' x < d \<longrightarrow> dist (f x') (f x) < e\<close>
@@ -559,8 +558,9 @@
   fix e :: real assume \<open>0 < e\<close>
   show \<open>\<exists>d>0. \<forall>x y :: 'a. dist x y < d \<longrightarrow> (\<forall>x' y'. dist x' y' < d \<longrightarrow> dist (x + x') (y + y') < e)\<close>
     apply (rule exI[of _ \<open>e/2\<close>])
-    using \<open>0 < e\<close> apply auto
-    by (smt (verit, ccfv_SIG) dist_add_cancel dist_add_cancel2 dist_commute dist_triangle_lt)
+    using \<open>0 < e\<close>
+    by (smt (verit) dist_add_cancel dist_add_cancel2 dist_commute 
+        dist_triangle_lt field_sum_of_halves)
 qed
 
 subsection \<open>Product is a Complete Metric Space\<close>
@@ -607,10 +607,7 @@
     done
   show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
     unfolding norm_prod_def
-    apply (simp add: power_mult_distrib)
-    apply (simp add: distrib_left [symmetric])
-    apply (simp add: real_sqrt_mult)
-    done
+    by (simp add: power_mult_distrib real_sqrt_mult flip: distrib_left)
   show "sgn x = scaleR (inverse (norm x)) x"
     by (rule sgn_prod_def)
   show "dist x y = norm (x - y)"
@@ -654,13 +651,10 @@
     using f.pos_bounded by fast
   obtain Kg where "0 < Kg" and norm_g: "\<And>x. norm (g x) \<le> norm x * Kg"
     using g.pos_bounded by fast
-  have "\<forall>x. norm (f x, g x) \<le> norm x * (Kf + Kg)"
-    apply (rule allI)
-    apply (simp add: norm_Pair)
-    apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp)
-    apply (simp add: distrib_left)
-    apply (rule add_mono [OF norm_f norm_g])
-    done
+  have "\<And>x. sqrt ((norm (f x))\<^sup>2) + sqrt ((norm (g x))\<^sup>2) \<le> norm x * (Kf + Kg)"
+    by (simp add: add_mono distrib_left norm_f norm_g)
+  then have "\<forall>x. norm (f x, g x) \<le> norm x * (Kf + Kg)"
+    by (smt (verit) norm_ge_zero norm_prod_def prod.sel sqrt_add_le_add_sqrt zero_le_power)
   then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
 qed
 
@@ -730,44 +724,50 @@
   by (metis norm_ge_zero sqrt_sum_squares_le_sum)
 
 lemma (in vector_space_prod) span_Times_sing1: "p.span ({0} \<times> B) = {0} \<times> vs2.span B"
-  apply (rule p.span_unique)
-  subgoal by (auto intro!: vs1.span_base vs2.span_base)
-  subgoal using vs1.subspace_single_0 vs2.subspace_span by (rule subspace_Times)
-  subgoal for T
-  proof safe
+proof (rule p.span_unique)
+  show "{0} \<times> B \<subseteq> {0} \<times> vs2.span B"
+    by (auto intro!: vs1.span_base vs2.span_base)
+  show "p.subspace ({0} \<times> vs2.span B)"
+    using vs1.subspace_single_0 vs2.subspace_span by (rule subspace_Times)
+  fix T :: "('b \<times> 'c) set"
+  assume subset_T: "{0} \<times> B \<subseteq> T" and subspace: "p.subspace T" 
+  show "{0} \<times> vs2.span B \<subseteq> T"
+  proof clarify
     fix b
-    assume subset_T: "{0} \<times> B \<subseteq> T" and subspace: "p.subspace T" and b_span: "b \<in> vs2.span B"
+    assume b_span: "b \<in> vs2.span B"
     then obtain t r where b: "b = (\<Sum>a\<in>t. r a *b a)" and t: "finite t" "t \<subseteq> B"
       by (auto simp: vs2.span_explicit)
     have "(0, b) = (\<Sum>b\<in>t. scale (r b) (0, b))"
-      unfolding b scale_prod sum_prod
-      by simp
+      unfolding b scale_prod sum_prod by simp
     also have "\<dots> \<in> T"
       using \<open>t \<subseteq> B\<close> subset_T
       by (auto intro!: p.subspace_sum p.subspace_scale subspace)
     finally show "(0, b) \<in> T" .
   qed
-  done
+qed
 
 lemma (in vector_space_prod) span_Times_sing2: "p.span (A \<times> {0}) = vs1.span A \<times> {0}"
-  apply (rule p.span_unique)
-  subgoal by (auto intro!: vs1.span_base vs2.span_base)
-  subgoal using vs1.subspace_span vs2.subspace_single_0 by (rule subspace_Times)
-  subgoal for T
-  proof safe
+proof (rule p.span_unique)
+  show "A \<times> {0} \<subseteq> vs1.span A \<times> {0}"
+    by (auto intro!: vs1.span_base vs2.span_base)
+  show "p.subspace (vs1.span A \<times> {0})"
+    using vs1.subspace_span vs2.subspace_single_0 by (rule subspace_Times)
+  fix T :: "('b \<times> 'c) set"
+  assume subset_T: "A \<times> {0} \<subseteq> T" and subspace: "p.subspace T"
+  show "vs1.span A \<times> {0} \<subseteq> T"
+  proof clarify
     fix a
-    assume subset_T: "A \<times> {0} \<subseteq> T" and subspace: "p.subspace T" and a_span: "a \<in> vs1.span A"
+    assume a_span: "a \<in> vs1.span A"
     then obtain t r where a: "a = (\<Sum>a\<in>t. r a *a a)" and t: "finite t" "t \<subseteq> A"
       by (auto simp: vs1.span_explicit)
     have "(a, 0) = (\<Sum>a\<in>t. scale (r a) (a, 0))"
-      unfolding a scale_prod sum_prod
-      by simp
+      unfolding a scale_prod sum_prod by simp
     also have "\<dots> \<in> T"
       using \<open>t \<subseteq> A\<close> subset_T
       by (auto intro!: p.subspace_sum p.subspace_scale subspace)
     finally show "(a, 0) \<in> T" .
   qed
-  done
+qed
 
 subsection \<open>Product is Finite Dimensional\<close>