bump to nightly-2023-05-06-08

mathlib commit leanprover-community/mathlib@3905fa8

Mathbin/MeasureTheory/Group/AddCircle.lean

@@ -79,7 +79,7 @@ theorem isAddFundamentalDomain_of_ae_ball (I : Set <| AddCircle T) (u x : AddCir
     · simpa only [Ne.def, AddSubgroup.mk_eq_zero_iff] using hg'
     change ae_disjoint volume (g +ᵥ I) I
     refine'
-      ae_disjoint.congr (Disjoint.aeDisjoint _)
+      ae_disjoint.congr (Disjoint.aedisjoint _)
         ((quasi_measure_preserving_add_left volume (-g)).vadd_ae_eq_of_ae_eq g hI) hI
     have hBg : g +ᵥ B = ball (g + x) (T / (2 * n)) := by
       rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]

Mathbin/MeasureTheory/Group/FundamentalDomain.lean

@@ -55,7 +55,7 @@ structure IsAddFundamentalDomain (G : Type _) {α : Type _} [Zero G] [VAdd G α]
   (s : Set α) (μ : Measure α := by exact MeasureTheory.MeasureSpace.volume) : Prop where
   NullMeasurableSet : NullMeasurableSet s μ
   ae_covers : ∀ᵐ x ∂μ, ∃ g : G, g +ᵥ x ∈ s
-  AeDisjoint : Pairwise <| (AeDisjoint μ on fun g : G => g +ᵥ s)
+  AEDisjoint : Pairwise <| (AEDisjoint μ on fun g : G => g +ᵥ s)
 #align measure_theory.is_add_fundamental_domain MeasureTheory.IsAddFundamentalDomain
 
 /-- A measurable set `s` is a *fundamental domain* for an action of a group `G` on a measurable
@@ -66,7 +66,7 @@ structure IsFundamentalDomain (G : Type _) {α : Type _} [One G] [SMul G α] [Me
   (s : Set α) (μ : Measure α := by exact MeasureTheory.MeasureSpace.volume) : Prop where
   NullMeasurableSet : NullMeasurableSet s μ
   ae_covers : ∀ᵐ x ∂μ, ∃ g : G, g • x ∈ s
-  AeDisjoint : Pairwise <| (AeDisjoint μ on fun g : G => g • s)
+  AEDisjoint : Pairwise <| (AEDisjoint μ on fun g : G => g • s)
 #align measure_theory.is_fundamental_domain MeasureTheory.IsFundamentalDomain
 #align measure_theory.is_add_fundamental_domain MeasureTheory.IsAddFundamentalDomain
 
@@ -85,8 +85,8 @@ theorem mk' (h_meas : NullMeasurableSet s μ) (h_exists : ∀ x : α, ∃! g : G
     IsFundamentalDomain G s μ :=
   { NullMeasurableSet := h_meas
     ae_covers := eventually_of_forall fun x => (h_exists x).exists
-    AeDisjoint := fun a b hab =>
-      Disjoint.aeDisjoint <|
+    AEDisjoint := fun a b hab =>
+      Disjoint.aedisjoint <|
         disjoint_left.2 fun x hxa hxb =>
           by
           rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb
@@ -99,11 +99,11 @@ theorem mk' (h_meas : NullMeasurableSet s μ) (h_exists : ∀ x : α, ∃! g : G
 @[to_additive
       "For `s` to be a fundamental domain, it's enough to check `ae_disjoint (g +ᵥ s) s` for\n`g ≠ 0`."]
 theorem mk'' (h_meas : NullMeasurableSet s μ) (h_ae_covers : ∀ᵐ x ∂μ, ∃ g : G, g • x ∈ s)
-    (h_ae_disjoint : ∀ (g) (_ : g ≠ (1 : G)), AeDisjoint μ (g • s) s)
+    (h_ae_disjoint : ∀ (g) (_ : g ≠ (1 : G)), AEDisjoint μ (g • s) s)
     (h_qmp : ∀ g : G, QuasiMeasurePreserving ((· • ·) g : α → α) μ μ) : IsFundamentalDomain G s μ :=
   { NullMeasurableSet := h_meas
     ae_covers := h_ae_covers
-    AeDisjoint := pairwise_aeDisjoint_of_aeDisjoint_forall_ne_one h_ae_disjoint h_qmp }
+    AEDisjoint := pairwise_aEDisjoint_of_aEDisjoint_forall_ne_one h_ae_disjoint h_qmp }
 #align measure_theory.is_fundamental_domain.mk'' MeasureTheory.IsFundamentalDomain.mk''
 #align measure_theory.is_add_fundamental_domain.mk'' MeasureTheory.IsAddFundamentalDomain.mk''
 
@@ -115,13 +115,13 @@ sufficiently large. -/
 @[to_additive MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le
       "\nIf a measurable space has a finite measure `μ` and a countable additive group `G` acts\nquasi-measure-preservingly, then to show that a set `s` is a fundamental domain, it is sufficient\nto check that its translates `g +ᵥ s` are (almost) disjoint and that the sum `∑' g, μ (g +ᵥ s)` is\nsufficiently large."]
 theorem mk_of_measure_univ_le [IsFiniteMeasure μ] [Countable G] (h_meas : NullMeasurableSet s μ)
-    (h_ae_disjoint : ∀ (g) (_ : g ≠ (1 : G)), AeDisjoint μ (g • s) s)
+    (h_ae_disjoint : ∀ (g) (_ : g ≠ (1 : G)), AEDisjoint μ (g • s) s)
     (h_qmp : ∀ g : G, QuasiMeasurePreserving ((· • ·) g : α → α) μ μ)
     (h_measure_univ_le : μ (univ : Set α) ≤ ∑' g : G, μ (g • s)) : IsFundamentalDomain G s μ :=
-  have ae_disjoint : Pairwise (AeDisjoint μ on fun g : G => g • s) :=
-    pairwise_aeDisjoint_of_aeDisjoint_forall_ne_one h_ae_disjoint h_qmp
+  have ae_disjoint : Pairwise (AEDisjoint μ on fun g : G => g • s) :=
+    pairwise_aEDisjoint_of_aEDisjoint_forall_ne_one h_ae_disjoint h_qmp
   { NullMeasurableSet := h_meas
-    AeDisjoint
+    AEDisjoint
     ae_covers :=
       by
       replace h_meas : ∀ g : G, null_measurable_set (g • s) μ := fun g =>
@@ -149,7 +149,7 @@ theorem unionᵢ_smul_ae_eq (h : IsFundamentalDomain G s μ) : (⋃ g : G, g •
 @[to_additive]
 theorem mono (h : IsFundamentalDomain G s μ) {ν : Measure α} (hle : ν ≪ μ) :
     IsFundamentalDomain G s ν :=
-  ⟨h.1.mono_ac hle, hle h.2, h.AeDisjoint.mono fun a b hab => hle hab⟩
+  ⟨h.1.mono_ac hle, hle h.2, h.AEDisjoint.mono fun a b hab => hle hab⟩
 #align measure_theory.is_fundamental_domain.mono MeasureTheory.IsFundamentalDomain.mono
 #align measure_theory.is_add_fundamental_domain.mono MeasureTheory.IsAddFundamentalDomain.mono
 
@@ -159,7 +159,7 @@ theorem preimage_of_equiv {ν : Measure β} (h : IsFundamentalDomain G s μ) {f
     (hef : ∀ g, Semiconj f ((· • ·) (e g)) ((· • ·) g)) : IsFundamentalDomain H (f ⁻¹' s) ν :=
   { NullMeasurableSet := h.NullMeasurableSet.Preimage hf
     ae_covers := (hf.ae h.ae_covers).mono fun x ⟨g, hg⟩ => ⟨e g, by rwa [mem_preimage, hef g x]⟩
-    AeDisjoint := fun a b hab => by
+    AEDisjoint := fun a b hab => by
       lift e to G ≃ H using he
       have : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹ := by simp [hab]
       convert(h.ae_disjoint this).Preimage hf using 1
@@ -180,11 +180,11 @@ theorem image_of_equiv {ν : Measure β} (h : IsFundamentalDomain G s μ) (f : 
 #align measure_theory.is_add_fundamental_domain.image_of_equiv MeasureTheory.IsAddFundamentalDomain.image_of_equiv
 
 @[to_additive]
-theorem pairwise_aeDisjoint_of_ac {ν} (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) :
-    Pairwise fun g₁ g₂ : G => AeDisjoint ν (g₁ • s) (g₂ • s) :=
-  h.AeDisjoint.mono fun g₁ g₂ H => hν H
-#align measure_theory.is_fundamental_domain.pairwise_ae_disjoint_of_ac MeasureTheory.IsFundamentalDomain.pairwise_aeDisjoint_of_ac
-#align measure_theory.is_add_fundamental_domain.pairwise_ae_disjoint_of_ac MeasureTheory.IsAddFundamentalDomain.pairwise_aeDisjoint_of_ac
+theorem pairwise_aEDisjoint_of_ac {ν} (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) :
+    Pairwise fun g₁ g₂ : G => AEDisjoint ν (g₁ • s) (g₂ • s) :=
+  h.AEDisjoint.mono fun g₁ g₂ H => hν H
+#align measure_theory.is_fundamental_domain.pairwise_ae_disjoint_of_ac MeasureTheory.IsFundamentalDomain.pairwise_aEDisjoint_of_ac
+#align measure_theory.is_add_fundamental_domain.pairwise_ae_disjoint_of_ac MeasureTheory.IsAddFundamentalDomain.pairwise_aEDisjoint_of_ac
 
 @[to_additive]
 theorem smul_of_comm {G' : Type _} [Group G'] [MulAction G' α] [MeasurableSpace G']
@@ -505,7 +505,7 @@ has measure at most `μ s`. -/
 @[to_additive
       "If the additive action of a countable group `G` admits an invariant measure `μ` with\na fundamental domain `s`, then every null-measurable set `t` such that the sets `g +ᵥ t ∩ s` are\npairwise a.e.-disjoint has measure at most `μ s`."]
 theorem measure_le_of_pairwise_disjoint (hs : IsFundamentalDomain G s μ)
-    (ht : NullMeasurableSet t μ) (hd : Pairwise (AeDisjoint μ on fun g : G => g • t ∩ s)) :
+    (ht : NullMeasurableSet t μ) (hd : Pairwise (AEDisjoint μ on fun g : G => g • t ∩ s)) :
     μ t ≤ μ s :=
   calc
     μ t = ∑' g : G, μ (g • t ∩ s) := hs.measure_eq_tsum t
@@ -527,7 +527,7 @@ theorem exists_ne_one_smul_eq (hs : IsFundamentalDomain G s μ) (htm : NullMeasu
     (ht : μ s < μ t) : ∃ (x : _)(_ : x ∈ t)(y : _)(_ : y ∈ t)(g : _)(_ : g ≠ (1 : G)), g • x = y :=
   by
   contrapose! ht
-  refine' hs.measure_le_of_pairwise_disjoint htm (Pairwise.aeDisjoint fun g₁ g₂ hne => _)
+  refine' hs.measure_le_of_pairwise_disjoint htm (Pairwise.aedisjoint fun g₁ g₂ hne => _)
   dsimp [Function.onFun]
   refine' (Disjoint.inf_left _ _).inf_right _
   rw [Set.disjoint_left]
@@ -743,7 +743,7 @@ protected theorem fundamentalInterior : IsFundamentalDomain G (fundamentalInteri
         measure_union_null
           (measure_Union_null fun _ => measure_smul_null hs.measure_fundamental_frontier _)
           hs.ae_covers
-    AeDisjoint := (pairwise_disjoint_fundamentalInterior _ _).mono fun _ _ => Disjoint.aeDisjoint }
+    AEDisjoint := (pairwise_disjoint_fundamentalInterior _ _).mono fun _ _ => Disjoint.aedisjoint }
 #align measure_theory.is_fundamental_domain.fundamental_interior MeasureTheory.IsFundamentalDomain.fundamentalInterior
 
 end IsFundamentalDomain

Mathbin/MeasureTheory/Group/GeometryOfNumbers.lean

@@ -59,7 +59,7 @@ theorem exists_pair_mem_lattice_not_disjoint_vadd [AddCommGroup L] [Countable L]
   exact
     ((fund.measure_eq_tsum _).trans
           (measure_Union₀
-              (Pairwise.mono h fun i j hij => (hij.mono inf_le_left inf_le_left).AeDisjoint)
+              (Pairwise.mono h fun i j hij => (hij.mono inf_le_left inf_le_left).AEDisjoint)
               fun _ => (hS.vadd _).inter fund.null_measurable_set).symm).trans_le
       (measure_mono <| Union_subset fun _ => inter_subset_right _ _)
 #align measure_theory.exists_pair_mem_lattice_not_disjoint_vadd MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd

Mathbin/MeasureTheory/Integral/Average.lean

@@ -157,7 +157,7 @@ theorem measure_smul_set_average (f : α → E) {s : Set α} (h : μ s ≠ ∞)
   rw [← measure_smul_average, restrict_apply_univ]
 #align measure_theory.measure_smul_set_average MeasureTheory.measure_smul_set_average
 
-theorem average_union {f : α → E} {s t : Set α} (hd : AeDisjoint μ s t) (ht : NullMeasurableSet t μ)
+theorem average_union {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ)
     (hsμ : μ s ≠ ∞) (htμ : μ t ≠ ∞) (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) :
     (⨍ x in s ∪ t, f x ∂μ) =
       (((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ x in s, f x ∂μ) +
@@ -167,7 +167,7 @@ theorem average_union {f : α → E} {s t : Set α} (hd : AeDisjoint μ s t) (ht
   rw [restrict_union₀ hd ht, average_add_measure hfs hft, restrict_apply_univ, restrict_apply_univ]
 #align measure_theory.average_union MeasureTheory.average_union
 
-theorem average_union_mem_openSegment {f : α → E} {s t : Set α} (hd : AeDisjoint μ s t)
+theorem average_union_mem_openSegment {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t)
     (ht : NullMeasurableSet t μ) (hs₀ : μ s ≠ 0) (ht₀ : μ t ≠ 0) (hsμ : μ s ≠ ∞) (htμ : μ t ≠ ∞)
     (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) :
     (⨍ x in s ∪ t, f x ∂μ) ∈ openSegment ℝ (⨍ x in s, f x ∂μ) (⨍ x in t, f x ∂μ) :=
@@ -179,7 +179,7 @@ theorem average_union_mem_openSegment {f : α → E} {s t : Set α} (hd : AeDisj
       ⟨(μ s).toReal, (μ t).toReal, hs₀, ht₀, (average_union hd ht hsμ htμ hfs hft).symm⟩
 #align measure_theory.average_union_mem_open_segment MeasureTheory.average_union_mem_openSegment
 
-theorem average_union_mem_segment {f : α → E} {s t : Set α} (hd : AeDisjoint μ s t)
+theorem average_union_mem_segment {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t)
     (ht : NullMeasurableSet t μ) (hsμ : μ s ≠ ∞) (htμ : μ t ≠ ∞) (hfs : IntegrableOn f s μ)
     (hft : IntegrableOn f t μ) :
     (⨍ x in s ∪ t, f x ∂μ) ∈ [⨍ x in s, f x ∂μ -[ℝ] ⨍ x in t, f x ∂μ] :=

Mathbin/MeasureTheory/Integral/Lebesgue.lean

@@ -1216,19 +1216,19 @@ theorem lintegral_tsum [Countable β] {f : β → α → ℝ≥0∞} (hf : ∀ i
 open Measure
 
 theorem lintegral_Union₀ [Countable β] {s : β → Set α} (hm : ∀ i, NullMeasurableSet (s i) μ)
-    (hd : Pairwise (AeDisjoint μ on s)) (f : α → ℝ≥0∞) :
+    (hd : Pairwise (AEDisjoint μ on s)) (f : α → ℝ≥0∞) :
     (∫⁻ a in ⋃ i, s i, f a ∂μ) = ∑' i, ∫⁻ a in s i, f a ∂μ := by
   simp only [measure.restrict_Union_ae hd hm, lintegral_sum_measure]
 #align measure_theory.lintegral_Union₀ MeasureTheory.lintegral_Union₀
 
 theorem lintegral_unionᵢ [Countable β] {s : β → Set α} (hm : ∀ i, MeasurableSet (s i))
     (hd : Pairwise (Disjoint on s)) (f : α → ℝ≥0∞) :
     (∫⁻ a in ⋃ i, s i, f a ∂μ) = ∑' i, ∫⁻ a in s i, f a ∂μ :=
-  lintegral_Union₀ (fun i => (hm i).NullMeasurableSet) hd.AeDisjoint f
+  lintegral_Union₀ (fun i => (hm i).NullMeasurableSet) hd.AEDisjoint f
 #align measure_theory.lintegral_Union MeasureTheory.lintegral_unionᵢ
 
 theorem lintegral_bUnion₀ {t : Set β} {s : β → Set α} (ht : t.Countable)
-    (hm : ∀ i ∈ t, NullMeasurableSet (s i) μ) (hd : t.Pairwise (AeDisjoint μ on s)) (f : α → ℝ≥0∞) :
+    (hm : ∀ i ∈ t, NullMeasurableSet (s i) μ) (hd : t.Pairwise (AEDisjoint μ on s)) (f : α → ℝ≥0∞) :
     (∫⁻ a in ⋃ i ∈ t, s i, f a ∂μ) = ∑' i : t, ∫⁻ a in s i, f a ∂μ :=
   by
   haveI := ht.to_encodable
@@ -1238,19 +1238,19 @@ theorem lintegral_bUnion₀ {t : Set β} {s : β → Set α} (ht : t.Countable)
 theorem lintegral_bUnion {t : Set β} {s : β → Set α} (ht : t.Countable)
     (hm : ∀ i ∈ t, MeasurableSet (s i)) (hd : t.PairwiseDisjoint s) (f : α → ℝ≥0∞) :
     (∫⁻ a in ⋃ i ∈ t, s i, f a ∂μ) = ∑' i : t, ∫⁻ a in s i, f a ∂μ :=
-  lintegral_bUnion₀ ht (fun i hi => (hm i hi).NullMeasurableSet) hd.AeDisjoint f
+  lintegral_bUnion₀ ht (fun i hi => (hm i hi).NullMeasurableSet) hd.AEDisjoint f
 #align measure_theory.lintegral_bUnion MeasureTheory.lintegral_bUnion
 
 theorem lintegral_bUnion_finset₀ {s : Finset β} {t : β → Set α}
-    (hd : Set.Pairwise (↑s) (AeDisjoint μ on t)) (hm : ∀ b ∈ s, NullMeasurableSet (t b) μ)
+    (hd : Set.Pairwise (↑s) (AEDisjoint μ on t)) (hm : ∀ b ∈ s, NullMeasurableSet (t b) μ)
     (f : α → ℝ≥0∞) : (∫⁻ a in ⋃ b ∈ s, t b, f a ∂μ) = ∑ b in s, ∫⁻ a in t b, f a ∂μ := by
   simp only [← Finset.mem_coe, lintegral_bUnion₀ s.countable_to_set hm hd, ← s.tsum_subtype']
 #align measure_theory.lintegral_bUnion_finset₀ MeasureTheory.lintegral_bUnion_finset₀
 
 theorem lintegral_bUnion_finset {s : Finset β} {t : β → Set α} (hd : Set.PairwiseDisjoint (↑s) t)
     (hm : ∀ b ∈ s, MeasurableSet (t b)) (f : α → ℝ≥0∞) :
     (∫⁻ a in ⋃ b ∈ s, t b, f a ∂μ) = ∑ b in s, ∫⁻ a in t b, f a ∂μ :=
-  lintegral_bUnion_finset₀ hd.AeDisjoint (fun b hb => (hm b hb).NullMeasurableSet) f
+  lintegral_bUnion_finset₀ hd.AEDisjoint (fun b hb => (hm b hb).NullMeasurableSet) f
 #align measure_theory.lintegral_bUnion_finset MeasureTheory.lintegral_bUnion_finset
 
 theorem lintegral_unionᵢ_le [Countable β] (s : β → Set α) (f : α → ℝ≥0∞) :

Mathbin/MeasureTheory/Integral/SetIntegral.lean

@@ -94,15 +94,15 @@ theorem set_integral_congr_set_ae (hst : s =ᵐ[μ] t) : (∫ x in s, f x ∂μ)
   rw [measure.restrict_congr_set hst]
 #align measure_theory.set_integral_congr_set_ae MeasureTheory.set_integral_congr_set_ae
 
-theorem integral_union_ae (hst : AeDisjoint μ s t) (ht : NullMeasurableSet t μ)
+theorem integral_union_ae (hst : AEDisjoint μ s t) (ht : NullMeasurableSet t μ)
     (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) :
     (∫ x in s ∪ t, f x ∂μ) = (∫ x in s, f x ∂μ) + ∫ x in t, f x ∂μ := by
   simp only [integrable_on, measure.restrict_union₀ hst ht, integral_add_measure hfs hft]
 #align measure_theory.integral_union_ae MeasureTheory.integral_union_ae
 
 theorem integral_union (hst : Disjoint s t) (ht : MeasurableSet t) (hfs : IntegrableOn f s μ)
     (hft : IntegrableOn f t μ) : (∫ x in s ∪ t, f x ∂μ) = (∫ x in s, f x ∂μ) + ∫ x in t, f x ∂μ :=
-  integral_union_ae hst.AeDisjoint ht.NullMeasurableSet hfs hft
+  integral_union_ae hst.AEDisjoint ht.NullMeasurableSet hfs hft
 #align measure_theory.integral_union MeasureTheory.integral_union
 
 theorem integral_diff (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :
@@ -160,7 +160,7 @@ theorem integral_univ : (∫ x in univ, f x ∂μ) = ∫ x, f x ∂μ := by rw [
 theorem integral_add_compl₀ (hs : NullMeasurableSet s μ) (hfi : Integrable f μ) :
     ((∫ x in s, f x ∂μ) + ∫ x in sᶜ, f x ∂μ) = ∫ x, f x ∂μ := by
   rw [←
-    integral_union_ae (@disjoint_compl_right (Set α) _ _).AeDisjoint hs.compl hfi.integrable_on
+    integral_union_ae (@disjoint_compl_right (Set α) _ _).AEDisjoint hs.compl hfi.integrable_on
       hfi.integrable_on,
     union_compl_self, integral_univ]
 #align measure_theory.integral_add_compl₀ MeasureTheory.integral_add_compl₀
@@ -243,7 +243,7 @@ theorem tendsto_set_integral_of_monotone {ι : Type _} [Countable ι] [Semilatti
 #align measure_theory.tendsto_set_integral_of_monotone MeasureTheory.tendsto_set_integral_of_monotone
 
 theorem hasSum_integral_unionᵢ_ae {ι : Type _} [Countable ι] {s : ι → Set α}
-    (hm : ∀ i, NullMeasurableSet (s i) μ) (hd : Pairwise (AeDisjoint μ on s))
+    (hm : ∀ i, NullMeasurableSet (s i) μ) (hd : Pairwise (AEDisjoint μ on s))
     (hfi : IntegrableOn f (⋃ i, s i) μ) :
     HasSum (fun n => ∫ a in s n, f a ∂μ) (∫ a in ⋃ n, s n, f a ∂μ) :=
   by
@@ -255,7 +255,7 @@ theorem hasSum_integral_unionᵢ {ι : Type _} [Countable ι] {s : ι → Set α
     (hm : ∀ i, MeasurableSet (s i)) (hd : Pairwise (Disjoint on s))
     (hfi : IntegrableOn f (⋃ i, s i) μ) :
     HasSum (fun n => ∫ a in s n, f a ∂μ) (∫ a in ⋃ n, s n, f a ∂μ) :=
-  hasSum_integral_unionᵢ_ae (fun i => (hm i).NullMeasurableSet) (hd.mono fun i j h => h.AeDisjoint)
+  hasSum_integral_unionᵢ_ae (fun i => (hm i).NullMeasurableSet) (hd.mono fun i j h => h.AEDisjoint)
     hfi
 #align measure_theory.has_sum_integral_Union MeasureTheory.hasSum_integral_unionᵢ
 
@@ -266,7 +266,7 @@ theorem integral_unionᵢ {ι : Type _} [Countable ι] {s : ι → Set α} (hm :
 #align measure_theory.integral_Union MeasureTheory.integral_unionᵢ
 
 theorem integral_unionᵢ_ae {ι : Type _} [Countable ι] {s : ι → Set α}
-    (hm : ∀ i, NullMeasurableSet (s i) μ) (hd : Pairwise (AeDisjoint μ on s))
+    (hm : ∀ i, NullMeasurableSet (s i) μ) (hd : Pairwise (AEDisjoint μ on s))
     (hfi : IntegrableOn f (⋃ i, s i) μ) : (∫ a in ⋃ n, s n, f a ∂μ) = ∑' n, ∫ a in s n, f a ∂μ :=
   (HasSum.tsum_eq (hasSum_integral_unionᵢ_ae hm hd hfi)).symm
 #align measure_theory.integral_Union_ae MeasureTheory.integral_unionᵢ_ae