--- a/src/HOL/List.thy Mon Nov 07 22:16:37 2022 +0100
+++ b/src/HOL/List.thy Tue Nov 08 08:41:29 2022 +0100
@@ -5882,7 +5882,11 @@
by (cases xs) auto
lemma sort_key_id_if_sorted: "sorted (map f xs) \<Longrightarrow> sort_key f xs = xs"
-by (induct xs) (auto simp add: insort_is_Cons)
+by (induction xs) (auto simp add: insort_is_Cons)
+
+text \<open>Subsumed by @{thm sort_key_id_if_sorted} but easier to find:\<close>
+lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
+by (simp add: sort_key_id_if_sorted)
lemma insort_key_remove1:
assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"