feat: (s ∩ t).card = s.card + t.card - (s ∪ t).card (#10224)

YaelDillies · YaelDillies · commit 80bf34f135fe · 2024-02-11T21:58:26.000Z
once coerced to an `AddGroupWithOne`. Also unify `Finset.card_disjoint_union` and `Finset.card_union_eq`

From LeanAPAP
diff --git a/Mathlib/Combinatorics/SetFamily/CauchyDavenport.lean b/Mathlib/Combinatorics/SetFamily/CauchyDavenport.lean
@@ -167,7 +167,7 @@ lemma Finset.min_le_card_mul (hs : s.Nonempty) (ht : t.Nonempty) :
   obtain hgt | hgt := disjoint_or_nonempty_inter t (g⁻¹ • t)
   · rw [← card_smul_finset g⁻¹ t]
     refine' Or.inr ((add_le_add_right hst _).trans _)
-    rw [← card_union_eq hgt]
+    rw [← card_union_of_disjoint hgt]
     exact (card_le_card_mul_left _ hgs).trans (le_add_of_le_left aux1)
   -- Else, we're done by induction on either `(s', t')` or `(s'', t'')` depending on whether
   -- `|s| + |t| ≤ |s'| + |t'|` or `|s| + |t| < |s''| + |t''|`. One of those two inequalities must
diff --git a/Mathlib/Combinatorics/SetFamily/Compression/Down.lean b/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
@@ -283,7 +283,7 @@ theorem compression_idem (a : α) (𝒜 : Finset (Finset α)) : 𝓓 a (𝓓 a 
 @[simp]
 theorem card_compression (a : α) (𝒜 : Finset (Finset α)) : (𝓓 a 𝒜).card = 𝒜.card := by
   rw [compression, card_disjUnion, filter_image,
-    card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_disjoint_union]
+    card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_union_of_disjoint]
   · conv_rhs => rw [← filter_union_filter_neg_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
   · exact disjoint_filter_filter_neg 𝒜 𝒜 (fun s => (erase s a ∈ 𝒜))
   intro s hs
diff --git a/Mathlib/Combinatorics/SetFamily/Compression/UV.lean b/Mathlib/Combinatorics/SetFamily/Compression/UV.lean
@@ -212,8 +212,8 @@ theorem compression_idem (u v : α) (s : Finset α) : 𝓒 u v (𝓒 u v s) = 
 /-- Compressing a family doesn't change its size. -/
 @[simp]
 theorem card_compression (u v : α) (s : Finset α) : (𝓒 u v s).card = s.card := by
-  rw [compression, card_disjoint_union compress_disjoint, filter_image,
-    card_image_of_injOn compress_injOn, ← card_disjoint_union (disjoint_filter_filter_neg s _ _),
+  rw [compression, card_union_of_disjoint compress_disjoint, filter_image,
+    card_image_of_injOn compress_injOn, ← card_union_of_disjoint (disjoint_filter_filter_neg s _ _),
     filter_union_filter_neg_eq]
 #align uv.card_compression UV.card_compression
 
@@ -297,7 +297,7 @@ variable [DecidableEq α] {𝒜 : Finset (Finset α)} {u v a : Finset α} {r : 
 theorem card_compress (huv : u.card = v.card) (a : Finset α) : (compress u v a).card = a.card := by
   unfold compress
   split_ifs with h
-  · rw [card_sdiff (h.2.trans le_sup_left), sup_eq_union, card_disjoint_union h.1.symm, huv,
+  · rw [card_sdiff (h.2.trans le_sup_left), sup_eq_union, card_union_of_disjoint h.1.symm, huv,
       add_tsub_cancel_right]
   · rfl
 #align uv.card_compress UV.card_compress
diff --git a/Mathlib/Combinatorics/SetFamily/LYM.lean b/Mathlib/Combinatorics/SetFamily/LYM.lean
@@ -190,7 +190,7 @@ theorem le_card_falling_div_choose [Fintype α] (hk : k ≤ Fintype.card α)
     exact card_le_card (slice_subset_falling _ _)
   rw [succ_eq_add_one] at *
   rw [sum_range_succ, ← slice_union_shadow_falling_succ,
-    card_disjoint_union (IsAntichain.disjoint_slice_shadow_falling h𝒜), cast_add, _root_.add_div,
+    card_union_of_disjoint (IsAntichain.disjoint_slice_shadow_falling h𝒜), cast_add, _root_.add_div,
     add_comm]
   rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left hk)]
   exact
diff --git a/Mathlib/Combinatorics/SetFamily/Shatter.lean b/Mathlib/Combinatorics/SetFamily/Shatter.lean
@@ -120,7 +120,7 @@ lemma card_le_card_shatterer (𝒜 : Finset (Finset α)) : 𝒜.card ≤ 𝒜.sh
     exact fun s _ ↦ aux (fun t ht ↦ (mem_filter.1 ht).2)
   rw [← card_memberSubfamily_add_card_nonMemberSubfamily a]
   refine (add_le_add ih₁ ih₀).trans ?_
-  rw [← card_union_add_card_inter, ← hℬ, ← card_disjoint_union]
+  rw [← card_union_add_card_inter, ← hℬ, ← card_union_of_disjoint]
   swap
   · simp only [disjoint_left, mem_union, mem_shatterer, mem_image, not_exists, not_and]
     rintro _ (hs | hs) s - rfl
diff --git a/Mathlib/Combinatorics/SimpleGraph/Density.lean b/Mathlib/Combinatorics/SimpleGraph/Density.lean
@@ -78,7 +78,7 @@ variable (r)
 theorem card_interedges_add_card_interedges_compl (s : Finset α) (t : Finset β) :
     (interedges r s t).card + (interedges (fun x y ↦ ¬r x y) s t).card = s.card * t.card := by
   classical
-  rw [← card_product, interedges, interedges, ← card_union_eq, filter_union_filter_neg_eq]
+  rw [← card_product, interedges, interedges, ← card_union_of_disjoint, filter_union_filter_neg_eq]
   exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2
 #align rel.card_interedges_add_card_interedges_compl Rel.card_interedges_add_card_interedges_compl
 
@@ -378,7 +378,7 @@ theorem card_interedges_add_card_interedges_compl (h : Disjoint s t) :
     refine' filter_congr fun x hx ↦ _
     rw [mem_product] at hx
     rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
-  rw [this, ← card_union_eq, filter_union_filter_neg_eq]
+  rw [this, ← card_union_of_disjoint, filter_union_filter_neg_eq]
   exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2
 #align simple_graph.card_interedges_add_card_interedges_compl SimpleGraph.card_interedges_add_card_interedges_compl
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
@@ -243,7 +243,7 @@ theorem degree_compl [Fintype (Gᶜ.neighborSet v)] [Fintype V] :
     Gᶜ.degree v = Fintype.card V - 1 - G.degree v := by
   classical
     rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
-    simp [card_disjoint_union (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v))]
+    simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v))]
 #align simple_graph.degree_compl SimpleGraph.degree_compl
 
 instance incidenceSetFintype [DecidableEq V] : Fintype (G.incidenceSet v) :=
