# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1725009408 -3600
# Node ID 07c51801c2ea35a55161a004e50a1eff7fb2140b
# Parent  94bc8f62c835f06b03c7947c8beb1587695f8fe5
More tidying of old proofs

diff -r 94bc8f62c835 -r 07c51801c2ea src/HOL/Library/Equipollence.thy
--- a/src/HOL/Library/Equipollence.thy	Mon Aug 26 22:14:19 2024 +0100
+++ b/src/HOL/Library/Equipollence.thy	Fri Aug 30 10:16:48 2024 +0100
@@ -313,9 +313,7 @@
 
 lemma insert_eqpoll_cong:
      "\<lbrakk>A \<approx> B; a \<notin> A; b \<notin> B\<rbrakk> \<Longrightarrow> insert a A \<approx> insert b B"
-  apply (rule lepoll_antisym)
-  apply (simp add: eqpoll_imp_lepoll insert_lepoll_cong)+
-  by (meson eqpoll_imp_lepoll eqpoll_sym insert_lepoll_cong)
+  by (meson eqpoll_imp_lepoll eqpoll_sym insert_lepoll_cong lepoll_antisym)
 
 lemma insert_eqpoll_insert_iff:
      "\<lbrakk>a \<notin> A; b \<notin> B\<rbrakk> \<Longrightarrow> insert a A \<approx> insert b B  \<longleftrightarrow>  A \<approx> B"
@@ -346,8 +344,7 @@
 proof (induction A rule: finite_induct)
   case (insert x A)
   then show ?case
-    apply (auto simp: insert_absorb)
-    by (metis insert_commute insert_iff insert_lepoll_insertD)
+    by (metis insertI2 insert_lepoll_insert_iff insert_subsetI lepoll_trans subsetI subset_imp_lepoll)
 qed auto
 
 
@@ -489,9 +486,7 @@
     define \<chi> where "\<chi> \<equiv> \<lambda>z. THE x. x \<in> A \<and> z \<in> F x"
     have \<chi>: "\<chi> z = x" if "x \<in> A" "z \<in> F x" for x z
       unfolding \<chi>_def
-      apply (rule the_equality)
-      apply (simp add: that)
-      by (metis disj disjnt_iff pairwiseD that)
+      by (smt (verit, best) disj disjnt_iff pairwiseD that(1,2) theI_unique)
     let ?f = "\<lambda>z. (\<chi> z, b (\<chi> z) z)"
     show "inj_on ?f (\<Union>(F ` A))"
       unfolding inj_on_def
@@ -562,12 +557,18 @@
 qed
 
 lemma lepoll_funcset_right:
-   "B \<lesssim> B' \<Longrightarrow> A \<rightarrow>\<^sub>E B \<lesssim> A \<rightarrow>\<^sub>E B'"
-  apply (auto simp: lepoll_def inj_on_def)
-  apply (rule_tac x = "\<lambda>g. \<lambda>z \<in> A. f(g z)" in exI)
-  apply (auto simp: fun_eq_iff)
-  apply (metis PiE_E)
-  by blast
+  assumes "B \<lesssim> B'" shows "A \<rightarrow>\<^sub>E B \<lesssim> A \<rightarrow>\<^sub>E B'"
+proof -
+  obtain f where f: "inj_on f B" "f ` B \<subseteq> B'"
+    by (meson assms lepoll_def)
+  let ?G = "\<lambda>g. \<lambda>z \<in> A. f(g z)"
+  have "inj_on ?G (A \<rightarrow>\<^sub>E B)"
+    using f by (smt (verit, best) PiE_ext PiE_mem inj_on_def restrict_apply')
+  moreover have "?G ` (A \<rightarrow>\<^sub>E B) \<subseteq> (A \<rightarrow>\<^sub>E B')"
+    using f by fastforce
+  ultimately show ?thesis
+    by (meson lepoll_def)
+qed
 
 lemma lepoll_funcset_left:
   assumes "B \<noteq> {}" "A \<lesssim> A'"
@@ -588,10 +589,7 @@
     then have "?F k (f x) = ?F l (f x)"
       by simp
     then show "k x = l x"
-      apply (auto simp: h split: if_split_asm)
-      apply (metis PiE_arb h k l)
-      apply (metis (full_types) PiE_E h k l)
-      using fim k l by fastforce
+      by (smt (verit, best) PiE_arb fim h image_subset_iff k l restrict_apply')
   next
     show "?F ` (A \<rightarrow>\<^sub>E B) \<subseteq> A' \<rightarrow>\<^sub>E B"
       using \<open>b \<in> B\<close> by force
@@ -608,13 +606,13 @@
 proof -
   obtain f where f: "\<And>i. i \<in> A \<Longrightarrow> inj_on (f i) (B i) \<and> (f i) ` B i \<subseteq> C i"
     using assms unfolding lepoll_def by metis
-  then show ?thesis
-    unfolding lepoll_def
-    apply (rule_tac x = "\<lambda>g. \<lambda>i \<in> A. f i (g i)" in exI)
-    apply (auto simp: inj_on_def)
-     apply (rule PiE_ext, auto)
-     apply (metis (full_types) PiE_mem restrict_apply')
-    by blast
+  let ?G = "\<lambda>g. \<lambda>i \<in> A. f i (g i)"
+  have "inj_on ?G (PiE A B)"
+    by (smt (verit, ccfv_SIG) PiE_ext PiE_iff f inj_on_def restrict_apply')
+  moreover have "?G ` (PiE A B) \<subseteq> (PiE A C)"
+    using f by fastforce
+  ultimately show ?thesis
+    by (meson lepoll_def)
 qed
 
 
@@ -678,18 +676,15 @@
       also have "\<dots> = (UNIV::nat set) \<rightarrow>\<^sub>E (UNIV::bool set)"
         by auto
       also have "\<dots> \<lesssim> J \<rightarrow>\<^sub>E (UNIV::bool set)"
-        apply (rule lepoll_funcset_left)
-        using infinite_le_lepoll that by auto
+        by (metis empty_not_UNIV infinite_le_lepoll lepoll_funcset_left that)
       also have "\<dots> \<lesssim> Pi\<^sub>E J S"
       proof -
-        have *: "(UNIV::bool set) \<lesssim> S i" if "i \<in> I" and "\<forall>a. \<not> S i \<subseteq> {a}" for i
+        have *: "(UNIV::bool set) \<lesssim> S i" if "i \<in> I" and \<section>: "\<forall>a. \<not> S i \<subseteq> {a}" for i
         proof -
           obtain a b where "{a,b} \<subseteq> S i" "a \<noteq> b"
-            by (metis \<open>\<forall>a. \<not> S i \<subseteq> {a}\<close> all_not_in_conv empty_subsetI insertCI insert_subset set_eq_subset subsetI)
+            by (metis \<section> empty_subsetI insert_subset subsetI)
           then show ?thesis
-            apply (clarsimp simp: lepoll_def inj_on_def)
-            apply (rule_tac x="\<lambda>x. if x then a else b" in exI, auto)
-            done
+            by (metis Set.set_insert UNIV_bool insert_iff insert_lepoll_cong insert_subset singleton_lepoll)
         qed
         show ?thesis
           by (auto simp: * J_def intro: lepoll_PiE)
@@ -727,10 +722,12 @@
     have *: "finite (Pi\<^sub>E I S)"
       if "finite J" and "\<forall>i\<in>I. finite (S i)"
     proof (rule finite_subset)
-      show "Pi\<^sub>E I S \<subseteq> ?F"
-        apply safe
-        using J_def apply blast
+      have "\<And>f j. \<lbrakk>f \<in> Pi\<^sub>E I S; j \<in> J\<rbrakk> \<Longrightarrow> f j \<in> \<Union> (S ` J)"
+        using J_def by blast
+      moreover
+      have "\<And>f j. \<lbrakk>f \<in> Pi\<^sub>E I S; f j \<noteq> (if j \<in> I then a j else undefined)\<rbrakk> \<Longrightarrow> j \<in> J"
         by (metis DiffI PiE_E a singletonD)
+      ultimately show "Pi\<^sub>E I S \<subseteq> ?F" by force
       show "finite ?F"
       proof (rule finite_restricted_funspace [OF \<open>finite J\<close>])
         show "finite (\<Union> (S ` J))"
diff -r 94bc8f62c835 -r 07c51801c2ea src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Mon Aug 26 22:14:19 2024 +0100
+++ b/src/HOL/Library/FSet.thy	Fri Aug 30 10:16:48 2024 +0100
@@ -1174,15 +1174,13 @@
 
 lemma atomize_fBall:
     "(\<And>x. x |\<in>| A ==> P x) == Trueprop (fBall A (\<lambda>x. P x))"
-apply (simp only: atomize_all atomize_imp)
-apply (rule equal_intr_rule)
-  by (transfer, simp)+
+  by (simp add: Set.atomize_ball)
 
 lemma fBall_mono[mono]: "P \<le> Q \<Longrightarrow> fBall S P \<le> fBall S Q"
-by auto
+  by auto
 
 lemma fBex_mono[mono]: "P \<le> Q \<Longrightarrow> fBex S P \<le> fBex S Q"
-by auto
+  by auto
 
 end
 
@@ -1551,7 +1549,7 @@
 lemma fset_strong_cases:
   obtains "xs = {||}"
     | ys x where "x |\<notin>| ys" and "xs = finsert x ys"
-by transfer blast
+  by auto
 
 lemma fset_induct2:
   "P {||} {||} \<Longrightarrow>
@@ -1559,12 +1557,7 @@
   (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
   (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow>
   P xsa ysa"
-  apply (induct xsa arbitrary: ysa)
-  apply (induct_tac x rule: fset_induct_stronger)
-  apply simp_all
-  apply (induct_tac xa rule: fset_induct_stronger)
-  apply simp_all
-  done
+by (induct xsa arbitrary: ysa; metis fset_induct_stronger)
 
 
 subsection \<open>Lemmas depending on induction\<close>
@@ -1582,25 +1575,16 @@
 
 lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y)
   \<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
-apply (rule ext)+
-apply transfer'
-apply (subst rel_set_def[unfolded fun_eq_iff])
-by blast
+  by transfer' (metis (no_types, opaque_lifting) rel_set_def)
 
 lemma finite_rel_set:
   assumes fin: "finite X" "finite Z"
   assumes R_S: "rel_set (R OO S) X Z"
   shows "\<exists>Y. finite Y \<and> rel_set R X Y \<and> rel_set S Y Z"
 proof -
-  obtain f where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)"
-  apply atomize_elim
-  apply (subst bchoice_iff[symmetric])
-  using R_S[unfolded rel_set_def OO_def] by blast
-
-  obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
-  apply atomize_elim
-  apply (subst bchoice_iff[symmetric])
-  using R_S[unfolded rel_set_def OO_def] by blast
+  obtain f g where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)"
+               and g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
+    using R_S[unfolded rel_set_def OO_def] by metis
 
   let ?Y = "f ` X \<union> g ` Z"
   have "finite ?Y" by (simp add: fin)
@@ -1712,13 +1696,13 @@
 lemma ffilter_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "((A ===> (=)) ===> rel_fset A ===> rel_fset A) ffilter ffilter"
-  using assms unfolding rel_fun_def
-  using Lifting_Set.filter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
+  using assms Lifting_Set.filter_transfer
+  unfolding rel_fun_def by (metis ffilter.rep_eq rel_fset.rep_eq)
 
 lemma card_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_fset A ===> (=)) fcard fcard"
-  unfolding rel_fun_def
-  using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
+  using card_transfer unfolding rel_fun_def
+  by (metis fcard.rep_eq rel_fset.rep_eq)
 
 end
 
@@ -1734,13 +1718,10 @@
 
 lemma rel_fset_alt:
   "rel_fset R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
-by transfer (simp add: rel_set_def)
+  by transfer (simp add: rel_set_def)
 
 lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
-apply (rule f_the_inv_into_f[unfolded inj_on_def])
-apply (simp add: fset_inject)
-apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
-.
+  by (metis CollectI f_the_inv_into_f fset_cases fset_cong inj_onI rangeI)
 
 lemma rel_fset_aux:
 "(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
@@ -1761,10 +1742,7 @@
   qed (auto simp add: *)
 next
   assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
-  apply (simp add: subset_eq Ball_def)
-  apply (rule conjI)
-  apply (transfer, clarsimp, metis snd_conv)
-  by (transfer, clarsimp, metis fst_conv)
+    using Product_Type.Collect_case_prodD by blast
 qed
 
 bnf "'a fset"
@@ -1789,7 +1767,7 @@
 done
 
 lemma rel_fset_fset: "rel_set \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2"
-  by transfer (rule refl)
+  by (simp add: rel_fset.rep_eq)
 
 end
 
@@ -1801,11 +1779,13 @@
 
 subsection \<open>Size setup\<close>
 
-context includes fset.lifting begin
+context includes fset.lifting 
+begin
 lift_definition size_fset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a fset \<Rightarrow> nat" is "\<lambda>f. sum (Suc \<circ> f)" .
 end
 
-instantiation fset :: (type) size begin
+instantiation fset :: (type) size 
+begin
 definition size_fset where
   size_fset_overloaded_def: "size_fset = FSet.size_fset (\<lambda>_. 0)"
 instance ..
@@ -1820,8 +1800,8 @@
     folded size_fset_overloaded_def])
 
 lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)"
-  apply (subst fun_eq_iff)
-  including fset.lifting by transfer (auto intro: sum.reindex_cong subset_inj_on)
+  unfolding fun_eq_iff
+  by (simp add: inj_def inj_onI sum.reindex)
 
 setup \<open>
 BNF_LFP_Size.register_size_global \<^type_name>\<open>fset\<close> \<^const_name>\<open>size_fset\<close>
@@ -1901,16 +1881,11 @@
 subsubsection \<open>Countability\<close>
 
 lemma exists_fset_of_list: "\<exists>xs. fset_of_list xs = S"
-including fset.lifting
-by transfer (rule finite_list)
+  including fset.lifting
+  by transfer (rule finite_list)
 
 lemma fset_of_list_surj[simp, intro]: "surj fset_of_list"
-proof -
-  have "x \<in> range fset_of_list" for x :: "'a fset"
-    unfolding image_iff
-    using exists_fset_of_list by fastforce
-  thus ?thesis by auto
-qed
+  by (metis exists_fset_of_list surj_def)
 
 instance fset :: (countable) countable
 proof
diff -r 94bc8f62c835 -r 07c51801c2ea src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Aug 26 22:14:19 2024 +0100
+++ b/src/HOL/Library/Float.thy	Fri Aug 30 10:16:48 2024 +0100
@@ -103,8 +103,8 @@
   by (simp add: float_def) (metis mult_minus_left of_int_minus)
 
 lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float"
-  apply (clarsimp simp: float_def)
-  by (metis (no_types, opaque_lifting) of_int_add powr_add mult.assoc mult.left_commute of_int_mult)
+  apply (clarsimp simp: float_def mult_ac)
+  by (metis mult.assoc of_int_mult of_int_add powr_add)
 
 lemma minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x - y \<in> float"
   using plus_float [of x "- y"] by simp
@@ -248,10 +248,7 @@
 end
 
 lemma float_numeral[simp]: "real_of_float (numeral x :: float) = numeral x"
-proof (induct x)
-  case One
-  then show ?case by simp
-qed (metis of_int_numeral real_of_float_of_int_eq)+
+  by (metis of_int_numeral real_of_float_of_int_eq)
 
 lemma transfer_numeral [transfer_rule]:
   "rel_fun (=) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
@@ -525,10 +522,7 @@
     then have "mantissa f = m * 2^nat (e - exponent f)"
       by linarith
     with \<open>exponent f < e\<close> have "2 dvd mantissa f"
-      apply (intro dvdI[where k="m * 2^(nat (e-exponent f)) div 2"])
-      apply (cases "nat (e - exponent f)")
-      apply auto
-      done
+      by (force intro: dvdI[where k="m * 2^(nat (e-exponent f)) div 2"])
     then show False using mantissa_not_dvd[OF not_0] by simp
   qed
   ultimately have "real_of_int m = mantissa f * 2^nat (exponent f - e)"
@@ -843,15 +837,7 @@
   then have ne: "real_of_int (a mod b) / real_of_int b \<noteq> 0"
     using \<open>b \<noteq> 0\<close> by auto
   have "\<lceil>real_of_int a / real_of_int b\<rceil> = \<lfloor>real_of_int a / real_of_int b\<rfloor> + 1"
-    apply (rule ceiling_eq)
-    apply (auto simp flip: floor_divide_of_int_eq)
-  proof -
-    have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<le> real_of_int a / real_of_int b"
-      by simp
-    moreover have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<noteq> real_of_int a / real_of_int b"
-      by (smt (verit) floor_divide_of_int_eq ne of_int_div_aux)
-    ultimately show "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> < real_of_int a / real_of_int b" by arith
-  qed
+    by (metis add_cancel_left_right ceiling_altdef floor_divide_of_int_eq ne of_int_div_aux)
   then show ?thesis
     using \<open>\<not> b dvd a\<close> by simp
 qed
@@ -967,11 +953,12 @@
 proof -
   have "0 \<le> log 2 x - real_of_int \<lfloor>log 2 x\<rfloor>"
     by (simp add: algebra_simps)
-  with assms
-  show ?thesis
-    apply (auto simp: truncate_down_def round_down_def mult_powr_eq
+  moreover have "0 \<le> real p - real_of_int \<lfloor>log 2 x\<rfloor> + log 2 x"
+    by linarith
+  ultimately show ?thesis
+    using assms
+    by (auto simp: truncate_down_def round_down_def mult_powr_eq
       intro!: ge_one_powr_ge_zero mult_pos_pos)
-    by linarith
 qed
 
 lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y"
@@ -2119,8 +2106,7 @@
       assume [simp]: "odd j"
       have "power_up prec 0 (Suc (j div 2)) \<le> - power_up prec b (Suc (j div 2))"
         if "b < 0" "even (j div 2)"
-        apply (rule order_trans[where y=0])
-        using IH that by (auto simp: div2_less_self)
+        by (metis Suc_neq_Zero even_Suc neg_0_le_iff_le power_up_eq_zero_iff power_up_nonpos_iff that)
       then have "truncate_up prec ((power_up prec a (Suc (j div 2)))\<^sup>2)
         \<le> truncate_up prec ((power_up prec b (Suc (j div 2)))\<^sup>2)"
         using IH
@@ -2307,9 +2293,7 @@
 qualified lemma compute_floor_fl[code]:
   "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
   apply transfer
-  apply (simp add: powr_int floor_divide_of_int_eq)
-  apply (metis floor_divide_of_int_eq of_int_eq_numeral_power_cancel_iff)
-  done
+  using compute_int_floor_fl int_floor_fl.rep_eq powr_int by auto
 
 end
 
diff -r 94bc8f62c835 -r 07c51801c2ea src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Mon Aug 26 22:14:19 2024 +0100
+++ b/src/HOL/Library/FuncSet.thy	Fri Aug 30 10:16:48 2024 +0100
@@ -259,9 +259,7 @@
   by (auto simp add: bij_betw_def inj_on_def compose_eq)
 
 lemma bij_betw_compose: "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (compose A g f) A C"
-  apply (simp add: bij_betw_def compose_eq inj_on_compose)
-  apply (auto simp add: compose_def image_def)
-  done
+  by (simp add: bij_betw_def inj_on_compose surj_compose)
 
 lemma bij_betw_restrict_eq [simp]: "bij_betw (restrict f A) A B = bij_betw f A B"
   by (simp add: bij_betw_def)
@@ -298,15 +296,10 @@
   by (unfold inv_into_def) (fast intro: someI2)
 
 lemma compose_inv_into_id: "bij_betw f A B \<Longrightarrow> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)"
-  apply (simp add: bij_betw_def compose_def)
-  apply (rule restrict_ext, auto)
-  done
+  by (smt (verit, best) bij_betwE bij_betw_inv_into_left compose_def restrict_apply' restrict_ext)
 
 lemma compose_id_inv_into: "f ` A = B \<Longrightarrow> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)"
-  apply (simp add: compose_def)
-  apply (rule restrict_ext)
-  apply (simp add: f_inv_into_f)
-  done
+  by (smt (verit, best) compose_def f_inv_into_f restrict_apply' restrict_ext)
 
 lemma extensional_insert[intro, simp]:
   assumes "a \<in> extensional (insert i I)"
@@ -538,12 +531,15 @@
   "(\<lambda>f. f i) ` (PiE I S) = (if PiE I S = {} then {} else if i \<in> I then S i else {undefined})"
 proof -
   have "(\<lambda>f. f i) ` Pi\<^sub>E I S = S i" if "i \<in> I" "f \<in> PiE I S" for f
-    using that apply auto
-    by (rule_tac x="(\<lambda>k. if k=i then x else f k)" in image_eqI) auto
-  moreover have "(\<lambda>f. f i) ` Pi\<^sub>E I S = {undefined}" if "f \<in> PiE I S" "i \<notin> I" for f
-    using that by (blast intro: PiE_arb [OF that, symmetric])
-  ultimately show ?thesis
-    by auto
+  proof -
+    have "x \<in> S i \<Longrightarrow> \<exists>f\<in>Pi\<^sub>E I S. x = f i" for x
+      using that
+      by (force intro: bexI [where x="\<lambda>k. if k=i then x else f k"]) 
+    then show ?thesis
+      using that by force
+  qed
+  then show ?thesis
+    by (smt (verit) PiE_arb equals0I image_cong image_constant image_empty)
 qed
 
 lemma PiE_singleton:
@@ -563,9 +559,12 @@
   by (metis (mono_tags, lifting) PiE_eq PiE_singleton insert_not_empty restrict_apply' restrict_extensional)
 
 lemma PiE_over_singleton_iff: "(\<Pi>\<^sub>E x\<in>{a}. B x) = (\<Union>b \<in> B a. {\<lambda>x \<in> {a}. b})"
-  apply (auto simp: PiE_iff split: if_split_asm)
-  apply (metis (no_types, lifting) extensionalityI restrict_apply' restrict_extensional singletonD)
-  done
+proof -
+  have "\<And>x. \<lbrakk>x a \<in> B a; x \<in> extensional {a}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>B a. x = (\<lambda>x\<in>{a}. xa)"
+    using PiE_singleton by fastforce
+  then show ?thesis
+    by (auto simp: PiE_iff split: if_split_asm)
+qed
 
 lemma all_PiE_elements:
    "(\<forall>z \<in> PiE I S. \<forall>i \<in> I. P i (z i)) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. \<forall>x \<in> S i. P i x)" (is "?lhs = ?rhs")
@@ -582,7 +581,7 @@
       have "(\<lambda>j \<in> I. if j=i then x else f j) \<in> PiE I S"
         by (simp add: f that(2))
       then have "P i ((\<lambda>j \<in> I. if j=i then x else f j) i)"
-        using L that(1) by blast
+        using L that by blast
       with that show ?thesis
         by simp
     qed
@@ -608,26 +607,30 @@
   assumes "x \<notin> S"
   shows "{f. f \<in> (insert x S) \<rightarrow>\<^sub>E T \<and> inj_on f (insert x S)} =
     (\<lambda>(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
-  using assms
-  apply (auto del: PiE_I PiE_E)
-  apply (auto intro: extensional_funcset_fun_upd_inj_onI
-    extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
-  apply (auto simp add: image_iff inj_on_def)
-  apply (rule_tac x="xa x" in exI)
-  apply (auto intro: PiE_mem del: PiE_I PiE_E)
-  apply (rule_tac x="xa(x := undefined)" in exI)
-  apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
-  apply (auto dest!: PiE_mem split: if_split_asm)
-  done
+proof -
+  have "\<And>a f y. \<lbrakk>f \<in> S \<rightarrow>\<^sub>E T - {a}; a = (if y = x then a else f y); y \<in> S\<rbrakk>
+       \<Longrightarrow> False"
+    using assms by (auto dest!: PiE_mem split: if_split_asm)
+  moreover
+  have "\<And>f. \<lbrakk> f \<in> insert x S \<rightarrow>\<^sub>E T; inj_on f S; \<forall>xb\<in>S. f x \<noteq> f xb\<rbrakk>
+          \<Longrightarrow> \<exists>b. b \<in> S \<rightarrow>\<^sub>E T - {f x} \<and> inj_on b S \<and> f = b(x := f x)"
+    unfolding inj_on_def
+    by (smt (verit, ccfv_threshold) PiE_restrict fun_upd_apply fun_upd_triv insert_Diff insert_iff
+        restrict_PiE_iff restrict_upd)
+  ultimately show ?thesis
+    using assms
+    apply (auto simp: image_iff  intro: extensional_funcset_fun_upd_inj_onI
+        extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
+    apply (smt (verit, best) PiE_cong PiE_mem inj_on_def insertCI)
+    by blast
+qed
 
 lemma extensional_funcset_extend_domain_inj_onI:
   assumes "x \<notin> S"
   shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
   using assms
-  apply (auto intro!: inj_onI)
-  apply (metis fun_upd_same)
-  apply (metis assms PiE_arb fun_upd_triv fun_upd_upd)
-  done
+  apply (simp add: inj_on_def)
+  by (metis PiE_restrict fun_upd_apply restrict_fupd)
 
 
 subsubsection \<open>Misc properties of functions, composition and restriction from HOL Light\<close>
diff -r 94bc8f62c835 -r 07c51801c2ea src/HOL/Library/Interval.thy
--- a/src/HOL/Library/Interval.thy	Mon Aug 26 22:14:19 2024 +0100
+++ b/src/HOL/Library/Interval.thy	Fri Aug 30 10:16:48 2024 +0100
@@ -564,16 +564,7 @@
   using that
   apply transfer
   apply (clarsimp simp add: Let_def)
-  apply (intro conjI)
-         apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-        apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-       apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-      apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-     apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-    apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-   apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-  apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
-  done
+  by (smt (verit, best) linorder_le_cases max.coboundedI1 max.coboundedI2 min.absorb1 min.coboundedI2 mult_left_mono mult_left_mono_neg)
 
 lemma set_of_distrib_left:
   "set_of (B * (A1 + A2)) \<subseteq> set_of (B * A1 + B * A2)"
@@ -595,19 +586,7 @@
   "set_of ((A1 + A2) * B) \<subseteq> set_of (A1 * B + A2 * B)"
   for A1 A2 B :: "'a::{linordered_ring, real_normed_algebra, linear_continuum_topology} interval"
   unfolding set_of_times set_of_plus set_plus_def
-  apply clarsimp
-  subgoal for b a1 a2
-    apply (rule exI[where x="a1 * b"])
-    apply (rule conjI)
-    subgoal by force
-    subgoal
-      apply (rule exI[where x="a2 * b"])
-      apply (rule conjI)
-      subgoal by force
-      subgoal by (simp add: algebra_simps)
-      done
-    done
-  done
+  using distrib_right by blast
 
 lemma set_of_mul_inc_left:
   "set_of (A * B) \<subseteq> set_of (A' * B)"
@@ -671,10 +650,7 @@
       mult_bounds_enclose_zero1 mult_bounds_enclose_zero2)
 
 instance "interval" :: ("{linordered_semiring, zero, times}") mult_zero
-  apply standard
-  subgoal by transfer auto
-  subgoal by transfer auto
-  done
+  by (standard; transfer; auto)
 
 lift_definition min_interval::"'a::linorder interval \<Rightarrow> 'a interval \<Rightarrow> 'a interval" is
   "\<lambda>(l1, u1). \<lambda>(l2, u2). (min l1 l2, min u1 u2)"
diff -r 94bc8f62c835 -r 07c51801c2ea src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Mon Aug 26 22:14:19 2024 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Fri Aug 30 10:16:48 2024 +0100
@@ -135,53 +135,50 @@
 begin
 
 lemma size0: "0 < n"
-using size1 by simp
+  using size1 by simp
 
 lemmas definitions =
   zero_def one_def add_def mult_def minus_def diff_def
 
 lemma Rep_less_n: "Rep x < n"
-by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
+  by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
 
 lemma Rep_le_n: "Rep x \<le> n"
-by (rule Rep_less_n [THEN order_less_imp_le])
+  by (rule Rep_less_n [THEN order_less_imp_le])
 
 lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y"
-by (rule type_definition.Rep_inject [OF type, symmetric])
+  by (rule type_definition.Rep_inject [OF type, symmetric])
 
 lemma Rep_inverse: "Abs (Rep x) = x"
-by (rule type_definition.Rep_inverse [OF type])
+  by (rule type_definition.Rep_inverse [OF type])
 
 lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m"
-by (rule type_definition.Abs_inverse [OF type])
+  by (rule type_definition.Abs_inverse [OF type])
 
 lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
   using size0 by (simp add: Abs_inverse)
 
 lemma Rep_Abs_0: "Rep (Abs 0) = 0"
-by (simp add: Abs_inverse size0)
+  by (simp add: Abs_inverse size0)
 
 lemma Rep_0: "Rep 0 = 0"
-by (simp add: zero_def Rep_Abs_0)
+  by (simp add: zero_def Rep_Abs_0)
 
 lemma Rep_Abs_1: "Rep (Abs 1) = 1"
-by (simp add: Abs_inverse size1)
+  by (simp add: Abs_inverse size1)
 
 lemma Rep_1: "Rep 1 = 1"
-by (simp add: one_def Rep_Abs_1)
+  by (simp add: one_def Rep_Abs_1)
 
 lemma Rep_mod: "Rep x mod n = Rep x"
-apply (rule_tac x=x in type_definition.Abs_cases [OF type])
-apply (simp add: type_definition.Abs_inverse [OF type])
-done
+  using type_definition.Abs_cases [OF type]
+  by (metis Abs_inverse atLeastLessThan_iff mod_pos_pos_trivial)
 
 lemmas Rep_simps =
   Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
 
 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
-apply (intro_classes, unfold definitions)
-apply (simp_all add: Rep_simps mod_simps field_simps)
-done
+  by intro_classes (auto simp: Rep_simps mod_simps field_simps definitions)
 
 end
 
@@ -192,20 +189,13 @@
 begin
 
 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
-apply (induct k)
-apply (simp add: zero_def)
-apply (simp add: Rep_simps add_def one_def mod_simps ac_simps)
-done
+  by  (induct k) (simp_all add: zero_def Rep_simps add_def one_def mod_simps ac_simps)
 
 lemma of_int_eq: "of_int z = Abs (z mod n)"
-apply (cases z rule: int_diff_cases)
-apply (simp add: Rep_simps of_nat_eq diff_def mod_simps)
-done
+  by (cases z rule: int_diff_cases) (simp add: Rep_simps of_nat_eq diff_def mod_simps)
 
-lemma Rep_numeral:
-  "Rep (numeral w) = numeral w mod n"
-using of_int_eq [of "numeral w"]
-by (simp add: Rep_inject_sym Rep_Abs_mod)
+lemma Rep_numeral: "Rep (numeral w) = numeral w mod n"
+  by (metis Rep_Abs_mod of_int_eq of_int_numeral)
 
 lemma iszero_numeral:
   "iszero (numeral w::'a) \<longleftrightarrow> numeral w mod n = 0"
@@ -214,14 +204,11 @@
 lemma cases:
   assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P"
   shows "P"
-apply (cases x rule: type_definition.Abs_cases [OF type])
-apply (rule_tac z="y" in 1)
-apply (simp_all add: of_int_eq)
-done
+  by (metis Rep_inverse Rep_less_n Rep_mod assms of_int_eq pos_mod_sign size0)
 
 lemma induct:
   "(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)"
-by (cases x rule: cases) simp
+  by (cases x rule: cases) simp
 
 lemma UNIV_eq: "(UNIV :: 'a set) = Abs ` {0..<n}"
   using type type_definition.univ by blast
@@ -304,7 +291,7 @@
   mod_type "int CARD('a::finite bit1)"
            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
-apply (rule mod_type.intro)
+  apply (rule mod_type.intro)
 apply (simp add: type_definition_bit1)
 apply (rule one_less_int_card)
 apply (rule zero_bit1_def)