diff -r 06350a8745c9 -r 362d750f5788 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Aug 01 14:07:34 2024 +0200
+++ b/src/HOL/List.thy	Fri Aug 02 18:25:18 2024 +0200
@@ -6629,14 +6629,33 @@
 lemma lexn_conv:
   "lexn r n =
     {(xs,ys). length xs = n \<and> length ys = n \<and>
-    (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y) \<in> r)}"
+    (\<exists>xys x y xs' ys'. xs = xys @ x#xs' \<and> ys = xys @ y # ys' \<and> (x, y) \<in> r)}"
+  (is "?L n = ?R n" is "_ = {(xs,ys). ?len n xs \<and> ?len n ys \<and> (\<exists>xys. ?P xs ys xys)}")
 proof (induction n)
   case (Suc n)
+(* A compact proof referring to a system-generated name:
   then show ?case
-    apply (simp add: image_Collect lex_prod_def, safe, blast)
-     apply (rule_tac x = "ab # xys" in exI, simp)
-    apply (case_tac xys; force)
+    apply (auto simp add: image_Collect lex_prod_def)
+    apply blast
+    apply (meson Cons_eq_appendI)
+    apply (case_tac xys; fastforce)
     done
+*)
+  have "(xs,ys) \<in> ?L (Suc n)" if r: "(xs,ys) \<in> ?R (Suc n)" for xs ys
+  proof -
+    from r obtain xys where r': "?len (Suc n) xs" "?len (Suc n) ys" "?P xs ys xys" by auto
+    then show ?thesis
+    proof (cases xys)
+      case Nil
+      thus ?thesis using r' by (auto simp: image_Collect lex_prod_def)
+    next
+      case Cons
+      thus ?thesis using r' Suc by (fastforce simp: image_Collect lex_prod_def)
+    qed
+  qed
+  moreover have "(xs,ys) \<in> ?L (Suc n) \<Longrightarrow> (xs,ys) \<in> ?R (Suc n)" for xs ys
+    using Suc by (auto simp add: image_Collect lex_prod_def)(blast, meson Cons_eq_appendI)
+  ultimately show ?case by (meson pred_equals_eq2)
 qed auto
 
 text\<open>By Mathias Fleury:\<close>