--- a/src/HOL/Groups_Big.thy Mon Feb 14 16:41:48 2022 +0100
+++ b/src/HOL/Groups_Big.thy Tue Feb 15 13:00:05 2022 +0000
@@ -1226,7 +1226,7 @@
using assms card_eq_0_iff finite_UnionD by fastforce
qed
-lemma card_Union_le_sum_card:
+lemma card_Union_le_sum_card_weak:
fixes U :: "'a set set"
assumes "\<forall>u \<in> U. finite u"
shows "card (\<Union>U) \<le> sum card U"
@@ -1249,6 +1249,11 @@
qed
qed
+lemma card_Union_le_sum_card:
+ fixes U :: "'a set set"
+ shows "card (\<Union>U) \<le> sum card U"
+ by (metis Union_upper card.infinite card_Union_le_sum_card_weak finite_subset zero_le)
+
lemma card_UN_le:
assumes "finite I"
shows "card(\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. card(A i))"