# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1626186353 -3600
# Node ID a5212df98387121b228efbeb91cd153d1032f6d2
# Parent  8d93f9ca6518a48c2bc1ed5f5d090893fcd2fb1e
simplified a few proofs

diff -r 8d93f9ca6518 -r a5212df98387 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Tue Jul 13 10:57:15 2021 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Tue Jul 13 15:25:53 2021 +0100
@@ -334,13 +334,7 @@
   fix K :: "('a ^ 'b) set set"
   assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
     unfolding open_vec_def
-    apply clarify
-    apply (drule (1) bspec)
-    apply (drule (1) bspec)
-    apply clarify
-    apply (rule_tac x=A in exI)
-    apply fast
-    done
+    by (metis Union_iff)
 qed
 
 end
@@ -612,9 +606,7 @@
   by (rule L2_set_mono) (auto simp: assms)
 
 lemma component_le_norm_cart: "\<bar>x$i\<bar> \<le> norm x"
-  apply (simp add: norm_vec_def)
-  apply (rule member_le_L2_set, simp_all)
-  done
+  by (metis norm_nth_le real_norm_def)
 
 lemma norm_bound_component_le_cart: "norm x \<le> e ==> \<bar>x$i\<bar> \<le> e"
   by (metis component_le_norm_cart order_trans)
@@ -626,11 +618,10 @@
   by (simp add: norm_vec_def L2_set_le_sum)
 
 lemma bounded_linear_vec_nth[intro]: "bounded_linear (\<lambda>x. x $ i)"
-apply standard
-apply (rule vector_add_component)
-apply (rule vector_scaleR_component)
-apply (rule_tac x="1" in exI, simp add: norm_nth_le)
-done
+proof
+  show "\<exists>K. \<forall>x. norm (x $ i) \<le> norm x * K"
+    by (metis mult.commute mult.left_neutral norm_nth_le)
+qed auto
 
 instance vec :: (banach, finite) banach ..
 
@@ -681,13 +672,7 @@
 
 lemma inner_axis_axis:
   "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)"
-  unfolding inner_vec_def
-  apply (cases "i = j")
-  apply clarsimp
-  apply (subst sum.remove [of _ j], simp_all)
-  apply (rule sum.neutral, simp add: axis_def)
-  apply (rule sum.neutral, simp add: axis_def)
-  done
+  by (simp add: inner_vec_def axis_def sum.neutral sum.remove [of _ j])
 
 lemma inner_axis: "inner x (axis i y) = inner (x $ i) y"
   by (simp add: inner_vec_def axis_def sum.remove [where x=i])
@@ -987,7 +972,6 @@
 
 lemma linear_vec [simp]: "linear vec"
   using Vector_Spaces_linear_vec
-  apply (auto )
   by unfold_locales (vector algebra_simps)+
 
 subsection \<open>Matrix operations\<close>
@@ -1033,20 +1017,14 @@
 lemma matrix_mul_lid [simp]:
   fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
   shows "mat 1 ** A = A"
-  apply (simp add: matrix_matrix_mult_def mat_def)
-  apply vector
-  apply (auto simp only: if_distrib if_distribR sum.delta'[OF finite]
-    mult_1_left mult_zero_left if_True UNIV_I)
-  done
+  unfolding matrix_matrix_mult_def mat_def
+  by (auto simp: if_distrib if_distribR sum.delta'[OF finite] cong: if_cong)
 
 lemma matrix_mul_rid [simp]:
   fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
   shows "A ** mat 1 = A"
-  apply (simp add: matrix_matrix_mult_def mat_def)
-  apply vector
-  apply (auto simp only: if_distrib if_distribR sum.delta[OF finite]
-    mult_1_right mult_zero_right if_True UNIV_I cong: if_cong)
-  done
+  unfolding matrix_matrix_mult_def mat_def
+  by (auto simp: if_distrib if_distribR sum.delta'[OF finite] cong: if_cong)
 
 proposition matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
   apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
@@ -1090,16 +1068,18 @@
 
 lemma matrix_eq:
   fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
-  shows "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
-  apply auto
-  apply (subst vec_eq_iff)
-  apply clarify
-  apply (clarsimp simp add: matrix_vector_mult_def if_distrib if_distribR vec_eq_iff cong del: if_weak_cong)
-  apply (erule_tac x="axis ia 1" in allE)
-  apply (erule_tac x="i" in allE)
-  apply (auto simp add: if_distrib if_distribR axis_def
-    sum.delta[OF finite] cong del: if_weak_cong)
-  done
+  shows "A = B \<longleftrightarrow> (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?rhs
+  then show ?lhs
+    apply (subst vec_eq_iff)
+    apply (clarsimp simp add: matrix_vector_mult_def if_distrib if_distribR vec_eq_iff cong: if_cong)
+    apply (erule_tac x="axis ia 1" in allE)
+    apply (erule_tac x="i" in allE)
+    apply (auto simp add: if_distrib if_distribR axis_def
+        sum.delta[OF finite] cong del: if_weak_cong)
+    done
+qed auto
 
 lemma matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x"
   by (simp add: matrix_vector_mult_def inner_vec_def)