diff -r 766a07ff7a07 -r 98571d7e4a7d src/HOL/List.thy
--- a/src/HOL/List.thy	Sun May 04 15:05:51 2025 +0200
+++ b/src/HOL/List.thy	Sun May 04 20:50:01 2025 +0200
@@ -2440,6 +2440,19 @@
 lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
   by (simp add: set_conv_nth) force
 
+lemma set_list_update:
+  "set (xs [i := k]) = insert k (set (take i xs) \<union> set (drop (Suc i) xs))"
+  if \<open>i < length xs\<close>
+using that proof (induct xs arbitrary: i)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons x xs i)
+  then show ?case
+    by (cases i) (simp_all add: insert_commute)
+qed
+
 
 subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>