src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Mon Mar 04 21:58:53 2024 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Mar 05 14:32:50 2024 +0000
@@ -1873,6 +1873,11 @@
     by (simp add: card_Diff_subset)
 qed
 
+lemma card_Int_Diff:
+  assumes "finite A"
+  shows "card A = card (A \<inter> B) + card (A - B)"
+  by (simp add: assms card_Diff_subset_Int card_mono)
+
 lemma diff_card_le_card_Diff:
   assumes "finite B"
   shows "card A - card B \<le> card (A - B)"