bump to nightly-2024-02-13-08

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Data/Finset/Card.lean

@@ -544,17 +544,19 @@ theorem card_union_le (s t : Finset α) : (s ∪ t).card ≤ s.card + t.card :=
 #align finset.card_union_le Finset.card_union_le
 -/
 
-#print Finset.card_union_eq /-
-theorem card_union_eq (h : Disjoint s t) : (s ∪ t).card = s.card + t.card := by
+#print Finset.card_union_of_disjoint /-
+theorem card_union_of_disjoint (h : Disjoint s t) : (s ∪ t).card = s.card + t.card := by
   rw [← disj_union_eq_union s t h, card_disj_union _ _ _]
-#align finset.card_union_eq Finset.card_union_eq
+#align finset.card_union_eq Finset.card_union_of_disjoint
 -/
 
-#print Finset.card_disjoint_union /-
+/- warning: finset.card_disjoint_union clashes with finset.card_union_eq -> Finset.card_union_of_disjoint
+Case conversion may be inaccurate. Consider using '#align finset.card_disjoint_union Finset.card_union_of_disjointₓ'. -/
+#print 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
+theorem card_union_of_disjoint (h : Disjoint s t) : card (s ∪ t) = s.card + t.card :=
+  card_union_of_disjoint h
+#align finset.card_disjoint_union Finset.card_union_of_disjoint
 -/
 
 #print Finset.card_sdiff /-

Mathbin/Data/Set/Ncard.lean

@@ -751,7 +751,7 @@ theorem ncard_union_eq (h : Disjoint s t)
   classical
   rw [ncard_eq_to_finset_card _ hs, ncard_eq_to_finset_card _ ht,
     ncard_eq_to_finset_card _ (hs.union ht), finite.to_finset_union]
-  refine' Finset.card_union_eq _
+  refine' Finset.card_union_of_disjoint _
   rwa [finite.disjoint_to_finset]
 #align set.ncard_union_eq Set.ncard_union_eq
 -/

Mathbin/FieldTheory/PolynomialGaloisGroup.lean

@@ -524,7 +524,7 @@ theorem card_complex_roots_eq_card_real_add_card_not_gal_inv (p : ℚ[X]) :
       exact ⟨(mem_root_set.mp w.2).2, mt (hc0 w).mpr (equiv.perm.mem_support.mp hw)⟩
     · rintro ⟨hz1, hz2⟩
       exact ⟨⟨z, mem_root_set.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

Mathbin/GroupTheory/Perm/Support.lean

@@ -785,7 +785,7 @@ theorem card_support_eq_two {f : Perm α} : f.support.card = 2 ↔ IsSwap f :=
 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]

Mathbin/MeasureTheory/Measure/Haar/Basic.lean

@@ -287,7 +287,7 @@ theorem index_union_eq (K₁ K₂ : Compacts G) {V : Set G} (hV : (interior V).N
       (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₁ h1g₁ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩

lake-manifest.json

@@ -58,19 +58,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "841bef78260cf3074576dfedbd529ed34fd036f1",
+   "rev": "fa3313a1fc92ebc5761b89af004215ac88cbebc2",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "841bef78260cf3074576dfedbd529ed34fd036f1",
+   "inputRev": "fa3313a1fc92ebc5761b89af004215ac88cbebc2",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "c210736dce83fe29d9d9452ffd4b5b3b9680292d",
+   "rev": "7119c821c6d989a542e351f5e573658d25c2fdf5",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c210736dce83fe29d9d9452ffd4b5b3b9680292d",
+   "inputRev": "7119c821c6d989a542e351f5e573658d25c2fdf5",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mathlib3port",

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2024-02-12-08"
+def tag : String := "nightly-2024-02-13-08"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"c210736dce83fe29d9d9452ffd4b5b3b9680292d"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"7119c821c6d989a542e351f5e573658d25c2fdf5"
 
 @[default_target]
 lean_lib Mathbin where