diff --git a/Mathlib/Combinatorics/SimpleGraph/Operations.lean b/Mathlib/Combinatorics/SimpleGraph/Operations.lean
@@ -102,7 +102,7 @@ theorem card_edgeFinset_replaceVertex_of_not_adj (hn : ¬G.Adj s t) :
     (G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t := by
   have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
   rw [G.edgeFinset_replaceVertex_of_not_adj hn,
-    card_disjoint_union G.disjoint_sdiff_neighborFinset_image, card_sdiff inc,
+    card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff inc,
     tsub_add_eq_add_tsub <| card_le_card inc, card_incidenceFinset_eq_degree]
   congr 2
   rw [card_image_of_injective, card_neighborFinset_eq_degree]
@@ -113,7 +113,7 @@ theorem card_edgeFinset_replaceVertex_of_adj (ha : G.Adj s t) :
     (G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t - 1 := by
   have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
   rw [G.edgeFinset_replaceVertex_of_adj ha, card_sdiff (by simp [ha]),
-    card_disjoint_union G.disjoint_sdiff_neighborFinset_image, card_sdiff inc,
+    card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff inc,
     tsub_add_eq_add_tsub <| card_le_card inc, card_incidenceFinset_eq_degree]
   congr 2
   rw [card_image_of_injective, card_neighborFinset_eq_degree]
diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
@@ -187,8 +187,8 @@ theorem card_filter_equitabilise_small (hm : m ≠ 0) :
 #align finpartition.card_filter_equitabilise_small Finpartition.card_filter_equitabilise_small
 
 theorem card_parts_equitabilise (hm : m ≠ 0) : (P.equitabilise h).parts.card = a + b := by
-  rw [← filter_true_of_mem fun x => card_eq_of_mem_parts_equitabilise, filter_or, card_union_eq,
-    P.card_filter_equitabilise_small _ hm, P.card_filter_equitabilise_big]
+  rw [← filter_true_of_mem fun x => card_eq_of_mem_parts_equitabilise, filter_or,
+    card_union_of_disjoint, P.card_filter_equitabilise_small _ hm, P.card_filter_equitabilise_big]
   -- Porting note: was `infer_instance`
   exact disjoint_filter.2 fun x _ h₀ h₁ => Nat.succ_ne_self m <| h₁.symm.trans h₀
 #align finpartition.card_parts_equitabilise Finpartition.card_parts_equitabilise
diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean
@@ -459,22 +459,36 @@ theorem card_inter_add_card_union (s t : Finset α) :
     (s ∩ t).card + (s ∪ t).card = s.card + t.card := by rw [add_comm, card_union_add_card_inter]
 #align finset.card_inter_add_card_union Finset.card_inter_add_card_union
 
+lemma card_union (s t : Finset α) : (s ∪ t).card = s.card + t.card - (s ∩ t).card := by
+  rw [← card_union_add_card_inter, Nat.add_sub_cancel]
+
+lemma card_inter (s t : Finset α) : (s ∩ t).card = s.card + t.card - (s ∪ t).card := by
+  rw [← card_inter_add_card_union, Nat.add_sub_cancel]
+
 theorem card_union_le (s t : Finset α) : (s ∪ t).card ≤ s.card + t.card :=
   card_union_add_card_inter s t ▸ Nat.le_add_right _ _
 #align finset.card_union_le Finset.card_union_le
 
-theorem card_union_eq (h : Disjoint s t) : (s ∪ t).card = s.card + t.card := by
+@[simp] lemma card_union_of_disjoint (h : Disjoint s t) : (s ∪ t).card = s.card + t.card := by
   rw [← disjUnion_eq_union s t h, card_disjUnion _ _ _]
-#align finset.card_union_eq Finset.card_union_eq
+#align finset.card_union_eq Finset.card_union_of_disjoint
+#align finset.card_disjoint_union Finset.card_union_of_disjoint
 
-@[simp]
-theorem card_disjoint_union (h : Disjoint s t) : card (s ∪ t) = s.card + t.card :=
-  card_union_eq h
-#align finset.card_disjoint_union Finset.card_disjoint_union
+-- 2024-02-09
+@[deprecated] alias card_union_eq := card_union_of_disjoint
+@[deprecated] alias card_disjoint_union := card_union_of_disjoint
+
+lemma cast_card_inter [AddGroupWithOne R] :
+    ((s ∩ t).card : R) = s.card + t.card - (s ∪ t).card := by
+  rw [eq_sub_iff_add_eq, ← cast_add, card_inter_add_card_union, cast_add]
+
+lemma cast_card_union [AddGroupWithOne R] :
+    ((s ∪ t).card : R) = s.card + t.card - (s ∩ t).card := by
+  rw [eq_sub_iff_add_eq, ← cast_add, card_union_add_card_inter, cast_add]
 
 theorem card_sdiff (h : s ⊆ t) : card (t \ s) = t.card - s.card := by
   suffices card (t \ s) = card (t \ s ∪ s) - s.card by rwa [sdiff_union_of_subset h] at this
-  rw [card_disjoint_union sdiff_disjoint, add_tsub_cancel_right]
+  rw [card_union_of_disjoint sdiff_disjoint, add_tsub_cancel_right]
 #align finset.card_sdiff Finset.card_sdiff
 
 lemma cast_card_sdiff [AddGroupWithOne R] (h : s ⊆ t) : ((t \ s).card : R) = t.card - s.card := by
@@ -497,7 +511,7 @@ theorem card_le_card_sdiff_add_card : s.card ≤ (s \ t).card + t.card :=
 #align finset.card_le_card_sdiff_add_card Finset.card_le_card_sdiff_add_card
 
 theorem card_sdiff_add_card : (s \ t).card + t.card = (s ∪ t).card := by
-  rw [← card_disjoint_union sdiff_disjoint, sdiff_union_self_eq_union]
+  rw [← card_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]
 #align finset.card_sdiff_add_card Finset.card_sdiff_add_card
 
 lemma card_sdiff_comm (h : s.card = t.card) : (s \ t).card = (t \ s).card :=
@@ -507,7 +521,7 @@ lemma card_sdiff_comm (h : s.card = t.card) : (s \ t).card = (t \ s).card :=
 @[simp]
 lemma card_sdiff_add_card_inter (s t : Finset α) :
     (s \ t).card + (s ∩ t).card = s.card := by
-  rw [← card_disjoint_union (disjoint_sdiff_inter _ _), sdiff_union_inter]
+  rw [← card_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]
 
 @[simp]
 lemma card_inter_add_card_sdiff (s t : Finset α) :
@@ -519,7 +533,8 @@ end Lattice
 theorem filter_card_add_filter_neg_card_eq_card
     (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] :
     (s.filter p).card + (s.filter (fun a => ¬ p a)).card = s.card := by
-  classical rw [← card_union_eq (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]
+  classical
+  rw [← card_union_of_disjoint (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]
 #align finset.filter_card_add_filter_neg_card_eq_card Finset.filter_card_add_filter_neg_card_eq_card
 
 /-- Given a set `A` and a set `B` inside it, we can shrink `A` to any appropriate size, and keep `B`
diff --git a/Mathlib/Data/Finset/NAry.lean b/Mathlib/Data/Finset/NAry.lean
@@ -508,7 +508,7 @@ theorem card_dvd_card_image₂_right (hf : ∀ a ∈ s, Injective (f a))
     (hs.subset <| Set.image_subset _ <| coe_subset.2 <| subset_insert _ _)
   rw [image₂_insert_left]
   by_cases h : Disjoint (image (f a) t) (image₂ f s t)
-  · rw [card_union_eq h]
+  · rw [card_union_of_disjoint h]
     exact (card_image_of_injective _ <| hf _ <| mem_insert_self _ _).symm.dvd.add ih
   simp_rw [← biUnion_image_left, disjoint_biUnion_right, not_forall] at h
   obtain ⟨b, hb, h⟩ := h
diff --git a/Mathlib/Data/Finset/Prod.lean b/Mathlib/Data/Finset/Prod.lean
@@ -168,17 +168,17 @@ theorem filter_product_card (s : Finset α) (t : Finset β) (p : α → Prop) (q
       (s.filter p).card * (t.filter q).card +
         (s.filter (¬ p ·)).card * (t.filter (¬ q ·)).card := by
   classical
-    rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_eq]
-    · apply congr_arg
-      ext ⟨a, b⟩
-      simp only [filter_union_right, mem_filter, mem_product]
-      constructor <;> intro h <;> use h.1
-      · simp only [h.2, Function.comp_apply, Decidable.em, and_self]
-      · revert h
-        simp only [Function.comp_apply, and_imp]
-        rintro _ _ (_|_) <;> simp [*]
-    · apply Finset.disjoint_filter_filter'
-      exact (disjoint_compl_right.inf_left _).inf_right _
+  rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
+  · apply congr_arg
+    ext ⟨a, b⟩
+    simp only [filter_union_right, mem_filter, mem_product]
+    constructor <;> intro h <;> use h.1
+    · simp only [h.2, Function.comp_apply, Decidable.em, and_self]
+    · revert h
+      simp only [Function.comp_apply, and_imp]
+      rintro _ _ (_|_) <;> simp [*]
+  · apply Finset.disjoint_filter_filter'
+    exact (disjoint_compl_right.inf_left _).inf_right _
 #align finset.filter_product_card Finset.filter_product_card
 
 theorem empty_product (t : Finset β) : (∅ : Finset α) ×ˢ t = ∅ :=
diff --git a/Mathlib/Data/Nat/Count.lean b/Mathlib/Data/Nat/Count.lean
@@ -78,7 +78,7 @@ theorem count_add (a b : ℕ) : count p (a + b) = count p a + count (fun k ↦ p
     simp_rw [mem_map, mem_range, addLeftEmbedding_apply]
     rintro x hx ⟨c, _, rfl⟩
     exact (self_le_add_right _ _).not_lt hx
-  simp_rw [count_eq_card_filter_range, range_add, filter_union, card_disjoint_union this,
+  simp_rw [count_eq_card_filter_range, range_add, filter_union, card_union_of_disjoint this,
     filter_map, addLeftEmbedding, card_map]
   rfl
 #align nat.count_add Nat.count_add
diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean
@@ -256,7 +256,7 @@ theorem multiplicity_choose_prime_pow_add_multiplicity (hp : p.Prime) (hkn : k 
       rw [multiplicity_choose hp hkn (lt_succ_self _),
         multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0.bot_lt
           (lt_succ_of_le (log_mono_right hkn)),
-        ← Nat.cast_add, PartENat.coe_le_coe, log_pow hp.one_lt, ← card_disjoint_union hdisj,
+        ← Nat.cast_add, PartENat.coe_le_coe, log_pow hp.one_lt, ← card_union_of_disjoint hdisj,
         filter_union_right]
       have filter_le_Ico := (Ico 1 n.succ).card_filter_le
         fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean
@@ -95,7 +95,7 @@ theorem exists_root_sum_quadratic [Fintype R] {f g : R[X]} (hf2 : degree f = 2)
             (mt (congr_arg (· % 2)) (by simp [natDegree_eq_of_degree_eq_some hf2, hR])))
           (card_image_polynomial_eval (by rw [degree_neg, hg2]; exact by decide)))
       _ = 2 * ((univ.image fun x : R => eval x f) ∪ univ.image fun x : R => eval x (-g)).card := by
-        rw [card_disjoint_union hd];
+        rw [card_union_of_disjoint hd];
           simp [natDegree_eq_of_degree_eq_some hf2, natDegree_eq_of_degree_eq_some hg2, mul_add]
 
 #align finite_field.exists_root_sum_quadratic FiniteField.exists_root_sum_quadratic
diff --git a/Mathlib/FieldTheory/PolynomialGaloisGroup.lean b/Mathlib/FieldTheory/PolynomialGaloisGroup.lean
@@ -488,7 +488,7 @@ theorem card_complex_roots_eq_card_real_add_card_not_gal_inv (p : ℚ[X]) :
       exact ⟨(mem_rootSet.mp w.2).2, mt (hc0 w).mpr (Equiv.Perm.mem_support.mp hw)⟩
     · rintro ⟨hz1, hz2⟩
       exact ⟨⟨z, mem_rootSet.mpr ⟨hp, hz1⟩⟩, Equiv.Perm.mem_support.mpr (mt (hc0 _).mp hz2), rfl⟩
-  rw [← Finset.card_disjoint_union]
+  rw [← Finset.card_union_of_disjoint]
   · apply congr_arg Finset.card
     simp_rw [Finset.ext_iff, Finset.mem_union, ha, hb, hc]
     tauto
diff --git a/Mathlib/Geometry/Euclidean/Circumcenter.lean b/Mathlib/Geometry/Euclidean/Circumcenter.lean
@@ -680,7 +680,7 @@ theorem sum_reflectionCircumcenterWeightsWithCircumcenter {n : ℕ} {i₁ i₂ :
     (h : i₁ ≠ i₂) : ∑ i, reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i = 1 := by
   simp_rw [sum_pointsWithCircumcenter, reflectionCircumcenterWeightsWithCircumcenter, sum_ite,
     sum_const, filter_or, filter_eq']
-  rw [card_union_eq]
+  rw [card_union_of_disjoint]
   · set_option simprocs false in simp
   · simpa only [if_true, mem_univ, disjoint_singleton] using h
 #align affine.simplex.sum_reflection_circumcenter_weights_with_circumcenter Affine.Simplex.sum_reflectionCircumcenterWeightsWithCircumcenter
diff --git a/Mathlib/GroupTheory/Perm/Support.lean b/Mathlib/GroupTheory/Perm/Support.lean
@@ -636,7 +636,7 @@ theorem card_support_eq_two {f : Perm α} : f.support.card = 2 ↔ IsSwap f := b
 
 theorem Disjoint.card_support_mul (h : Disjoint f g) :
     (f * g).support.card = f.support.card + g.support.card := by
-  rw [← Finset.card_disjoint_union]
+  rw [← Finset.card_union_of_disjoint]
   · congr
     ext
     simp [h.support_mul]
diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean
@@ -253,7 +253,7 @@ theorem index_union_eq (K₁ K₂ : Compacts G) {V : Set G} (hV : (interior V).N
     le_trans
       (add_le_add (this K₁.1 <| Subset.trans (subset_union_left _ _) h1s)
         (this K₂.1 <| Subset.trans (subset_union_right _ _) h1s)) _
-  rw [← Finset.card_union_eq, Finset.filter_union_right]
+  rw [← Finset.card_union_of_disjoint, Finset.filter_union_right]
   exact s.card_filter_le _
   apply Finset.disjoint_filter.mpr
   rintro g₁ _ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩
diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
@@ -234,7 +234,7 @@ theorem sum_mul_div_add_sum_mul_div_eq_mul (p q : ℕ) [hp : Fact p.Prime] (hq0
       have := le_total (x.2 * p) (x.1 * q)
       simp only [mem_union, mem_filter, mem_Ico, mem_product]
       tauto
-  rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_disjoint_union hdisj, hunion,
+  rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_union_of_disjoint hdisj, hunion,
     card_product]
   simp only [card_Ico, tsub_zero, succ_sub_succ_eq_sub]
 #align zmod.sum_mul_div_add_sum_mul_div_eq_mul ZMod.sum_mul_div_add_sum_mul_div_eq_mul
diff --git a/Mathlib/NumberTheory/SmoothNumbers.lean b/Mathlib/NumberTheory/SmoothNumbers.lean
@@ -213,7 +213,7 @@ def roughNumbersUpTo (N k : ℕ) : Finset ℕ :=
 lemma smoothNumbersUpTo_card_add_roughNumbersUpTo_card (N k : ℕ) :
     (smoothNumbersUpTo N k).card + (roughNumbersUpTo N k).card = N := by
   rw [smoothNumbersUpTo, roughNumbersUpTo,
-    ← Finset.card_union_eq <| Finset.disjoint_filter.mpr fun n _ hn₂ h ↦ h.2 hn₂,
+    ← Finset.card_union_of_disjoint <| Finset.disjoint_filter.mpr fun n _ hn₂ h ↦ h.2 hn₂,
     Finset.filter_union_right]
   suffices : Finset.card (Finset.filter (fun x ↦ x ≠ 0) (Finset.range (succ N))) = N
   · convert this with n
diff --git a/Mathlib/RingTheory/Prime.lean b/Mathlib/RingTheory/Prime.lean
@@ -54,7 +54,7 @@ theorem mul_eq_mul_prime_pow {x y a p : R} {n : ℕ} (hp : Prime p) (hx : x * y
   rcases mul_eq_mul_prime_prod (fun _ _ ↦ hp)
     (show x * y = a * (range n).prod fun _ ↦ p by simpa) with
       ⟨t, u, b, c, htus, htu, rfl, rfl, rfl⟩
-  exact ⟨t.card, u.card, b, c, by rw [← card_disjoint_union htu, htus, card_range], by simp⟩
+  exact ⟨t.card, u.card, b, c, by rw [← card_union_of_disjoint htu, htus, card_range], by simp⟩
 #align mul_eq_mul_prime_pow mul_eq_mul_prime_pow
 
 end CancelCommMonoidWithZero
