# HG changeset patch
# User nipkow
# Date 1704897013 -3600
# Node ID 8e3e9e6ca538e39fb3f989d155f5f9b83d19a3fc
# Parent  71fde9e76ca94635b7d45debd9e3405dbb67a747
added and removed lemmas

diff -r 71fde9e76ca9 -r 8e3e9e6ca538 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jan 10 10:25:55 2024 +0100
+++ b/src/HOL/List.thy	Wed Jan 10 15:30:13 2024 +0100
@@ -5377,14 +5377,13 @@
   finally show ?thesis by simp
 qed
 
-lemma finite_lists_distinct_length_eq [intro]:
+lemma finite_subset_distinct:
   assumes "finite A"
-  shows "finite {xs. length xs = n \<and> distinct xs \<and> set xs \<subseteq> A}" (is "finite ?S")
-proof -
-  have "finite {xs. set xs \<subseteq> A \<and> length xs = n}"
-    using \<open>finite A\<close> by (rule finite_lists_length_eq)
-  moreover have "?S \<subseteq> {xs. set xs \<subseteq> A \<and> length xs = n}" by auto
-  ultimately show ?thesis using finite_subset by auto
+  shows "finite {xs. set xs \<subseteq> A \<and> distinct xs}" (is "finite ?S")
+proof (rule finite_subset)
+  from assms show "?S \<subseteq> {xs. set xs \<subseteq> A \<and> length xs \<le> card A}"
+    by clarsimp (metis distinct_card card_mono)
+  from assms show "finite ..." by (rule finite_lists_length_le)
 qed
 
 lemma card_lists_distinct_length_eq: