# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1755878073 -3600
# Node ID f53031c95f5190884df7f4c167809c028f366696
# Parent  b9888e947100e82b2fd38ee85c9430962337f54e
Fixed some ugly proofs

diff -r b9888e947100 -r f53031c95f51 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Fri Aug 22 16:00:54 2025 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Fri Aug 22 16:54:33 2025 +0100
@@ -346,7 +346,7 @@
       and notind: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> ?x \<bullet> i = 0)"
       using substdbasis_expansion_unique[OF assms] by blast+
     then have **: "sum u ?D = sum ((\<bullet>) ?x) ?D"
-      using assms by (auto intro!: sum.cong)
+      using assms by (meson subset_iff sum.cong)
     show "0 \<le> ?x \<bullet> i" if "i \<in> Basis" for i
       using as(1) ind notind that by fastforce
     show "sum ((\<bullet>) ?x) ?D \<le> 1"
@@ -376,24 +376,24 @@
   fix e
   assume "e > 0" and as: "ball x e \<subseteq> {x. (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i) \<and> sum ((\<bullet>) x) Basis \<le> 1}"
   show "(\<forall>i\<in>Basis. 0 < x \<bullet> i) \<and> sum ((\<bullet>) x) Basis < 1"
-  proof safe
+  proof (intro strip conjI)
     fix i :: 'a
     assume i: "i \<in> Basis"
     then show "0 < x \<bullet> i"
       using as[THEN subsetD[where c="x - (e/2) *\<^sub>R i"]] and \<open>e > 0\<close> 
       by (force simp add: inner_simps)
   next
-    have **: "dist x (x + (e/2) *\<^sub>R (SOME i. i\<in>Basis)) < e" using \<open>e > 0\<close>
+    obtain i::'a where i: "i \<in> Basis"
+      using nonempty_Basis by blast
+    have **: "dist x (x + (e/2) *\<^sub>R i) < e" using \<open>e > 0\<close>
       unfolding dist_norm
-      by (auto intro!: mult_strict_left_mono simp: SOME_Basis)
-    have "\<And>i. i \<in> Basis \<Longrightarrow> (x + (e/2) *\<^sub>R (SOME i. i\<in>Basis)) \<bullet> i =
-      x\<bullet>i + (if i = (SOME i. i\<in>Basis) then e/2 else 0)"
-      by (auto simp: SOME_Basis inner_Basis inner_simps)
-    then have *: "sum ((\<bullet>) (x + (e/2) *\<^sub>R (SOME i. i\<in>Basis))) Basis =
-      sum (\<lambda>i. x\<bullet>i + (if (SOME i. i\<in>Basis) = i then e/2 else 0)) Basis"
-      by (auto simp: intro!: sum.cong)
-    have "sum ((\<bullet>) x) Basis < sum ((\<bullet>) (x + (e/2) *\<^sub>R (SOME i. i\<in>Basis))) Basis"
-      using \<open>e > 0\<close> DIM_positive by (auto simp: SOME_Basis sum.distrib *)
+      by (auto intro!: mult_strict_left_mono simp: i)
+    have "\<And>i. i \<in> Basis \<Longrightarrow> (x + (e/2) *\<^sub>R i) \<bullet> i = x\<bullet>i + (if i = i then e/2 else 0)"
+      by (auto simp: inner_simps)
+    then have *: "sum ((\<bullet>) (x + (e/2) *\<^sub>R i)) Basis = sum (\<lambda>j. x\<bullet>j + (if j = i then e/2 else 0)) Basis"
+      using i by (auto simp: inner_Basis inner_left_distrib intro!: sum.cong)
+    have "sum ((\<bullet>) x) Basis < sum ((\<bullet>) (x + (e/2) *\<^sub>R i)) Basis"
+      using \<open>e > 0\<close> DIM_positive by (auto simp: i sum.distrib *)
     also have "\<dots> \<le> 1"
       using ** as by force
     finally show "sum ((\<bullet>) x) Basis < 1" by auto
@@ -404,7 +404,7 @@
   obtain a :: 'b where "a \<in> UNIV" using UNIV_witness ..
   let ?d = "(1 - sum ((\<bullet>) x) Basis) / real (DIM('a))"
   show "\<exists>e>0. ball x e \<subseteq> {x. (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i) \<and> sum ((\<bullet>) x) Basis \<le> 1}"
-  proof (rule_tac x="min (Min (((\<bullet>) x) ` Basis)) D" for D in exI, intro conjI subsetI CollectI)
+  proof (intro exI conjI subsetI CollectI)
     fix y
     assume y: "y \<in> ball x (min (Min ((\<bullet>) x ` Basis)) ?d)"
     have "sum ((\<bullet>) y) Basis \<le> sum (\<lambda>i. x\<bullet>i + ?d) Basis"
@@ -423,7 +423,7 @@
       by (auto simp add: Suc_le_eq)
     finally show "sum ((\<bullet>) y) Basis \<le> 1" .
     show "(\<forall>i\<in>Basis. 0 \<le> y \<bullet> i)"
-    proof safe
+    proof (intro strip)
       fix i :: 'a
       assume i: "i \<in> Basis"
       have "norm (x - y) < Min (((\<bullet>) x) ` Basis)"
@@ -469,7 +469,7 @@
         unfolding **[OF i] by (auto simp add: Suc_le_eq)
     next
       have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real DIM('a))) ?D"
-        by (auto intro: sum.cong)
+        by simp
       also have "\<dots> < 1"
         unfolding sum_constant divide_inverse[symmetric]
         by (auto simp add: field_simps)
@@ -619,7 +619,7 @@
   obtains a :: "'a::euclidean_space"
     where "a \<in> rel_interior (convex hull (insert 0 D))"
 proof -
-  let ?a = "sum (\<lambda>b::'a::euclidean_space. inverse (2 * real (card D)) *\<^sub>R b) D"
+  let ?a = "(\<Sum>b\<in>D. b /\<^sub>R (2 * real (card D)))"
   have "finite D"
     using assms finite_Basis infinite_super by blast
   then have d1: "0 < real (card D)"
@@ -627,7 +627,7 @@
   {
     fix i
     assume "i \<in> D"
-    have "?a \<bullet> i = sum (\<lambda>j. if i = j then inverse (2 * real (card D)) else 0) D"
+    have "?a \<bullet> i = (\<Sum>j\<in>D. if i = j then inverse (2 * real (card D)) else 0)"
       unfolding inner_sum_left
       using \<open>i \<in> D\<close> by (auto simp: inner_Basis subsetD[OF assms(2)] intro: sum.cong)
     also have "... = inverse (2 * real (card D))"
@@ -649,7 +649,7 @@
       finally show "0 < ?a \<bullet> i" by auto
     next
       have "sum ((\<bullet>) ?a) D = sum (\<lambda>i. inverse (2 * real (card D))) D"
-        by (rule sum.cong) (rule refl, rule **)
+        by (rule sum.cong [OF refl **]) 
       also have "\<dots> < 1"
         unfolding sum_constant divide_real_def[symmetric]
         by (auto simp add: field_simps)
@@ -5104,7 +5104,7 @@
       then have "sum u (S \<inter> T) = 1"
         using that by linarith
       moreover have "(\<Sum>v\<in>S \<inter> T. u v *\<^sub>R v) = (\<Sum>v\<in>S. u v *\<^sub>R v)"
-      by (auto simp: if_smult sum.inter_restrict intro: sum.cong)
+      by (auto simp: sum.inter_restrict intro: sum.cong)
     ultimately show ?thesis
       by force
     qed
@@ -6362,8 +6362,8 @@
     show "\<And>n. ?C n \<subseteq> S"
       by auto
     show "?C n \<subseteq> interior (?C (Suc n))" for n
-    proof (simp add: interior_diff, rule Diff_mono)
-      show "cball a (real n) \<subseteq> ball a (1 + real n)"
+    proof -
+      have \<section>: "cball a (real n) \<subseteq> ball a (1 + real n)"
         by (simp add: cball_subset_ball_iff)
       have cl: "closed (\<Union>x\<in>- S. \<Union>e\<in>cball 0 (1 / (2 + real n)). {x + e})"
         using assms by (auto intro: closed_compact_sums)
@@ -6372,8 +6372,10 @@
         by (intro closure_minimal UN_mono ball_subset_cball order_refl cl)
       also have "... \<subseteq> (\<Union>x \<in> -S. \<Union>y\<in>ball 0 (1 / (1 + real n)). {x + y})"
         by (simp add: cball_subset_ball_iff field_split_simps UN_mono)
-      finally show "closure (\<Union>x\<in>- S. \<Union>y\<in>ball 0 (1 / (2 + real n)). {x + y})
+      finally have "closure (\<Union>x\<in>- S. \<Union>y\<in>ball 0 (1 / (2 + real n)). {x + y})
                     \<subseteq> (\<Union>x \<in> -S. \<Union>y\<in>ball 0 (1 / (1 + real n)). {x + y})" .
+      with \<section> show ?thesis
+        by (auto simp: interior_diff)
     qed
     have "S \<subseteq> \<Union> (range ?C)"
     proof
@@ -6382,8 +6384,7 @@
       then obtain e where "e > 0" and e: "ball x e \<subseteq> S"
         using assms open_contains_ball by blast
       then obtain N1 where "N1 > 0" and N1: "real N1 > 1/e"
-        using reals_Archimedean2
-        by (metis divide_less_0_iff less_eq_real_def neq0_conv not_le of_nat_0 of_nat_1 of_nat_less_0_iff)
+        by (metis divide_less_0_1_iff gr0I of_nat_0 order_less_imp_triv reals_Archimedean2)
       obtain N2 where N2: "norm(x - a) \<le> real N2"
         by (meson real_arch_simple)
       have N12: "inverse((N1 + N2) + 1) \<le> inverse(N1)"
@@ -6424,11 +6425,7 @@
 lemma orthogonal_comp_anti_mono:
   assumes "A \<subseteq> B"
   shows "B\<^sup>\<bottom> \<subseteq> A\<^sup>\<bottom>"
-proof
-  fix x assume x: "x \<in> B\<^sup>\<bottom>"
-  show "x \<in> orthogonal_comp A" using x unfolding orthogonal_comp_def
-    by (simp add: orthogonal_def, metis assms in_mono)
-qed
+  using assms by (force simp add: orthogonal_comp_def orthogonal_def)
 
 lemma orthogonal_comp_null [simp]: "{0}\<^sup>\<bottom> = UNIV"
   by (auto simp: orthogonal_comp_def orthogonal_def)
@@ -6472,7 +6469,8 @@
     moreover have "?u \<in> U"
       by (metis (no_types, lifting) \<open>span B = U\<close> assms subspace_sum span_base span_mul)
     moreover have "(v - ?u) \<in> U\<^sup>\<bottom>"
-    proof (clarsimp simp: orthogonal_comp_def orthogonal_def)
+      unfolding orthogonal_comp_def orthogonal_def mem_Collect_eq
+    proof 
       fix y
       assume "y \<in> U"
       with \<open>span B = U\<close> span_finite [OF \<open>finite B\<close>]
@@ -6567,8 +6565,7 @@
     by (metis orthogonal_comp_null)
   then show "surj (adjoint f)"
     using adjoint_linear \<open>linear f\<close>
-    by (subst (asm) orthogonal_comp_self)
-      (simp add: adjoint_linear linear_subspace_image)
+    by (metis linear_subspace_image orthogonal_comp_self subspace_UNIV)
 qed
 
 lemma inj_adjoint_iff_surj [simp]: