bump to nightly-2023-05-06-14

mathlib commit leanprover-community/mathlib@3905fa8
leanprover-community · May 6, 2023 · 2f9b6e1 · 2f9b6e1
1 parent 3c3d1a5
commit 2f9b6e1
Show file tree

Hide file tree

Showing 4 changed files with 286 additions and 28 deletions.
diff --git a/Mathbin/MeasureTheory/Group/FundamentalDomain.lean b/Mathbin/MeasureTheory/Group/FundamentalDomain.lean
@@ -510,7 +510,7 @@ theorem measure_le_of_pairwise_disjoint (hs : IsFundamentalDomain G s μ)
   calc
     μ t = ∑' g : G, μ (g • t ∩ s) := hs.measure_eq_tsum t
     _ = μ (⋃ g : G, g • t ∩ s) :=
-      (Eq.symm <| measure_Union₀ hd fun g => (ht.smul _).inter hs.NullMeasurableSet)
+      (Eq.symm <| measure_unionᵢ₀ hd fun g => (ht.smul _).inter hs.NullMeasurableSet)
     _ ≤ μ s := measure_mono (unionᵢ_subset fun g => inter_subset_right _ _)
 
 #align measure_theory.is_fundamental_domain.measure_le_of_pairwise_disjoint MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint