# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1744494152 -3600
# Node ID d35d355f733042bbe4383417a657e134bc4c4ffe
# Parent  b52e57ed7e29ad0a1dcadb53ebbdb408cd15a06f
Tidied more messy old proofs

diff -r b52e57ed7e29 -r d35d355f7330 src/HOL/Analysis/Inner_Product.thy
--- a/src/HOL/Analysis/Inner_Product.thy	Fri Apr 11 22:17:06 2025 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy	Sat Apr 12 22:42:32 2025 +0100
@@ -87,6 +87,9 @@
 lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
   by (simp add: norm_eq_sqrt_inner)
 
+lemma dot_square_norm: "inner x x = (norm x)\<^sup>2"
+  by (metis power2_norm_eq_inner) 
+
 text \<open>Identities involving real multiplication and division.\<close>
 
 lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
@@ -143,15 +146,15 @@
   show "norm x = 0 \<longleftrightarrow> x = 0"
     unfolding norm_eq_sqrt_inner by simp
   show "norm (x + y) \<le> norm x + norm y"
-    proof (rule power2_le_imp_le)
-      have "inner x y \<le> norm x * norm y"
-        by (rule norm_cauchy_schwarz)
-      thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
-        unfolding power2_sum power2_norm_eq_inner
-        by (simp add: inner_add inner_commute)
-      show "0 \<le> norm x + norm y"
-        unfolding norm_eq_sqrt_inner by simp
-    qed
+  proof (rule power2_le_imp_le)
+    have "inner x y \<le> norm x * norm y"
+      by (rule norm_cauchy_schwarz)
+    thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
+      unfolding power2_sum power2_norm_eq_inner
+      by (simp add: inner_add inner_commute)
+    show "0 \<le> norm x + norm y"
+      unfolding norm_eq_sqrt_inner by simp
+  qed
   have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
     by (simp add: real_sqrt_mult)
   then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
@@ -184,9 +187,7 @@
   by (simp add: norm_eq_sqrt_inner)
 
 lemma norm_eq: "norm x = norm y \<longleftrightarrow> inner x x = inner y y"
-  apply (subst order_eq_iff)
-  apply (auto simp: norm_le)
-  done
+  by (simp add: norm_eq_sqrt_inner)
 
 lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> inner x x = 1"
   by (simp add: norm_eq_sqrt_inner)
@@ -231,10 +232,7 @@
   show "inner x (scaleR r y) = scaleR r (inner x y)"
     unfolding real_scaleR_def by (rule inner_scaleR_right)
   show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
-  proof
-    show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
-      by (simp add: Cauchy_Schwarz_ineq2)
-  qed
+    by (metis Cauchy_Schwarz_ineq2 mult.commute mult_1 real_norm_def)
 qed
 
 lemmas tendsto_inner [tendsto_intros] =
@@ -337,7 +335,6 @@
 lemma complex_inner_i_right [simp]: "inner x \<i> = Im x"
   unfolding inner_complex_def by simp
 
-
 lemma dot_square_norm: "inner x x = (norm x)\<^sup>2"
   by (simp only: power2_norm_eq_inner) (* TODO: move? *)
 
@@ -345,16 +342,10 @@
   by (auto simp add: norm_eq_sqrt_inner)
 
 lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> inner x x \<le> a\<^sup>2"
-  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
-  using norm_ge_zero[of x]
-  apply arith
-  done
+  by (metis norm_eq_sqrt_inner norm_ge_zero order_trans real_le_lsqrt sqrt_le_D)
 
 lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> inner x x \<ge> a\<^sup>2"
-  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
-  using norm_ge_zero[of x]
-  apply arith
-  done
+  by (metis nle_le norm_eq_square norm_le_square)
 
 lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> inner x x < a\<^sup>2"
   by (metis not_le norm_ge_square)
@@ -368,11 +359,10 @@
   inner_scaleR_left inner_scaleR_right
 
 lemma dot_norm: "inner x y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
-  by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
+  by (auto simp: power2_norm_eq_inner inner_simps inner_commute) 
 
 lemma dot_norm_neg: "inner x y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
-  by (simp only: power2_norm_eq_inner inner_simps inner_commute)
-    (auto simp add: algebra_simps)
+  by (auto simp: power2_norm_eq_inner inner_simps inner_commute)
 
 lemma of_real_inner_1 [simp]: 
   "inner (of_real x) (1 :: 'a :: {real_inner, real_normed_algebra_1}) = x"
@@ -403,9 +393,7 @@
     "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
      \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
   unfolding gderiv_def has_field_derivative_def
-  apply (drule (1) has_derivative_compose)
-  apply (simp add: ac_simps)
-  done
+  using has_derivative_compose by fastforce
 
 lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   by simp
@@ -434,11 +422,7 @@
     "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
      \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
       :> (scaleR (f x) dg + scaleR df (g x))"
-  unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
-  apply (rule has_derivative_subst)
-  apply (erule (1) has_derivative_scaleR)
-  apply (simp add: ac_simps)
-  done
+  by (simp add: DERIV_mult')
 
 lemma GDERIV_mult:
     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
diff -r b52e57ed7e29 -r d35d355f7330 src/HOL/Analysis/L2_Norm.thy
--- a/src/HOL/Analysis/L2_Norm.thy	Fri Apr 11 22:17:06 2025 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy	Sat Apr 12 22:42:32 2025 +0100
@@ -66,11 +66,8 @@
 
 lemma L2_set_left_distrib:
   "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A"
-  unfolding L2_set_def
-  apply (simp add: power_mult_distrib)
-  apply (simp add: sum_distrib_right [symmetric])
-  apply (simp add: real_sqrt_mult sum_nonneg)
-  done
+  unfolding L2_set_def power_mult_distrib
+  by (simp add: real_sqrt_mult sum_nonneg flip: sum_distrib_right)
 
 lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
   unfolding L2_set_def
@@ -101,44 +98,36 @@
   qed
 qed
 
-lemma L2_set_le_sum [rule_format]:
-  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
-  apply (cases "finite A")
-  apply (induct set: finite)
-  apply simp
-  apply clarsimp
-  apply (erule order_trans [OF sqrt_sum_squares_le_sum])
-  apply simp
-  apply simp
-  apply simp
-  done
+lemma L2_set_le_sum:
+  "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> L2_set f A \<le> sum f A"
+proof (induction A rule: infinite_finite_induct)
+  case (insert a A)
+  with order_trans [OF sqrt_sum_squares_le_sum] show ?case by force
+qed auto
 
 lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
-  apply (cases "finite A")
-  apply (induct set: finite)
-  apply simp
-  apply simp
-  apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
-  apply simp
-  apply simp
-  done
+proof (induction A rule: infinite_finite_induct)
+  case (insert a A)
+  with order_trans [OF sqrt_sum_squares_le_sum_abs] show ?case by force
+qed auto
 
 lemma L2_set_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> L2_set f A * L2_set g A"
-  apply (cases "finite A")
-  apply (induct set: finite)
-  apply simp
-  apply (rule power2_le_imp_le, simp)
-  apply (rule order_trans)
-  apply (rule power_mono)
-  apply (erule add_left_mono)
-  apply (simp add: sum_nonneg)
-  apply (simp add: power2_sum)
-  apply (simp add: power_mult_distrib)
-  apply (simp add: distrib_left distrib_right)
-  apply (rule ord_le_eq_trans)
-  apply (rule L2_set_mult_ineq_lemma)
-  apply simp_all
-  done
+proof (induction A rule: infinite_finite_induct)
+  case (insert a A)
+  have "(\<bar>f a\<bar> * \<bar>g a\<bar> + (\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>))\<^sup>2
+      \<le> (\<bar>f a\<bar> * \<bar>g a\<bar> + L2_set f A * L2_set g A)\<^sup>2"
+    by (simp add: insert.IH sum_nonneg)
+  also have "... \<le> ((f a)\<^sup>2 + (L2_set f A)\<^sup>2) * ((g a)\<^sup>2 + (L2_set g A)\<^sup>2)"
+    using L2_set_mult_ineq_lemma [of "L2_set f A" "L2_set g A" "\<bar>f a\<bar>" "\<bar>g a\<bar>"]
+    by (simp add: power2_eq_square algebra_simps)
+  also have "... = (sqrt ((f a)\<^sup>2 + (L2_set f A)\<^sup>2) * sqrt ((g a)\<^sup>2 + (L2_set g A)\<^sup>2))\<^sup>2"
+    using real_sqrt_mult real_sqrt_sum_squares_mult_squared_eq by presburger
+  finally have "(\<bar>f a\<bar> * \<bar>g a\<bar> + (\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>))\<^sup>2
+              \<le> (sqrt ((f a)\<^sup>2 + (L2_set f A)\<^sup>2) * sqrt ((g a)\<^sup>2 + (L2_set g A)\<^sup>2))\<^sup>2" .
+  then
+  show ?case
+    using power2_le_imp_le insert.hyps by fastforce
+qed auto
 
 lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A"
   unfolding L2_set_def
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>