merged

--- a/src/HOL/Groups_Big.thy	Sat Aug 01 17:43:30 2020 +0000
+++ b/src/HOL/Groups_Big.thy	Mon Aug 03 11:46:19 2020 +0100
@@ -165,6 +165,11 @@
   shows "F g A = F h B"
   using assms by (simp add: reindex)
 
+lemma image_eq:
+  assumes "inj_on g A"  
+  shows "F (\<lambda>x. x) (g ` A) = F g A"
+  using assms reindex_cong by fastforce
+
 lemma UNION_disjoint:
   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"

--- a/src/HOL/Library/Infinite_Set.thy	Sat Aug 01 17:43:30 2020 +0000
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Aug 03 11:46:19 2020 +0100
@@ -484,7 +484,7 @@
 
 lemma finite_enumerate_initial_segment:
   fixes S :: "'a::wellorder set"
-  assumes "finite S" "s \<in> S" and n: "n < card (S \<inter> {..<s})"
+  assumes "finite S" and n: "n < card (S \<inter> {..<s})"
   shows "enumerate (S \<inter> {..<s}) n = enumerate S n"
   using n
 proof (induction n)
@@ -502,18 +502,20 @@
   case (Suc n)
   then have less_card: "Suc n < card S"
     by (meson assms(1) card_mono inf_sup_ord(1) leD le_less_linear order.trans)
-  obtain t where t: "t \<in> {s \<in> S. enumerate S n < s}"
+  obtain T where T: "T \<in> {s \<in> S. enumerate S n < s}"
     by (metis Infinite_Set.enumerate_step enumerate_in_set finite_enumerate_in_set finite_enumerate_step less_card mem_Collect_eq)
-  have "(LEAST x. x \<in> S \<and> x < s \<and> enumerate S n < x) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
+  have "(LEAST x. x \<in> S \<and> x < s \<and> enumerate S n < x) = (LEAST x. x \<in> S \<and> enumerate S n < x)"
        (is "_ = ?r")
   proof (intro Least_equality conjI)
     show "?r \<in> S"
-      by (metis (mono_tags, lifting) LeastI mem_Collect_eq t)
-    show "?r < s"
-      using not_less_Least [of _ "\<lambda>t. t \<in> S \<and> enumerate S n < t"] Suc assms 
-      by (metis (no_types, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def linorder_cases)
+      by (metis (mono_tags, lifting) LeastI mem_Collect_eq T)
+    have "\<not> s \<le> ?r"
+      using not_less_Least [of _ "\<lambda>x. x \<in> S \<and> enumerate S n < x"] Suc assms
+      by (metis (mono_tags, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def less_le_trans)
+    then show "?r < s"
+      by auto
     show "enumerate S n < ?r"
-      by (metis (no_types, lifting) LeastI mem_Collect_eq t)
+      by (metis (no_types, lifting) LeastI mem_Collect_eq T)
   qed (auto simp: Least_le)
   then show ?case
     using Suc assms by (simp add: finite_enumerate_Suc'' less_card)