# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1712912312 -3600
# Node ID 0f9cd1a5edbea65b1b98c87d2311e0c26e22f9eb
# Parent  646cd337bb0836adff89d429c110d5c39aedd9f1
Tidying ugly proofs

diff -r 646cd337bb08 -r 0f9cd1a5edbe src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Apr 10 11:32:48 2024 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Apr 12 09:58:32 2024 +0100
@@ -36,11 +36,19 @@
   by (metis path_connected_continuous_image retract_of_def retraction)
 
 lemma retract_of_simply_connected:
-  "\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
-  apply (simp add: retract_of_def retraction_def Pi_iff, clarify)
-  apply (rule simply_connected_retraction_gen)
-       apply (force elim!: continuous_on_subset)+
-  done
+  assumes T: "simply_connected T" and "S retract_of T"
+  shows "simply_connected S"
+proof -
+  obtain r where r: "retraction T S r"
+    using assms by (metis retract_of_def) 
+  have "S \<subseteq> T"
+    by (meson \<open>retraction T S r\<close> retraction)
+  then have "(\<lambda>a. a) \<in> S \<rightarrow> T"
+    by blast
+  then show ?thesis
+    using simply_connected_retraction_gen [OF T]
+    by (metis (no_types) r retraction retraction_refl)
+qed
 
 lemma retract_of_homotopically_trivial:
   assumes ts: "T retract_of S"
@@ -56,10 +64,7 @@
   then obtain k where "Retracts S r T k"
     unfolding Retracts_def using continuous_on_id by blast
   then show ?thesis
-    apply (rule Retracts.homotopically_trivial_retraction_gen)
-    using assms
-    apply (force simp: hom)+
-    done
+    by (rule Retracts.homotopically_trivial_retraction_gen) (use assms hom in force)+
 qed
 
 lemma retract_of_homotopically_trivial_null:
@@ -74,9 +79,11 @@
   then obtain k where "Retracts S r T k"
     unfolding Retracts_def by fastforce
   then show ?thesis
-    apply (rule Retracts.homotopically_trivial_retraction_null_gen)
-    apply (rule TrueI refl assms that | assumption)+
-    done
+  proof (rule Retracts.homotopically_trivial_retraction_null_gen)
+    show "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S\<rbrakk>
+         \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>a. True) U S f (\<lambda>x. c)"
+      using hom by blast
+  qed (use assms that in auto)
 qed
 
 lemma retraction_openin_vimage_iff:
@@ -101,13 +108,13 @@
   assumes "locally connected T" "S retract_of T"
   shows "locally connected S"
   using assms
-  by (metis Abstract_Topology_2.retraction_openin_vimage_iff idempotent_imp_retraction locally_connected_quotient_image retract_ofE)
+  by (metis retraction_openin_vimage_iff idempotent_imp_retraction locally_connected_quotient_image retract_ofE)
 
 lemma retract_of_locally_path_connected:
   assumes "locally path_connected T" "S retract_of T"
   shows "locally path_connected S"
   using assms
-  by (metis Abstract_Topology_2.retraction_openin_vimage_iff idempotent_imp_retraction locally_path_connected_quotient_image retract_ofE)
+  by (metis retraction_openin_vimage_iff idempotent_imp_retraction locally_path_connected_quotient_image retract_ofE)
 
 text \<open>A few simple lemmas about deformation retracts\<close>
 
@@ -137,15 +144,16 @@
   then show ?rhs
     by (auto simp: retract_of_def retraction_def)
 next
-  assume ?rhs
-  then show ?lhs
-    apply (clarsimp simp add: retract_of_def retraction_def)
-    apply (rule_tac x=r in exI, simp)
-     apply (rule homotopic_with_trans, assumption)
-     apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
-        apply (rule_tac Y=S in homotopic_with_compose_continuous_left)
+  assume R: ?rhs
+  have "\<And>r f. \<lbrakk>T \<subseteq> S; continuous_on S r; homotopic_with_canon (\<lambda>x. True) S S id f;
+            f \<in> S \<rightarrow> T; r \<in> S \<rightarrow> T; \<forall>x\<in>T. r x = x\<rbrakk>
+           \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S S f r"
+    apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
+       apply (rule_tac Y=S in homotopic_with_compose_continuous_left)
          apply (auto simp: homotopic_with_sym Pi_iff)
     done
+  with R homotopic_with_trans show ?lhs
+    unfolding retract_of_def retraction_def by blast
 qed
 
 lemma deformation_retract_of_contractible_sing:
@@ -959,7 +967,7 @@
       qed }
     with ks_f' eq \<open>a \<noteq> f' n\<close> \<open>n \<noteq> 0\<close> show ?thesis
       apply (intro ex1I[of _ "f' ` {.. n}"])
-      apply auto []
+       apply auto []
       apply metis
       done
   next
@@ -1523,7 +1531,7 @@
              (\<forall>x i. P x \<and> Q i \<and> l x i = 1 \<longrightarrow> f x i \<le> x i)"
   unfolding all_conj_distrib [symmetric] 
   apply (subst choice_iff[symmetric])+
-  by (metis assms bot_nat_0.extremum nle_le zero_neq_one)
+  by (metis assms choice_iff bot_nat_0.extremum nle_le zero_neq_one)
 
 subsection \<open>Brouwer's fixed point theorem\<close>
 
@@ -1543,10 +1551,8 @@
     by auto
   obtain d where
       d: "d > 0" "\<And>x. x \<in> cbox 0 One \<Longrightarrow> d \<le> norm (f x - x)"
-    apply (rule brouwer_compactness_lemma[OF compact_cbox _ *])
-    apply (rule continuous_intros assms)+
-    apply blast
-    done
+    using brouwer_compactness_lemma[OF compact_cbox _ *] assms
+    by (metis (no_types, lifting) continuous_on_cong continuous_on_diff continuous_on_id)
   have *: "\<forall>x. x \<in> cbox 0 One \<longrightarrow> f x \<in> cbox 0 One"
     "\<forall>x. x \<in> (cbox 0 One::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
     using assms(2)[unfolded image_subset_iff Ball_def]
@@ -1581,8 +1587,7 @@
       case False
       then show ?thesis
         using label [OF \<open>i \<in> Basis\<close>] i(1) x y
-        apply (auto simp: inner_diff_left le_Suc_eq)
-        by (metis "*")
+        by (smt (verit, ccfv_threshold) inner_diff_left less_one order_le_less)
     qed
     also have "\<dots> \<le> norm (f y - f x) + norm (y - x)"
       by (simp add: add_mono i(2) norm_bound_Basis_le)
@@ -1980,9 +1985,8 @@
   then obtain a where "a \<in> S" "a \<notin> T" by blast
   define g where "g \<equiv> \<lambda>z. if z \<in> closure S then f z else z"
   have "continuous_on (closure S \<union> closure(-S)) g"
-    unfolding g_def
-    apply (rule continuous_on_cases)
-    using fros fid frontier_closures by (auto simp: contf)
+    unfolding g_def using fros fid frontier_closures
+    by (intro continuous_on_cases) (auto simp: contf)
   moreover have "closure S \<union> closure(- S) = UNIV"
     using closure_Un by fastforce
   ultimately have contg: "continuous_on UNIV g" by metis
@@ -2027,10 +2031,8 @@
 proof -
   have "\<exists>d. 0 < d \<and> (a + d *\<^sub>R l) \<in> rel_frontier S \<and>
             (\<forall>e. 0 \<le> e \<and> e < d \<longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S)"
-       if "(a + l) \<in> affine hull S" "l \<noteq> 0" for l
-    apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> arelS])
-    apply (rule that)+
-    by metis
+    if "(a + l) \<in> affine hull S" "l \<noteq> 0" for l
+    using ray_to_rel_frontier [OF \<open>bounded S\<close> arelS] that by metis
   then obtain dd
     where dd1: "\<And>l. \<lbrakk>(a + l) \<in> affine hull S; l \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < dd l \<and> (a + dd l *\<^sub>R l) \<in> rel_frontier S"
       and dd2: "\<And>l e. \<lbrakk>(a + l) \<in> affine hull S; e < dd l; 0 \<le> e; l \<noteq> 0\<rbrakk>
@@ -2071,11 +2073,11 @@
         then have "0 < dd x" and inS: "a + dd x *\<^sub>R x \<in> rel_frontier S"
           using dd1 by auto
         moreover have "a + dd x *\<^sub>R x \<in> open_segment a (a + k *\<^sub>R x)"
-          using k \<open>x \<noteq> 0\<close> \<open>0 < dd x\<close>
-          apply (simp add: in_segment)
-          apply (rule_tac x = "dd x / k" in exI)
-          apply (simp add: that vector_add_divide_simps algebra_simps)
-          done
+          unfolding in_segment
+        proof (intro conjI exI)
+          show "a + dd x *\<^sub>R x = (1 - dd x / k) *\<^sub>R a + (dd x / k) *\<^sub>R (a + k *\<^sub>R x)"
+            using k by (simp add: that algebra_simps)
+        qed (use \<open>x \<noteq> 0\<close> \<open>0 < dd x\<close> that in auto)
         ultimately show ?thesis
           using segsub by (auto simp: rel_frontier_def)
       qed
@@ -2094,47 +2096,45 @@
     by (blast intro: continuous_on_subset)
   show ?thesis
   proof
-    show "homotopic_with_canon (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+    show "homotopic_with_canon (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
     proof (rule homotopic_with_linear)
       show "continuous_on (T - {a}) id"
         by (intro continuous_intros continuous_on_compose)
-      show "continuous_on (T - {a}) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+      show "continuous_on (T - {a}) (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
         using contdd by (simp add: o_def)
-      show "closed_segment (id x) (a + dd (x - a) *\<^sub>R (x - a)) \<subseteq> T - {a}"
+      show "closed_segment (id x) (a + dd (x-a) *\<^sub>R (x-a)) \<subseteq> T - {a}"
            if "x \<in> T - {a}" for x
       proof (clarsimp simp: in_segment, intro conjI)
         fix u::real assume u: "0 \<le> u" "u \<le> 1"
-        have "a + dd (x - a) *\<^sub>R (x - a) \<in> T"
+        have "a + dd (x-a) *\<^sub>R (x-a) \<in> T"
           by (metis DiffD1 DiffD2 add.commute add.right_neutral affS dd1 diff_add_cancel relS singletonI subsetCE that)
-        then show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<in> T"
+        then show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x-a) *\<^sub>R (x-a)) \<in> T"
           using convexD [OF \<open>convex T\<close>] that u by simp
-        have iff: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + d *\<^sub>R (x - a)) = a \<longleftrightarrow>
-                  (1 - u + u * d) *\<^sub>R (x - a) = 0" for d
+        have iff: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + d *\<^sub>R (x-a)) = a \<longleftrightarrow>
+                  (1 - u + u * d) *\<^sub>R (x-a) = 0" for d
           by (auto simp: algebra_simps)
         have "x \<in> T" "x \<noteq> a" using that by auto
-        then have axa: "a + (x - a) \<in> affine hull S"
+        then have axa: "a + (x-a) \<in> affine hull S"
            by (metis (no_types) add.commute affS diff_add_cancel rev_subsetD)
-        then have "\<not> dd (x - a) \<le> 0 \<and> a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
+        then have "\<not> dd (x-a) \<le> 0 \<and> a + dd (x-a) *\<^sub>R (x-a) \<in> rel_frontier S"
           using \<open>x \<noteq> a\<close> dd1 by fastforce
-        with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<noteq> a"
+        with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x-a) *\<^sub>R (x-a)) \<noteq> a"
           using less_eq_real_def mult_le_0_iff not_less u by (fastforce simp: iff)
       qed
     qed
-    show "retraction (T - {a}) (rel_frontier S) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+    show "retraction (T - {a}) (rel_frontier S) (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
     proof (simp add: retraction_def, intro conjI ballI)
       show "rel_frontier S \<subseteq> T - {a}"
         using arelS relS rel_frontier_def by fastforce
-      show "continuous_on (T - {a}) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+      show "continuous_on (T - {a}) (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
         using contdd by (simp add: o_def)
-      show "(\<lambda>x. a + dd (x - a) *\<^sub>R (x - a)) \<in> (T - {a}) \<rightarrow> rel_frontier S"
-        apply (auto simp: rel_frontier_def)
-        apply (metis Diff_subset add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def subset_iff)
-        by (metis DiffE add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def rev_subsetD)
-      show "a + dd (x - a) *\<^sub>R (x - a) = x" if x: "x \<in> rel_frontier S" for x
+      show "(\<lambda>x. a + dd (x-a) *\<^sub>R (x-a)) \<in> (T - {a}) \<rightarrow> rel_frontier S"
+        unfolding Pi_iff using affS dd1 subset_eq by force
+      show "a + dd (x-a) *\<^sub>R (x-a) = x" if x: "x \<in> rel_frontier S" for x
       proof -
         have "x \<noteq> a"
           using that arelS by (auto simp: rel_frontier_def)
-        have False if "dd (x - a) < 1"
+        have False if "dd (x-a) < 1"
         proof -
           have "x \<in> closure S"
             using x by (auto simp: rel_frontier_def)
@@ -2142,21 +2142,21 @@
             by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
           have  xaffS: "x \<in> affine hull S"
             using affS relS x by auto
-          then have "0 < dd (x - a)" and inS: "a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
+          then have "0 < dd (x-a)" and inS: "a + dd (x-a) *\<^sub>R (x-a) \<in> rel_frontier S"
             using dd1 by (auto simp: \<open>x \<noteq> a\<close>)
-          moreover have "a + dd (x - a) *\<^sub>R (x - a) \<in> open_segment a x"
-            using  \<open>x \<noteq> a\<close> \<open>0 < dd (x - a)\<close>
-            apply (simp add: in_segment)
-            apply (rule_tac x = "dd (x - a)" in exI)
-            apply (simp add: algebra_simps that)
-            done
+          moreover have "a + dd (x-a) *\<^sub>R (x-a) \<in> open_segment a x"
+            unfolding in_segment
+          proof (intro exI conjI)
+            show "a + dd (x-a) *\<^sub>R (x-a) = (1 - dd (x-a)) *\<^sub>R a + (dd (x-a)) *\<^sub>R x"
+              by (simp add: algebra_simps)
+          qed (use  \<open>x \<noteq> a\<close> \<open>0 < dd (x-a)\<close> that in auto)
           ultimately show ?thesis
             using segsub by (auto simp: rel_frontier_def)
         qed
-        moreover have False if "1 < dd (x - a)"
+        moreover have False if "1 < dd (x-a)"
           using x that dd2 [of "x - a" 1] \<open>x \<noteq> a\<close> closure_affine_hull
           by (auto simp: rel_frontier_def)
-        ultimately have "dd (x - a) = 1" \<comment> \<open>similar to another proof above\<close>
+        ultimately have "dd (x-a) = 1" \<comment> \<open>similar to another proof above\<close>
           by fastforce
         with that show ?thesis
           by (simp add: rel_frontier_def)
@@ -2211,13 +2211,13 @@
 subsubsection\<open>Borsuk-style characterization of separation\<close>
 
 lemma continuous_on_Borsuk_map:
-   "a \<notin> S \<Longrightarrow>  continuous_on S (\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a))"
+   "a \<notin> S \<Longrightarrow>  continuous_on S (\<lambda>x. inverse(norm (x-a)) *\<^sub>R (x-a))"
 by (rule continuous_intros | force)+
 
 lemma Borsuk_map_into_sphere:
-   "(\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a)) \<in> S \<rightarrow> sphere 0 1 \<longleftrightarrow> (a \<notin> S)"
+   "(\<lambda>x. inverse(norm (x-a)) *\<^sub>R (x-a)) \<in> S \<rightarrow> sphere 0 1 \<longleftrightarrow> (a \<notin> S)"
 proof -
-  have "\<And>x. \<lbrakk>a \<notin> S; x \<in> S\<rbrakk> \<Longrightarrow> inverse (norm (x - a)) * norm (x - a) = 1"
+  have "\<And>x. \<lbrakk>a \<notin> S; x \<in> S\<rbrakk> \<Longrightarrow> inverse (norm (x-a)) * norm (x-a) = 1"
     by (metis left_inverse norm_eq_zero right_minus_eq)
   then show ?thesis
     by force
@@ -2226,16 +2226,19 @@
 lemma Borsuk_maps_homotopic_in_path_component:
   assumes "path_component (- S) a b"
     shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
-                   (\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a))
+                   (\<lambda>x. inverse(norm(x-a)) *\<^sub>R (x-a))
                    (\<lambda>x. inverse(norm(x - b)) *\<^sub>R (x - b))"
 proof -
-  obtain g where "path g" "path_image g \<subseteq> -S" "pathstart g = a" "pathfinish g = b"
+  obtain g where g: "path g" "path_image g \<subseteq> -S" "pathstart g = a" "pathfinish g = b"
     using assms by (auto simp: path_component_def)
-  then show ?thesis
-    apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def)
-    apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g \<circ> fst)z)) *\<^sub>R (snd z - (g \<circ> fst)z)" in exI)
-    apply (rule conjI continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
-    done
+  define h where "h \<equiv> \<lambda>z. (snd z - (g \<circ> fst) z) /\<^sub>R norm (snd z - (g \<circ> fst) z)"
+  have "continuous_on ({0..1} \<times> S) h"
+    unfolding h_def using g by (intro continuous_intros) (auto simp: path_defs)
+  moreover
+  have "h ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
+    unfolding h_def using g  by (auto simp: divide_simps path_defs)
+  ultimately show ?thesis
+    using g by (auto simp: h_def path_defs homotopic_with_def)
 qed
 
 lemma non_extensible_Borsuk_map:
@@ -2243,7 +2246,7 @@
   assumes "compact S" and cin: "C \<in> components(- S)" and boc: "bounded C" and "a \<in> C"
     shows "\<not> (\<exists>g. continuous_on (S \<union> C) g \<and>
                   g \<in> (S \<union> C) \<rightarrow> sphere 0 1 \<and>
-                  (\<forall>x \<in> S. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))"
+                  (\<forall>x \<in> S. g x = inverse(norm(x-a)) *\<^sub>R (x-a)))"
 proof -
   have "closed S" using assms by (simp add: compact_imp_closed)
   have "C \<subseteq> -S"
@@ -2258,7 +2261,7 @@
   { fix g
     assume "continuous_on (S \<union> C) g"
             "g \<in> (S \<union> C) \<rightarrow> sphere 0 1"
-       and [simp]: "\<And>x. x \<in> S \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
+       and [simp]: "\<And>x. x \<in> S \<Longrightarrow> g x = (x-a) /\<^sub>R norm (x-a)"
     then have norm_g1[simp]: "\<And>x. x \<in> S \<union> C \<Longrightarrow> norm (g x) = 1"
       by force
     have cb_eq: "cball a r = (S \<union> connected_component_set (- S) a) \<union>
@@ -2269,12 +2272,12 @@
       using \<open>continuous_on (S \<union> C) g\<close> ceq
       by (intro continuous_intros) blast
     have cont2: "continuous_on (cball a r - connected_component_set (- S) a)
-            (\<lambda>x. a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+            (\<lambda>x. a + r *\<^sub>R ((x-a) /\<^sub>R norm (x-a)))"
       by (rule continuous_intros | force simp: \<open>a \<notin> S\<close>)+
     have 1: "continuous_on (cball a r)
              (\<lambda>x. if connected_component (- S) a x
                   then a + r *\<^sub>R g x
-                  else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+                  else a + r *\<^sub>R ((x-a) /\<^sub>R norm (x-a)))"
       apply (subst cb_eq)
       apply (rule continuous_on_cases [OF _ _ cont1 cont2])
       using \<open>closed S\<close> ceq cin 
@@ -2285,7 +2288,7 @@
     have "retraction (cball a r) (sphere a r)
             (\<lambda>x. if x \<in> connected_component_set (- S) a
                  then a + r *\<^sub>R g x
-                 else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+                 else a + r *\<^sub>R ((x-a) /\<^sub>R norm (x-a)))"
       using  \<open>0 < r\<close> \<open>a \<notin> S\<close> \<open>a \<in> C\<close> r
       by (auto simp: norm_minus_commute retraction_def Pi_iff ceq dist_norm abs_if 
           mult_less_0_iff divide_simps 1 2)
@@ -2294,7 +2297,7 @@
              [OF \<open>0 < r\<close>, of a, unfolded retract_of_def, simplified, rule_format,
               of "\<lambda>x. if x \<in> connected_component_set (- S) a
                       then a + r *\<^sub>R g x
-                      else a + r *\<^sub>R inverse(norm(x - a)) *\<^sub>R (x - a)"]
+                      else a + r *\<^sub>R inverse(norm(x-a)) *\<^sub>R (x-a)"]
       by blast
   }
   then show ?thesis
@@ -2305,10 +2308,8 @@
 
 lemma brouwer_surjective:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "compact T"
-    and "convex T"
-    and "T \<noteq> {}"
-    and "continuous_on T f"
+  assumes T: "compact T" "convex T" "T \<noteq> {}"
+    and f: "continuous_on T f"
     and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
     and "x \<in> S"
   shows "\<exists>y\<in>T. f y = x"
@@ -2317,11 +2318,10 @@
     by (auto simp add: algebra_simps)
   show ?thesis
     unfolding *
-    apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
-    apply (intro continuous_intros)
-    using assms
-    apply auto
-    done
+  proof (rule brouwer[OF T])
+    show "continuous_on T (\<lambda>y. x + (y - f y))"
+      by (intro continuous_intros f)
+  qed (use assms in auto)
 qed
 
 lemma brouwer_surjective_cball:
diff -r 646cd337bb08 -r 0f9cd1a5edbe src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Wed Apr 10 11:32:48 2024 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Fri Apr 12 09:58:32 2024 +0100
@@ -22,19 +22,14 @@
 lemma expand_superset:
   assumes "finite A" and "{a. g a \<noteq> \<^bold>1} \<subseteq> A"
   shows "G g = F.F g A"
-  apply (simp add: expand_set)
-  apply (rule F.same_carrierI [of A])
-  apply (simp_all add: assms)
-  done
+  using F.mono_neutral_right assms expand_set by fastforce
 
 lemma conditionalize:
   assumes "finite A"
   shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else \<^bold>1)"
   using assms
-  apply (simp add: expand_set)
-  apply (rule F.same_carrierI [of A])
-  apply auto
-  done
+  by (smt (verit, ccfv_threshold) Diff_iff F.mono_neutral_cong_right expand_set mem_Collect_eq subsetI)
+
 
 lemma neutral [simp]:
   "G (\<lambda>a. \<^bold>1) = \<^bold>1"
@@ -140,30 +135,13 @@
     by (auto simp add: finite_cartesian_product_iff)
   have *: "G (\<lambda>a. G (g a)) =
     (F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) {a. \<exists>b. g a b \<noteq> \<^bold>1})"
-    apply (subst expand_superset [of "?B"])
-    apply (rule \<open>finite ?B\<close>)
-    apply auto
-    apply (subst expand_superset [of "?A"])
-    apply (rule \<open>finite ?A\<close>)
-    apply auto
-    apply (erule F.not_neutral_contains_not_neutral)
-    apply auto
-    done
-  have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> ?A \<times> ?B"
+    using \<open>finite ?A\<close> \<open>finite ?B\<close> expand_superset
+    by (smt (verit, del_insts) Collect_mono local.cong not_neutral_obtains_not_neutral)
+  have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> ?A \<times> ?B"
     by auto
-  with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> C"
-    by blast
   show ?thesis
-    apply (simp add: *)
-    apply (simp add: F.cartesian_product)
-    apply (subst expand_superset [of C])
-    apply (rule \<open>finite C\<close>)
-    apply (simp_all add: **)
-    apply (rule F.same_carrierI [of C])
-    apply (rule \<open>finite C\<close>)
-    apply (simp_all add: subset)
-    apply auto
-    done
+    using \<open>finite C\<close> expand_superset
+    using "*" ** F.cartesian_product fin_prod by force
 qed
 
 lemma cartesian_product2:
@@ -231,37 +209,23 @@
   fixes r :: "'a :: semiring_0"
   assumes "finite {a. g a \<noteq> 0}"
   shows "Sum_any g * r = (\<Sum>n. g n * r)"
-proof -
-  note assms
-  moreover have "{a. g a * r \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
-  ultimately show ?thesis
-    by (simp add: sum_distrib_right Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
-qed  
+  by (metis (mono_tags, lifting) Collect_mono Sum_any.expand_superset assms mult_zero_left sum_distrib_right)
 
 lemma Sum_any_right_distrib:
   fixes r :: "'a :: semiring_0"
   assumes "finite {a. g a \<noteq> 0}"
   shows "r * Sum_any g = (\<Sum>n. r * g n)"
-proof -
-  note assms
-  moreover have "{a. r * g a \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
-  ultimately show ?thesis
-    by (simp add: sum_distrib_left Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
-qed
+  by (metis (mono_tags, lifting) Collect_mono Sum_any.expand_superset assms mult_zero_right sum_distrib_left)
 
 lemma Sum_any_product:
   fixes f g :: "'b \<Rightarrow> 'a::semiring_0"
   assumes "finite {a. f a \<noteq> 0}" and "finite {b. g b \<noteq> 0}"
   shows "Sum_any f * Sum_any g = (\<Sum>a. \<Sum>b. f a * g b)"
 proof -
-  have subset_f: "{a. (\<Sum>b. f a * g b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}"
-    by rule (simp, rule, auto)
-  moreover have subset_g: "\<And>a. {b. f a * g b \<noteq> 0} \<subseteq> {b. g b \<noteq> 0}"
-    by rule (simp, rule, auto)
-  ultimately show ?thesis using assms
-    by (auto simp add: Sum_any.expand_set [of f] Sum_any.expand_set [of g]
-      Sum_any.expand_superset [of "{a. f a \<noteq> 0}"] Sum_any.expand_superset [of "{b. g b \<noteq> 0}"]
-      sum_product)
+  have "\<forall>a. (\<Sum>b. a * g b) = a * Sum_any g"
+    by (simp add: Sum_any_right_distrib assms(2))
+  then show ?thesis
+    by (simp add: Sum_any_left_distrib assms(1))
 qed
 
 lemma Sum_any_eq_zero_iff [simp]: 
diff -r 646cd337bb08 -r 0f9cd1a5edbe src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Apr 10 11:32:48 2024 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Apr 12 09:58:32 2024 +0100
@@ -559,10 +559,7 @@
 
 lemma mset_subset_eq_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)"
   unfolding subseteq_mset_def
-  apply (rule iffI)
-   apply (rule exI [where x = "B - A"])
-   apply (auto intro: multiset_eq_iff [THEN iffD2])
-  done
+  by (metis add_diff_cancel_left' count_diff count_union le_Suc_ex le_add_same_cancel1 multiset_eq_iff zero_le)
 
 interpretation subset_mset: ordered_cancel_comm_monoid_diff "(+)" 0 "(\<subseteq>#)" "(\<subset>#)" "(-)"
   by standard (simp, fact mset_subset_eq_exists_conv)
@@ -629,14 +626,18 @@
   by (metis mset_subset_eqD subsetI)
 
 lemma mset_subset_eq_insertD:
-  "add_mset x A \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
-apply (rule conjI)
- apply (simp add: mset_subset_eqD)
- apply (clarsimp simp: subset_mset_def subseteq_mset_def)
- apply safe
-  apply (erule_tac x = a in allE)
-  apply (auto split: if_split_asm)
-done
+  assumes "add_mset x A \<subseteq># B"
+  shows "x \<in># B \<and> A \<subset># B"
+proof 
+  show "x \<in># B"
+    using assms by (simp add: mset_subset_eqD)
+  have "A \<subseteq># add_mset x A"
+    by (metis (no_types) add_mset_add_single mset_subset_eq_add_left)
+  then have "A \<subset># add_mset x A"
+    by (meson multi_self_add_other_not_self subset_mset.le_imp_less_or_eq)
+  then show "A \<subset># B"
+    using assms subset_mset.strict_trans2 by blast
+qed
 
 lemma mset_subset_insertD:
   "add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
@@ -653,11 +654,7 @@
 
 lemma insert_subset_eq_iff:
   "add_mset a A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
-  using le_diff_conv2 [of "Suc 0" "count B a" "count A a"]
-  apply (auto simp add: subseteq_mset_def not_in_iff Suc_le_eq)
-  apply (rule ccontr)
-  apply (auto simp add: not_in_iff)
-  done
+  using mset_subset_eq_insertD subset_mset.le_diff_conv2 by fastforce
 
 lemma insert_union_subset_iff:
   "add_mset a A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
@@ -723,11 +720,12 @@
   by (simp add: union_mset_def)
 
 global_interpretation subset_mset: semilattice_neutr_order \<open>(\<union>#)\<close> \<open>{#}\<close> \<open>(\<supseteq>#)\<close> \<open>(\<supset>#)\<close>
-  apply standard
-      apply (simp_all add: multiset_eq_iff subseteq_mset_def subset_mset_def max_def)
-   apply (auto simp add: le_antisym dest: sym)
-   apply (metis nat_le_linear)+
-  done
+proof 
+  show "\<And>a b. (b \<subseteq># a) = (a = a \<union># b)"
+    by (simp add: Diff_eq_empty_iff_mset union_mset_def)
+  show "\<And>a b. (b \<subset># a) = (a = a \<union># b \<and> a \<noteq> b)"
+    by (metis Diff_eq_empty_iff_mset add_cancel_left_right subset_mset_def union_mset_def)
+qed (auto simp: multiset_eqI union_mset_def)
 
 interpretation subset_mset: semilattice_sup \<open>(\<union>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
 proof -
@@ -774,30 +772,8 @@
 qed
 
 lemma disjunct_not_in:
-  "A \<inter># B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)" (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?P
-  show ?Q
-  proof
-    fix a
-    from \<open>?P\<close> have "min (count A a) (count B a) = 0"
-      by (simp add: multiset_eq_iff)
-    then have "count A a = 0 \<or> count B a = 0"
-      by (cases "count A a \<le> count B a") (simp_all add: min_def)
-    then show "a \<notin># A \<or> a \<notin># B"
-      by (simp add: not_in_iff)
-  qed
-next
-  assume ?Q
-  show ?P
-  proof (rule multiset_eqI)
-    fix a
-    from \<open>?Q\<close> have "count A a = 0 \<or> count B a = 0"
-      by (auto simp add: not_in_iff)
-    then show "count (A \<inter># B) a = count {#} a"
-      by auto
-  qed
-qed
+  "A \<inter># B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)"
+  by (metis disjoint_iff set_mset_eq_empty_iff set_mset_inter)
 
 lemma inter_mset_empty_distrib_right: "A \<inter># (B + C) = {#} \<longleftrightarrow> A \<inter># B = {#} \<and> A \<inter># C = {#}"
   by (meson disjunct_not_in union_iff)
@@ -1148,15 +1124,7 @@
   fix X :: "'a multiset" and A
   assume "X \<in> A"
   show "Inf A \<subseteq># X"
-  proof (rule mset_subset_eqI)
-    fix x
-    from \<open>X \<in> A\<close> have "A \<noteq> {}" by auto
-    hence "count (Inf A) x = (INF X\<in>A. count X x)"
-      by (simp add: count_Inf_multiset_nonempty)
-    also from \<open>X \<in> A\<close> have "\<dots> \<le> count X x"
-      by (intro cInf_lower) simp_all
-    finally show "count (Inf A) x \<le> count X x" .
-  qed
+    by (metis \<open>X \<in> A\<close> count_Inf_multiset_nonempty empty_iff image_eqI mset_subset_eqI wellorder_Inf_le1)
 next
   fix X :: "'a multiset" and A
   assume nonempty: "A \<noteq> {}" and le: "\<And>Y. Y \<in> A \<Longrightarrow> X \<subseteq># Y"
@@ -1240,8 +1208,7 @@
       using that by (auto simp: subseteq_mset_def algebra_simps not_in_iff)
     hence "Sup A \<subseteq># Sup A - {#x#}" by (intro subset_mset.cSup_least nonempty)
     with \<open>x \<in># Sup A\<close> show False
-      by (auto simp: subseteq_mset_def simp flip: count_greater_zero_iff
-               dest!: spec[of _ x])
+      using mset_subset_diff_self by fastforce
   qed
 next
   fix x X assume "x \<in> set_mset X" "X \<in> A"
@@ -1253,20 +1220,12 @@
 lemma in_Sup_multiset_iff:
   assumes "subset_mset.bdd_above A"
   shows   "x \<in># Sup A \<longleftrightarrow> (\<exists>X\<in>A. x \<in># X)"
-proof -
-  from assms have "set_mset (Sup A) = (\<Union>X\<in>A. set_mset X)" by (rule set_mset_Sup)
-  also have "x \<in> \<dots> \<longleftrightarrow> (\<exists>X\<in>A. x \<in># X)" by simp
-  finally show ?thesis .
-qed
+  by (simp add: assms set_mset_Sup)
 
 lemma in_Sup_multisetD:
   assumes "x \<in># Sup A"
   shows   "\<exists>X\<in>A. x \<in># X"
-proof -
-  have "subset_mset.bdd_above A"
-    by (rule ccontr) (insert assms, simp_all add: Sup_multiset_unbounded)
-  with assms show ?thesis by (simp add: in_Sup_multiset_iff)
-qed
+  using Sup_multiset_unbounded assms in_Sup_multiset_iff by fastforce
 
 interpretation subset_mset: distrib_lattice "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
 proof
@@ -1328,11 +1287,7 @@
 lemma multiset_filter_mono:
   assumes "A \<subseteq># B"
   shows "filter_mset f A \<subseteq># filter_mset f B"
-proof -
-  from assms[unfolded mset_subset_eq_exists_conv]
-  obtain C where B: "B = A + C" by auto
-  show ?thesis unfolding B by auto
-qed
+  by (metis assms filter_sup_mset subset_mset.order_iff)
 
 lemma filter_mset_eq_conv:
   "filter_mset P M = N \<longleftrightarrow> N \<subseteq># M \<and> (\<forall>b\<in>#N. P b) \<and> (\<forall>a\<in>#M - N. \<not> P a)" (is "?P \<longleftrightarrow> ?Q")
@@ -1421,16 +1376,16 @@
   size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified]
 
 lemma size_multiset_empty [simp]: "size_multiset f {#} = 0"
-by (simp add: size_multiset_def)
+  by (simp add: size_multiset_def)
 
 lemma size_empty [simp]: "size {#} = 0"
-by (simp add: size_multiset_overloaded_def)
+  by (simp add: size_multiset_overloaded_def)
 
 lemma size_multiset_single : "size_multiset f {#b#} = Suc (f b)"
-by (simp add: size_multiset_eq)
+  by (simp add: size_multiset_eq)
 
 lemma size_single: "size {#b#} = 1"
-by (simp add: size_multiset_overloaded_def size_multiset_single)
+  by (simp add: size_multiset_overloaded_def size_multiset_single)
 
 lemma sum_wcount_Int:
   "finite A \<Longrightarrow> sum (wcount f N) (A \<inter> set_mset N) = sum (wcount f N) A"
@@ -1439,20 +1394,18 @@
 
 lemma size_multiset_union [simp]:
   "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
-apply (simp add: size_multiset_def sum_Un_nat sum.distrib sum_wcount_Int wcount_union)
-apply (subst Int_commute)
-apply (simp add: sum_wcount_Int)
-done
+  apply (simp add: size_multiset_def sum_Un_nat sum.distrib sum_wcount_Int wcount_union)
+  by (metis add_implies_diff finite_set_mset inf.commute sum_wcount_Int)
 
 lemma size_multiset_add_mset [simp]:
   "size_multiset f (add_mset a M) = Suc (f a) + size_multiset f M"
-  unfolding add_mset_add_single[of _ M] size_multiset_union by (auto simp: size_multiset_single)
+  by (metis add.commute add_mset_add_single size_multiset_single size_multiset_union)
 
 lemma size_add_mset [simp]: "size (add_mset a A) = Suc (size A)"
-by (simp add: size_multiset_overloaded_def wcount_add_mset)
+  by (simp add: size_multiset_overloaded_def wcount_add_mset)
 
 lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
-by (auto simp add: size_multiset_overloaded_def)
+  by (auto simp add: size_multiset_overloaded_def)
 
 lemma size_multiset_eq_0_iff_empty [iff]:
   "size_multiset f M = 0 \<longleftrightarrow> M = {#}"
@@ -1462,23 +1415,15 @@
 by (auto simp add: size_multiset_overloaded_def)
 
 lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
-by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
+  by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
 
 lemma size_eq_Suc_imp_elem: "size M = Suc n \<Longrightarrow> \<exists>a. a \<in># M"
-apply (unfold size_multiset_overloaded_eq)
-apply (drule sum_SucD)
-apply auto
-done
+  using all_not_in_conv by fastforce
 
 lemma size_eq_Suc_imp_eq_union:
   assumes "size M = Suc n"
   shows "\<exists>a N. M = add_mset a N"
-proof -
-  from assms obtain a where "a \<in># M"
-    by (erule size_eq_Suc_imp_elem [THEN exE])
-  then have "M = add_mset a (M - {#a#})" by simp
-  then show ?thesis by blast
-qed
+  by (metis assms insert_DiffM size_eq_Suc_imp_elem)
 
 lemma size_mset_mono:
   fixes A B :: "'a multiset"
@@ -1491,7 +1436,7 @@
 qed
 
 lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \<le> size M"
-by (rule size_mset_mono[OF multiset_filter_subset])
+  by (rule size_mset_mono[OF multiset_filter_subset])
 
 lemma size_Diff_submset:
   "M \<subseteq># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
@@ -1560,22 +1505,21 @@
 qed (simp add: empty)
 
 lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = add_mset a A"
-by (induct M) auto
+  by (induct M) auto
 
 lemma multiset_cases [cases type]:
-  obtains (empty) "M = {#}"
-    | (add) x N where "M = add_mset x N"
+  obtains (empty) "M = {#}" | (add) x N where "M = add_mset x N"
   by (induct M) simp_all
 
 lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
-by (cases "B = {#}") (auto dest: multi_member_split)
+  by (cases "B = {#}") (auto dest: multi_member_split)
 
 lemma union_filter_mset_complement[simp]:
   "\<forall>x. P x = (\<not> Q x) \<Longrightarrow> filter_mset P M + filter_mset Q M = M"
-by (subst multiset_eq_iff) auto
+  by (subst multiset_eq_iff) auto
 
 lemma multiset_partition: "M = {#x \<in># M. P x#} + {#x \<in># M. \<not> P x#}"
-by simp
+  by simp
 
 lemma mset_subset_size: "A \<subset># B \<Longrightarrow> size A < size B"
 proof (induct A arbitrary: B)
@@ -1587,8 +1531,7 @@
   have "add_mset x A \<subseteq># B"
     by (meson add.prems subset_mset_def)
   then show ?case
-    by (metis (no_types) add.prems add.right_neutral add_diff_cancel_left' leD nat_neq_iff
-      size_Diff_submset size_eq_0_iff_empty size_mset_mono subset_mset.le_iff_add subset_mset_def)
+    using add.prems subset_mset.less_eqE by fastforce
 qed
 
 lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
@@ -1605,19 +1548,17 @@
 text \<open>Well-foundedness of strict subset relation\<close>
 
 lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
-apply (rule wf_measure [THEN wf_subset, where f1=size])
-apply (clarsimp simp: measure_def inv_image_def mset_subset_size)
-done
+  using mset_subset_size wfP_def wfP_if_convertible_to_nat by blast
 
 lemma wfP_subset_mset[simp]: "wfP (\<subset>#)"
   by (rule wf_subset_mset_rel[to_pred])
 
 lemma full_multiset_induct [case_names less]:
-assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
-shows "P B"
-apply (rule wf_subset_mset_rel [THEN wf_induct])
-apply (rule ih, auto)
-done
+  assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
+  shows "P B"
+  apply (rule wf_subset_mset_rel [THEN wf_induct])
+  apply (rule ih, auto)
+  done
 
 lemma multi_subset_induct [consumes 2, case_names empty add]:
   assumes "F \<subseteq># A"
@@ -1912,9 +1853,7 @@
   proof (cases "x \<in># B")
     case True
     with add.prems have "image_mset f A = image_mset f (B - {#x#}) + C"
-      by (smt (verit, del_insts) add.left_commute add_cancel_right_left diff_union_cancelL
-          diff_union_single_conv image_mset_union union_mset_add_mset_left
-          union_mset_add_mset_right)
+      by (smt (verit) add_mset_add_mset_same_iff image_mset_add_mset insert_DiffM union_mset_add_mset_left)
     with add.IH have "\<exists>M3'. A = B - {#x#} + M3' \<and> image_mset f M3' = C"
       by (smt (verit, del_insts) True Un_insert_left Un_insert_right add.prems(2) inj_on_insert
           insert_DiffM set_mset_add_mset_insert)
@@ -2035,12 +1974,7 @@
 
 lemma set_eq_iff_mset_remdups_eq:
   \<open>set x = set y \<longleftrightarrow> mset (remdups x) = mset (remdups y)\<close>
-apply (rule iffI)
-apply (simp add: set_eq_iff_mset_eq_distinct[THEN iffD1])
-apply (drule distinct_remdups [THEN distinct_remdups
-      [THEN set_eq_iff_mset_eq_distinct [THEN iffD2]]])
-apply simp
-done
+  using set_eq_iff_mset_eq_distinct by fastforce
 
 lemma mset_eq_imp_distinct_iff:
   \<open>distinct xs \<longleftrightarrow> distinct ys\<close> if \<open>mset xs = mset ys\<close>
@@ -2255,14 +2189,14 @@
 
 lemma set_sorted_list_of_multiset [simp]:
   "set (sorted_list_of_multiset M) = set_mset M"
-by (induct M) (simp_all add: set_insort_key)
+  by (induct M) (simp_all add: set_insort_key)
 
 lemma sorted_list_of_mset_set [simp]:
   "sorted_list_of_multiset (mset_set A) = sorted_list_of_set A"
-by (cases "finite A") (induct A rule: finite_induct, simp_all)
+  by (cases "finite A") (induct A rule: finite_induct, simp_all)
 
 lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
-  by (induction n) (simp_all add: atLeastLessThanSuc)
+  by (metis distinct_upt mset_set_set set_upt)
 
 lemma image_mset_map_of:
   "distinct (map fst xs) \<Longrightarrow> {#the (map_of xs i). i \<in># mset (map fst xs)#} = mset (map snd xs)"
@@ -2308,7 +2242,7 @@
   unfolding replicate_mset_def by (induct n) auto
 
 lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
-  by (auto split: if_splits)
+  by auto
 
 lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
   by (induct n, simp_all)
@@ -2530,8 +2464,8 @@
   shows "size {#x \<in># M. P x#} < size M"
 proof -
   have "size (filter_mset P M) \<noteq> size M"
-    using assms by (metis add.right_neutral add_diff_cancel_left' count_filter_mset mem_Collect_eq
-      multiset_partition nonempty_has_size set_mset_def size_union)
+    using assms
+    by (metis dual_order.strict_iff_order filter_mset_eq_conv mset_subset_size subset_mset.nless_le)
   then show ?thesis
     by (meson leD nat_neq_iff size_filter_mset_lesseq)
 qed
@@ -3956,17 +3890,11 @@
   by (force simp: mult1_def)
 
 lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
-apply (unfold less_multiset_def multp_def mult_def)
-apply (erule trancl_induct)
- apply (blast intro: mult1_union)
-apply (blast intro: mult1_union trancl_trans)
-done
+  unfolding less_multiset_def multp_def mult_def
+  by (induction rule: trancl_induct; blast intro: mult1_union trancl_trans)
 
 lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::preorder multiset)"
-apply (subst add.commute [of B C])
-apply (subst add.commute [of D C])
-apply (erule union_le_mono2)
-done
+  by (metis add.commute union_le_mono2)
 
 lemma union_less_mono:
   fixes A B C D :: "'a::preorder multiset"
@@ -3991,8 +3919,8 @@
 definition "ms_weak = ms_strict \<union> Id"
 
 lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
-unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
-by (auto intro: wf_mult1 wf_trancl simp: mult_def)
+  unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
+  by (auto intro: wf_mult1 wf_trancl simp: mult_def)
 
 lemma smsI:
   "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
@@ -4268,11 +4196,7 @@
 
 lemma [code]: \<comment> \<open>not very efficient, but representation-ignorant!\<close>
   "mset_set A = mset (sorted_list_of_set A)"
-  apply (cases "finite A")
-  apply simp_all
-  apply (induct A rule: finite_induct)
-  apply simp_all
-  done
+  by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set)
 
 declare size_mset [code]
 
@@ -4313,18 +4237,15 @@
     hence id: "mset ys = add_mset x (mset (ys1 @ ys2))"
       by auto
     show ?thesis unfolding subset_eq_mset_impl.simps
-      unfolding Some option.simps split
-      unfolding id
-      using Cons[of "ys1 @ ys2"]
-      unfolding subset_mset_def subseteq_mset_def by auto
+      by (simp add: Some id Cons)
   qed
 qed
 
 lemma [code]: "mset xs \<subseteq># mset ys \<longleftrightarrow> subset_eq_mset_impl xs ys \<noteq> None"
-  using subset_eq_mset_impl[of xs ys] by (cases "subset_eq_mset_impl xs ys", auto)
+  by (simp add: subset_eq_mset_impl)
 
 lemma [code]: "mset xs \<subset># mset ys \<longleftrightarrow> subset_eq_mset_impl xs ys = Some True"
-  using subset_eq_mset_impl[of xs ys] by (cases "subset_eq_mset_impl xs ys", auto)
+  using subset_eq_mset_impl by blast
 
 instantiation multiset :: (equal) equal
 begin
@@ -4519,14 +4440,10 @@
   rel: rel_mset
   pred: pred_mset
 proof -
-  show "image_mset id = id"
-    by (rule image_mset.id)
   show "image_mset (g \<circ> f) = image_mset g \<circ> image_mset f" for f g
     unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
   show "(\<And>z. z \<in> set_mset X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X" for f g X
     by (induct X) simp_all
-  show "set_mset \<circ> image_mset f = (`) f \<circ> set_mset" for f
-    by auto
   show "card_order natLeq"
     by (rule natLeq_card_order)
   show "BNF_Cardinal_Arithmetic.cinfinite natLeq"
@@ -4538,34 +4455,15 @@
       (auto simp: finite_iff_ordLess_natLeq[symmetric])
   show "rel_mset R OO rel_mset S \<le> rel_mset (R OO S)" for R S
     unfolding rel_mset_def[abs_def] OO_def
-    apply clarify
-    subgoal for X Z Y xs ys' ys zs
-      apply (drule list_all2_reorder_left_invariance [where xs = ys' and ys = zs and xs' = ys])
-      apply (auto intro: list_all2_trans)
-      done
-    done
+    by (smt (verit, ccfv_SIG) list_all2_reorder_left_invariance list_all2_trans predicate2I)
   show "rel_mset R =
     (\<lambda>x y. \<exists>z. set_mset z \<subseteq> {(x, y). R x y} \<and>
     image_mset fst z = x \<and> image_mset snd z = y)" for R
     unfolding rel_mset_def[abs_def]
-    apply (rule ext)+
-    apply safe
-     apply (rule_tac x = "mset (zip xs ys)" in exI;
-       auto simp: in_set_zip list_all2_iff simp flip: mset_map)
-    apply (rename_tac XY)
-    apply (cut_tac X = XY in ex_mset)
-    apply (erule exE)
-    apply (rename_tac xys)
-    apply (rule_tac x = "map fst xys" in exI)
-    apply (auto simp: mset_map)
-    apply (rule_tac x = "map snd xys" in exI)
-    apply (auto simp: mset_map list_all2I subset_eq zip_map_fst_snd)
-    done
-  show "z \<in> set_mset {#} \<Longrightarrow> False" for z
-    by auto
+    by (metis (no_types, lifting) ex_mset list.in_rel mem_Collect_eq mset_map set_mset_mset)
   show "pred_mset P = (\<lambda>x. Ball (set_mset x) P)" for P
     by (simp add: fun_eq_iff pred_mset_iff)
-qed
+qed auto
 
 inductive rel_mset' :: \<open>('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset \<Rightarrow> bool\<close>
 where
@@ -4609,10 +4507,7 @@
     and addL: "\<And>a M N. P M N \<Longrightarrow> P (add_mset a M) N"
     and addR: "\<And>a M N. P M N \<Longrightarrow> P M (add_mset a N)"
   shows "P M N"
-apply(induct N rule: multiset_induct)
-  apply(induct M rule: multiset_induct, rule empty, erule addL)
-  apply(induct M rule: multiset_induct, erule addR, erule addR)
-done
+  by (induct N rule: multiset_induct; induct M rule: multiset_induct) (auto simp: assms)
 
 lemma multiset_induct2_size[consumes 1, case_names empty add]:
   assumes c: "size M = size N"
diff -r 646cd337bb08 -r 0f9cd1a5edbe src/HOL/Library/Poly_Mapping.thy
--- a/src/HOL/Library/Poly_Mapping.thy	Wed Apr 10 11:32:48 2024 +0100
+++ b/src/HOL/Library/Poly_Mapping.thy	Fri Apr 12 09:58:32 2024 +0100
@@ -459,7 +459,7 @@
     {b. \<exists>a. (f a * g b when k = a + b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
     by auto
   ultimately show ?thesis using fin_g
-    by (auto simp add: prod_fun_def
+    by (auto simp: prod_fun_def
       Sum_any.cartesian_product [of "{a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"] Sum_any_right_distrib mult_when)
 qed
 
@@ -526,14 +526,13 @@
       have "?lhs k = (\<Sum>(ab, c). (\<Sum>(a, b). f a * g b when ab = a + b) * h c when k = ab + c)"
         by (simp add: prod_fun_unfold_prod)
       also have "\<dots> = (\<Sum>(ab, c). (\<Sum>(a, b). f a * g b * h c when k = ab + c when ab = a + b))"
-        apply (subst Sum_any_left_distrib)
-        using fin_fg apply (simp add: split_def)
-        apply (subst Sum_any_when_independent [symmetric])
-        apply (simp add: when_when when_mult mult_when split_def conj_commute)
+        using fin_fg 
+        apply (simp add: Sum_any_left_distrib split_def flip: Sum_any_when_independent)
+        apply (simp add: when_when when_mult mult_when conj_commute)
         done
       also have "\<dots> = (\<Sum>(ab, c, a, b). f a * g b * h c when k = ab + c when ab = a + b)"
         apply (subst Sum_any.cartesian_product2 [of "(?FG' \<times> ?H) \<times> ?FG"])
-        apply (auto simp add: finite_cartesian_product_iff fin_fg fin_fg' fin_h dest: mult_not_zero)
+        apply (auto simp: finite_cartesian_product_iff fin_fg fin_fg' fin_h dest: mult_not_zero)
         done
       also have "\<dots> = (\<Sum>(ab, c, a, b). f a * g b * h c when k = a + b + c when ab = a + b)"
         by (rule Sum_any.cong) (simp add: split_def when_def)
@@ -558,7 +557,7 @@
       qed
       also have "\<dots> = (\<Sum>(a, bc). (\<Sum>(b, c). f a * g b * h c when bc = b + c when k = a + bc))"
         apply (subst Sum_any.cartesian_product2 [of "(?F \<times> ?GH') \<times> ?GH"])
-        apply (auto simp add: finite_cartesian_product_iff fin_f fin_gh fin_gh' ac_simps dest: mult_not_zero)
+        apply (auto simp: finite_cartesian_product_iff fin_f fin_gh fin_gh' ac_simps dest: mult_not_zero)
         done
       also have "\<dots> = (\<Sum>(a, bc). f a * (\<Sum>(b, c). g b * h c when bc = b + c) when k = a + bc)"
         apply (subst Sum_any_right_distrib)
@@ -580,10 +579,8 @@
     assume fin_h: "finite {k. h k \<noteq> 0}"
     show "prod_fun (\<lambda>k. f k + g k) h = (\<lambda>k. prod_fun f h k + prod_fun g h k)"
       apply (rule ext)
-      apply (auto simp add: prod_fun_def algebra_simps)
-      apply (subst Sum_any.distrib)
-      using fin_f fin_g apply (auto intro: finite_mult_not_eq_zero_rightI)
-      done
+      apply (simp add: prod_fun_def algebra_simps)
+      by (simp add: Sum_any.distrib fin_f fin_g finite_mult_not_eq_zero_rightI)
   qed
   show "a * (b + c) = a * b + a * c"
   proof transfer
@@ -593,15 +590,8 @@
     assume fin_h: "finite {k. h k \<noteq> 0}"
     show "prod_fun f (\<lambda>k. g k + h k) = (\<lambda>k. prod_fun f g k + prod_fun f h k)"
       apply (rule ext)
-      apply (auto simp add: prod_fun_def Sum_any.distrib algebra_simps when_add_distrib)
-      apply (subst Sum_any.distrib)
-      apply (simp_all add: algebra_simps)
-      apply (auto intro: fin_g fin_h)
-      apply (subst Sum_any.distrib)
-      apply (simp_all add: algebra_simps)
-      using fin_f apply (rule finite_mult_not_eq_zero_rightI)
-      using fin_f apply (rule finite_mult_not_eq_zero_rightI)
-      done
+      apply (auto simp: prod_fun_def Sum_any.distrib algebra_simps when_add_distrib fin_g fin_h)
+      by (simp add: Sum_any.distrib fin_f finite_mult_not_eq_zero_rightI)
   qed
   show "0 * a = 0"
     by transfer (simp add: prod_fun_def [abs_def])
@@ -632,16 +622,10 @@
         using fin_g by auto
       from fin_f fin_g have "finite {(a, b). f a \<noteq> 0 \<and> g b \<noteq> 0}" (is "finite ?AB")
         by simp
-      show "prod_fun f g k = prod_fun g f k"
-        apply (simp add: prod_fun_def)
-        apply (subst Sum_any_right_distrib)
-        apply (rule fin2)
-        apply (subst Sum_any_right_distrib)
-         apply (rule fin1)
-        apply (subst Sum_any.swap [of ?AB])
-        apply (fact \<open>finite ?AB\<close>)
-        apply (auto simp add: mult_when ac_simps)
-        done
+      have "(\<Sum>a. \<Sum>n. f a * (g n when k = a + n)) = (\<Sum>a. \<Sum>n. g a * (f n when k = a + n))"
+        by (subst Sum_any.swap [OF \<open>finite ?AB\<close>]) (auto simp: mult_when ac_simps)
+      then show "prod_fun f g k = prod_fun g f k"
+        by (simp add: prod_fun_def Sum_any_right_distrib [OF fin2] Sum_any_right_distrib [OF fin1])
     qed
   qed
   show "(a + b) * c = a * c + b * c"
@@ -651,12 +635,8 @@
     assume fin_g: "finite {k. g k \<noteq> 0}"
     assume fin_h: "finite {k. h k \<noteq> 0}"
     show "prod_fun (\<lambda>k. f k + g k) h = (\<lambda>k. prod_fun f h k + prod_fun g h k)"
-      apply (auto simp add: prod_fun_def fun_eq_iff algebra_simps)
-      apply (subst Sum_any.distrib)
-      using fin_f apply (rule finite_mult_not_eq_zero_rightI)
-      using fin_g apply (rule finite_mult_not_eq_zero_rightI)
-      apply simp_all
-      done
+      by (auto simp: prod_fun_def fun_eq_iff algebra_simps 
+            Sum_any.distrib fin_f fin_g finite_mult_not_eq_zero_rightI)
   qed
 qed
 
@@ -720,7 +700,7 @@
 
 lemma lookup_single:
   "lookup (single k v) k' = (v when k = k')"
-  by transfer rule
+  by (simp add: single.rep_eq)
 
 lemma lookup_single_eq [simp]:
   "lookup (single k v) k = v"
@@ -810,11 +790,7 @@
 
 lemma lookup_of_int:
   "lookup (of_int l) k = (of_int l when k = 0)"
-proof -
-  have "lookup (of_int l) k = lookup (single 0 (of_int l)) k"
-    by simp
-  then show ?thesis unfolding lookup_single by simp
-qed
+  by (metis lookup_single_not_eq single.rep_eq single_of_int)
 
 
 subsection \<open>Integral domains\<close>
@@ -841,10 +817,10 @@
       by simp
     assume "f \<noteq> (\<lambda>a. 0)"
     then obtain a where "f a \<noteq> 0"
-      by (auto simp add: fun_eq_iff)
+      by (auto simp: fun_eq_iff)
     assume "g \<noteq> (\<lambda>b. 0)"
     then obtain b where "g b \<noteq> 0"
-      by (auto simp add: fun_eq_iff)
+      by (auto simp: fun_eq_iff)
     from \<open>f a \<noteq> 0\<close> and \<open>g b \<noteq> 0\<close> have "F \<noteq> {}" and "G \<noteq> {}"
       by auto
     note Max_F = \<open>finite F\<close> \<open>F \<noteq> {}\<close>
@@ -860,7 +836,7 @@
     define q where "q = Max F + Max G"
     have "(\<Sum>(a, b). f a * g b when q = a + b) =
       (\<Sum>(a, b). f a * g b when q = a + b when a \<in> F \<and> b \<in> G)"
-      by (rule Sum_any.cong) (auto simp add: split_def when_def q_def intro: ccontr)
+      by (rule Sum_any.cong) (auto simp: split_def when_def q_def intro: ccontr)
     also have "\<dots> =
       (\<Sum>(a, b). f a * g b when (Max F, Max G) = (a, b))"
     proof (rule Sum_any.cong)
@@ -873,7 +849,7 @@
         by auto
       show "(case ab of (a, b) \<Rightarrow> f a * g b when q = a + b when a \<in> F \<and> b \<in> G) =
          (case ab of (a, b) \<Rightarrow> f a * g b when (Max F, Max G) = (a, b))"
-        by (auto simp add: split_def when_def q_def dest: add_strict_mono [of a "Max F" b "Max G"])
+        by (auto simp: split_def when_def q_def dest: add_strict_mono [of a "Max F" b "Max G"])
     qed
     also have "\<dots> = (\<Sum>ab. (case ab of (a, b) \<Rightarrow> f a * g b) when
       (Max F, Max G) = ab)"
@@ -883,7 +859,7 @@
     finally have "prod_fun f g q \<noteq> 0"
       by (simp add: prod_fun_unfold_prod)
     then show "prod_fun f g \<noteq> (\<lambda>k. 0)"
-      by (auto simp add: fun_eq_iff)
+      by (auto simp: fun_eq_iff)
   qed
 qed
 
@@ -954,7 +930,7 @@
       by (blast intro: less_funI)
   }
   with * show "less_fun (\<lambda>k. h k + f k) (\<lambda>k. h k + g k) \<or> (\<lambda>k. h k + f k) = (\<lambda>k. h k + g k)"
-    by (auto simp add: fun_eq_iff)
+    by (auto simp: fun_eq_iff)
 qed
 
 instance poly_mapping :: (linorder, "{ordered_comm_monoid_add, ordered_ab_semigroup_add_imp_le, cancel_comm_monoid_add, linorder}") linordered_cancel_ab_semigroup_add
@@ -1036,7 +1012,7 @@
 
 lemma range_one [simp]:
   "range 1 = {1}"
-  by transfer (auto simp add: when_def)
+  by transfer (auto simp: when_def)
 
 lemma keys_single [simp]:
   "keys (single k v) = (if v = 0 then {} else {k})"
@@ -1044,13 +1020,12 @@
 
 lemma range_single [simp]:
   "range (single k v) = (if v = 0 then {} else {v})"
-  by transfer (auto simp add: when_def)
+  by transfer (auto simp: when_def)
 
 lemma keys_mult:
   "keys (f * g) \<subseteq> {a + b | a b. a \<in> keys f \<and> b \<in> keys g}"
   apply transfer
-  apply (auto simp add: prod_fun_def dest!: mult_not_zero elim!: Sum_any.not_neutral_obtains_not_neutral)
-  apply blast
+  apply (force simp: prod_fun_def dest!: mult_not_zero elim!: Sum_any.not_neutral_obtains_not_neutral)
   done
 
 lemma setsum_keys_plus_distrib:
@@ -1064,13 +1039,7 @@
 proof -
   let ?A = "Poly_Mapping.keys p \<union> Poly_Mapping.keys q"
   have "?lhs = (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup p k + Poly_Mapping.lookup q k))"
-    apply(rule sum.mono_neutral_cong_left)
-       apply(simp_all add: Poly_Mapping.keys_add)
-     apply(transfer fixing: f)
-     apply(auto simp add: hom_0)[1]
-    apply(transfer fixing: f)
-    apply(auto simp add: hom_0)[1]
-    done
+    by(intro sum.mono_neutral_cong_left) (auto simp: sum.mono_neutral_cong_left hom_0 in_keys_iff lookup_add)
   also have "\<dots> = (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup p k) + f k (Poly_Mapping.lookup q k))"
     by(rule sum.cong)(simp_all add: hom_plus)
   also have "\<dots> = (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup p k)) + (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup q k))"
@@ -1138,14 +1107,14 @@
   shows "degree f - 1 \<in> keys f"
 proof -
   from assms have "keys f \<noteq> {}"
-    by (auto simp add: degree_def)
+    by (auto simp: degree_def)
   then show ?thesis unfolding degree_def
     by (simp add: mono_Max_commute [symmetric] mono_Suc)
 qed
 
 lemma in_keys_less_degree:
   "n \<in> keys f \<Longrightarrow> n < degree f"
-unfolding degree_def by transfer (auto simp add: Max_gr_iff)
+unfolding degree_def by transfer (auto simp: Max_gr_iff)
 
 lemma beyond_degree_lookup_zero:
   "degree f \<le> n \<Longrightarrow> lookup f n = 0"
@@ -1307,7 +1276,7 @@
   { fix x
     have "prod_fun (\<lambda>k'. s when 0 = k') p x =
           (\<Sum>l :: 'a. if l = 0 then s * (\<Sum>q. p q when x = q) else 0)"
-      by(auto simp add: prod_fun_def when_def intro: Sum_any.cong simp del: Sum_any.delta)
+      by(auto simp: prod_fun_def when_def intro: Sum_any.cong simp del: Sum_any.delta)
     also have "\<dots> = (\<lambda>k. s * p k when p k \<noteq> 0) x" by(simp add: when_def)
     also note calculation }
   then show "(\<lambda>k. s * p k when p k \<noteq> 0) = prod_fun (\<lambda>k'. s when 0 = k') p"
@@ -1316,10 +1285,10 @@
 
 lemma map_single [simp]:
   "(c = 0 \<Longrightarrow> f 0 = 0) \<Longrightarrow> map f (single x c) = single x (f c)"
-by transfer(auto simp add: fun_eq_iff when_def)
+  by transfer(auto simp: fun_eq_iff when_def)
 
 lemma map_eq_zero_iff: "map f p = 0 \<longleftrightarrow> (\<forall>k \<in> keys p. f (lookup p k) = 0)"
-by transfer(auto simp add: fun_eq_iff when_def)
+  by transfer(auto simp: fun_eq_iff when_def)
 
 subsection \<open>Canonical dense representation of @{typ "nat \<Rightarrow>\<^sub>0 'a"}\<close>
 
@@ -1345,7 +1314,7 @@
 proof (transfer, rule ext)
   fix n :: nat and v :: 'a
   show "nth_default 0 [v] n = (v when 0 = n)"
-    by (auto simp add: nth_default_def nth_append)
+    by (auto simp: nth_default_def nth_append)
 qed
 
 lemma nth_replicate [simp]:
@@ -1353,7 +1322,7 @@
 proof (transfer, rule ext)
   fix m n :: nat and v :: 'a
   show "nth_default 0 (replicate n 0 @ [v]) m = (v when n = m)"
-    by (auto simp add: nth_default_def nth_append)
+    by (auto simp: nth_default_def nth_append)
 qed
 
 lemma nth_strip_while [simp]:
@@ -1379,16 +1348,16 @@
   { fix n
     assume "nth_default 0 xs n \<noteq> 0"
     then have "n < length xs" and "xs ! n \<noteq> 0"
-      by (auto simp add: nth_default_def split: if_splits)
+      by (auto simp: nth_default_def split: if_splits)
     then have "(n, xs ! n) \<in> {(n, v). (n, v) \<in> set (enumerate 0 xs) \<and> v \<noteq> 0}" (is "?x \<in> ?A")
-      by (auto simp add: in_set_conv_nth enumerate_eq_zip)
+      by (auto simp: in_set_conv_nth enumerate_eq_zip)
     then have "fst ?x \<in> fst ` ?A"
       by blast
     then have "n \<in> fst ` {(n, v). (n, v) \<in> set (enumerate 0 xs) \<and> v \<noteq> 0}"
       by simp
   }
   then show "{k. nth_default 0 xs k \<noteq> 0} = fst ` {(n, v). (n, v) \<in> set (enumerate 0 xs) \<and> v \<noteq> 0}"
-    by (auto simp add: in_enumerate_iff_nth_default_eq)
+    by (auto simp: in_enumerate_iff_nth_default_eq)
 qed
 
 lemma range_nth [simp]:
@@ -1409,16 +1378,16 @@
     with * obtain n where n: "n < length xs" "xs ! n \<noteq> 0"
       by (fastforce simp add: no_trailing_unfold last_conv_nth neq_Nil_conv)
     then have "?bound = Max (Suc ` {k. (k < length xs \<longrightarrow> xs ! k \<noteq> (0::'a)) \<and> k < length xs})"
-      by (subst Max_insert) (auto simp add: nth_default_def)
+      by (subst Max_insert) (auto simp: nth_default_def)
     also let ?A = "{k. k < length xs \<and> xs ! k \<noteq> 0}"
     have "{k. (k < length xs \<longrightarrow> xs ! k \<noteq> (0::'a)) \<and> k < length xs} = ?A" by auto
     also have "Max (Suc ` ?A) = Suc (Max ?A)" using n
-      by (subst mono_Max_commute [where f = Suc, symmetric]) (auto simp add: mono_Suc)
+      by (subst mono_Max_commute [where f = Suc, symmetric]) (auto simp: mono_Suc)
     also {
       have "Max ?A \<in> ?A" using n Max_in [of ?A] by fastforce
       hence "Suc (Max ?A) \<le> length xs" by simp
       moreover from * False have "length xs - 1 \<in> ?A"
-        by(auto simp add: no_trailing_unfold last_conv_nth)
+        by(auto simp: no_trailing_unfold last_conv_nth)
       hence "length xs - 1 \<le> Max ?A" using Max_ge[of ?A "length xs - 1"] by auto
       hence "length xs \<le> Suc (Max ?A)" by simp
       ultimately have "Suc (Max ?A) = length xs" by simp }
@@ -1433,7 +1402,7 @@
 lemma nth_idem:
   "nth (List.map (lookup f) [0..<degree f]) = f"
   unfolding degree_def by transfer
-    (auto simp add: nth_default_def fun_eq_iff not_less)
+    (auto simp: nth_default_def fun_eq_iff not_less)
 
 lemma nth_idem_bound:
   assumes "degree f \<le> n"
@@ -1444,7 +1413,7 @@
   then have "[0..<n] = [0..<degree f] @ [degree f..<degree f + m]"
     by (simp add: upt_add_eq_append [of 0])
   moreover have "List.map (lookup f) [degree f..<degree f + m] = replicate m 0"
-    by (rule replicate_eqI) (auto simp add: beyond_degree_lookup_zero)
+    by (rule replicate_eqI) (auto simp: beyond_degree_lookup_zero)
   ultimately show ?thesis by (simp add: nth_idem)
 qed
 
@@ -1489,10 +1458,10 @@
   from assms have "sorted_list_of_set (set (List.map fst xs)) = List.map fst xs"
     unfolding sorted_list_of_set_sort_remdups by (simp add: distinct_remdups_id sort_key_id_if_sorted)
   moreover from assms have "keys (the_value xs) = fst ` set xs"
-    by transfer (auto simp add: image_def split: option.split dest: set_map_of_compr)
+    by transfer (auto simp: image_def split: option.split dest: set_map_of_compr)
   ultimately show ?thesis
     unfolding items_def using assms
-    by (auto simp add: lookup_the_value intro: map_idI)
+    by (auto simp: lookup_the_value intro: map_idI)
 qed
 
 lemma the_value_Nil [simp]:
@@ -1549,7 +1518,7 @@
   then have "f k + g (m k) = (\<Sum>k' \<in> ?keys. f k' + g (m k') when k' = k)"
     by (simp add: sum.delta when_def)
   also have "\<dots> < (\<Sum>k' \<in> ?keys. Suc (f k' + g (m k')))" using *
-    by (intro sum_strict_mono) (auto simp add: when_def)
+    by (intro sum_strict_mono) (auto simp: when_def)
   also have "\<dots> \<le> g 0 + \<dots>" by simp
   finally have "f k + g (m k) < \<dots>" .
   then show "f k + g (m k) < g 0 + (\<Sum>k | m k \<noteq> 0. Suc (f k + g (m k)))"
@@ -1599,7 +1568,7 @@
   "m = m' \<Longrightarrow> g 0 = g' 0 \<Longrightarrow> (\<And>k. k \<in> keys m' \<Longrightarrow> f k = f' k)
     \<Longrightarrow> (\<And>v. v \<in> range m' \<Longrightarrow> g v = g' v)
     \<Longrightarrow> poly_mapping_size f g m = poly_mapping_size f' g' m'"
-  by (auto simp add: poly_mapping_size_def intro!: sum.cong)
+  by (auto simp: poly_mapping_size_def intro!: sum.cong)
 
 instantiation poly_mapping :: (type, zero) size
 begin
@@ -1623,7 +1592,7 @@
 lemma mapp_cong [fundef_cong]:
   "\<lbrakk> m = m'; \<And>k. k \<in> keys m' \<Longrightarrow> f k (lookup m' k) = f' k (lookup m' k) \<rbrakk>
   \<Longrightarrow> mapp f m = mapp f' m'"
-  by transfer (auto simp add: fun_eq_iff)
+  by transfer (auto simp: fun_eq_iff)
 
 lemma lookup_mapp:
   "lookup (mapp f p) k = (f k (lookup p k) when k \<in> keys p)"
@@ -1688,8 +1657,6 @@
   
 
 lemma keys_cmul_iff [iff]: "i \<in> Poly_Mapping.keys (frag_cmul c x) \<longleftrightarrow> i \<in> Poly_Mapping.keys x \<and> c \<noteq> 0"
-  apply auto
-  apply (meson subsetD keys_cmul)
   by (metis in_keys_iff lookup_frag_cmul mult_eq_0_iff)
 
 lemma keys_minus [simp]: "Poly_Mapping.keys(-a) = Poly_Mapping.keys a"
@@ -1697,7 +1664,7 @@
 
 lemma keys_diff: 
   "Poly_Mapping.keys(a - b) \<subseteq> Poly_Mapping.keys a \<union> Poly_Mapping.keys b"
-  by (auto simp add: in_keys_iff lookup_minus)
+  by (auto simp: in_keys_iff lookup_minus)
 
 lemma keys_eq_empty [simp]: "Poly_Mapping.keys c = {} \<longleftrightarrow> c = 0"
   by (metis in_keys_iff keys_zero lookup_zero poly_mapping_eqI)
@@ -1769,10 +1736,11 @@
     by (auto simp: frag_extend_def Poly_Mapping.lookup_add frag_cmul_distrib)
   also have "... = (\<Sum>i \<in> Poly_Mapping.keys a \<union> Poly_Mapping.keys b. frag_cmul (poly_mapping.lookup a i) (f i) 
                          + frag_cmul (poly_mapping.lookup b i) (f i))"
-    apply (rule sum.mono_neutral_cong_left)
-    using keys_add [of a b]
-     apply (auto simp add: in_keys_iff plus_poly_mapping.rep_eq frag_cmul_distrib [symmetric])
-    done
+  proof (rule sum.mono_neutral_cong_left)
+    show "\<forall>i\<in>keys a \<union> keys b - keys (a + b).
+       frag_cmul (lookup a i) (f i) + frag_cmul (lookup b i) (f i) = 0"
+      by (metis DiffD2 frag_cmul_distrib frag_cmul_zero in_keys_iff lookup_add)
+  qed (auto simp: keys_add)
   also have "... = (frag_extend f a) + (frag_extend f b)"
     by (auto simp: * sum.distrib frag_extend_def)
   finally show ?thesis .
@@ -1814,9 +1782,15 @@
   shows "P(frag_cmul k c)"
 proof -
   have "P (frag_cmul (int n) c)" for n
-    apply (induction n)
-     apply (simp_all add: assms frag_cmul_distrib)
-    by (metis add.left_neutral add_diff_cancel_right' add_uminus_conv_diff P)
+  proof (induction n)
+    case 0
+    then show ?case
+      by (simp add: assms)
+  next
+    case (Suc n)
+    then show ?case
+      by (metis assms diff_0 diff_minus_eq_add frag_cmul_distrib frag_cmul_one of_nat_Suc)
+  qed
   then show ?thesis
     by (metis (no_types, opaque_lifting) add_diff_eq assms(2) diff_add_cancel frag_cmul_distrib int_diff_cases)
 qed
@@ -1840,14 +1814,11 @@
       by simp
     have Pfrag: "P (frag_cmul (poly_mapping.lookup c i) (frag_of i))"
       by (metis "0" diff frag_closure_minus_cmul insert.prems insert_subset sing subset_iff)
-    show ?case
-      apply (simp add: insert.hyps)
-      apply (subst ab)
-      using insert apply (blast intro: assms Pfrag)
-      done
+    with insert show ?case
+      by (metis (mono_tags, lifting) "0" ab diff insert_subset sum.insert)
   qed
   then show ?thesis
-    by (subst frag_expansion) (auto simp add: frag_extend_def)
+    by (subst frag_expansion) (auto simp: frag_extend_def)
 qed
 
 lemma frag_extend_compose: