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>