From a217b9c33f992270d4d643bffed75e2de74e2089 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 18 Jan 2022 09:14:41 +0000
Subject: [PATCH] feat(measure_theory): drop some `measurable_set` assumptions
 (#11536)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* make `exists_subordinate_pairwise_disjoint` work for `null_measurable_set`s;
* use `ae_disjoint` in `measure_Union₀`, drop `measure_Union_of_null_inter`;
* prove `measure_inter_add_diff` for `null_measurable_set`s;
* drop some `measurable_set` assumptions in `measure_union`, `measure_diff`, etc;
* golf.
---
 .../constructions/borel_space.lean            |   6 +-
 src/measure_theory/covering/besicovitch.lean  |   2 +-
 src/measure_theory/decomposition/jordan.lean  |   2 -
 .../decomposition/lebesgue.lean               | 118 ++++++--------
 .../decomposition/radon_nikodym.lean          |   3 +-
 .../function/continuous_map_dense.lean        |   4 +-
 .../group/fundamental_domain.lean             |   4 +-
 src/measure_theory/integral/bochner.lean      |  10 +-
 .../integral/interval_integral.lean           |   4 +-
 src/measure_theory/integral/set_integral.lean |  48 +++---
 src/measure_theory/measure/ae_disjoint.lean   |  10 ++
 src/measure_theory/measure/haar_lebesgue.lean |   9 +-
 src/measure_theory/measure/measure_space.lean | 153 ++++++++----------
 .../measure/measure_space_def.lean            |   4 +-
 .../measure/null_measurable.lean              |  74 +++++++--
 src/measure_theory/measure/regular.lean       |  39 ++---
 src/measure_theory/measure/stieltjes.lean     |   6 +-
 17 files changed, 245 insertions(+), 251 deletions(-)

diff --git a/src/measure_theory/constructions/borel_space.lean b/src/measure_theory/constructions/borel_space.lean
index 8d075d12bd6b7..c8737b477be0a 100644
--- a/src/measure_theory/constructions/borel_space.lean
+++ b/src/measure_theory/constructions/borel_space.lean
@@ -623,8 +623,8 @@ begin
   { rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, -, hst⟩,
     have : directed_on (≤) s, from directed_on_iff_directed.2 (directed_of_sup $ λ _ _, id),
     simp only [← bsupr_measure_Iic hsc (hsd.exists_ge' hst) this, h] },
-  rw [← Iic_diff_Iic, measure_diff (Iic_subset_Iic.2 hlt.le) measurable_set_Iic measurable_set_Iic,
-      measure_diff (Iic_subset_Iic.2 hlt.le) measurable_set_Iic measurable_set_Iic, h a, h b],
+  rw [← Iic_diff_Iic, measure_diff (Iic_subset_Iic.2 hlt.le) measurable_set_Iic,
+      measure_diff (Iic_subset_Iic.2 hlt.le) measurable_set_Iic, h a, h b],
   { rw ← h a, exact (measure_lt_top μ _).ne },
   { exact (measure_lt_top μ _).ne }
 end
@@ -1239,7 +1239,6 @@ begin
     { apply disjoint_left.2 (λ x hx h'x, _),
       have : 0 < f x := h'x.2,
       exact lt_irrefl 0 (this.trans_le hx.2.le) },
-    { exact hs.inter (hf (measurable_set_singleton _)) },
     { exact hs.inter (hf measurable_set_Ioi) } },
   have B : μ (s ∩ f⁻¹' (Ioi 0)) = μ (s ∩ f⁻¹' {∞}) + μ (s ∩ f⁻¹' (Ioo 0 ∞)),
   { rw ← measure_union,
@@ -1254,7 +1253,6 @@ begin
     { apply disjoint_left.2 (λ x hx h'x, _),
       have : f x < ∞ := h'x.2.2,
       exact lt_irrefl _ (this.trans_le (le_of_eq hx.2.symm)) },
-    { exact hs.inter (hf (measurable_set_singleton _)) },
     { exact hs.inter (hf measurable_set_Ioo) } },
   have C : μ (s ∩ f⁻¹' (Ioo 0 ∞)) = ∑' (n : ℤ), μ (s ∩ f⁻¹' (Ico (t^n) (t^(n+1)))),
   { rw [← measure_Union, ennreal.Ioo_zero_top_eq_Union_Ico_zpow (ennreal.one_lt_coe_iff.2 ht)
diff --git a/src/measure_theory/covering/besicovitch.lean b/src/measure_theory/covering/besicovitch.lean
index 82b9070b174c9..9d76dbf429aa5 100644
--- a/src/measure_theory/covering/besicovitch.lean
+++ b/src/measure_theory/covering/besicovitch.lean
@@ -585,7 +585,7 @@ begin
       { rw [finset.set_bUnion_finset_image],
         exact le_trans (measure_mono (diff_subset_diff so (subset.refl _))) H },
     rw [← diff_inter_self_eq_diff,
-      measure_diff_le_iff_le_add _ omeas (inter_subset_right _ _) ((measure_lt_top μ _).ne)], swap,
+      measure_diff_le_iff_le_add _ (inter_subset_right _ _) ((measure_lt_top μ _).ne)], swap,
     { apply measurable_set.inter _ omeas,
       haveI : encodable (u i) := (u_count i).to_encodable,
       exact measurable_set.Union
diff --git a/src/measure_theory/decomposition/jordan.lean b/src/measure_theory/decomposition/jordan.lean
index f0a6e8d4aace4..e8d1f7ec11632 100644
--- a/src/measure_theory/decomposition/jordan.lean
+++ b/src/measure_theory/decomposition/jordan.lean
@@ -369,7 +369,6 @@ begin
           (hS₄ ▸ measure_mono (set.inter_subset_right _ _)), zero_add],
     { refine set.disjoint_of_subset_left (set.inter_subset_right _ _)
         (set.disjoint_of_subset_right (set.inter_subset_right _ _) disjoint_compl_right) },
-    { exact hi.inter hS₁ },
     { exact hi.inter hS₁.compl } },
   have hμ₂ : (j₂.pos_part i).to_real = j₂.to_signed_measure (i ∩ Tᶜ),
   { rw [to_signed_measure, to_signed_measure_sub_apply (hi.inter hT₁.compl),
@@ -381,7 +380,6 @@ begin
           (hT₄ ▸ measure_mono (set.inter_subset_right _ _)), zero_add],
     { exact set.disjoint_of_subset_left (set.inter_subset_right _ _)
         (set.disjoint_of_subset_right (set.inter_subset_right _ _) disjoint_compl_right) },
-    { exact hi.inter hT₁ },
     { exact hi.inter hT₁.compl } },
   -- since the two signed measures associated with the Jordan decompositions are the same,
   -- and the symmetric difference of the Hahn decompositions have measure zero, the result follows
diff --git a/src/measure_theory/decomposition/lebesgue.lean b/src/measure_theory/decomposition/lebesgue.lean
index dd6849820e38a..5ea9ddc237f8d 100644
--- a/src/measure_theory/decomposition/lebesgue.lean
+++ b/src/measure_theory/decomposition/lebesgue.lean
@@ -59,6 +59,7 @@ Lebesgue decomposition theorem
 
 noncomputable theory
 open_locale classical measure_theory nnreal ennreal
+open set
 
 variables {α β : Type*} {m : measurable_space α} {μ ν : measure_theory.measure α}
 include m
@@ -234,7 +235,7 @@ begin
   obtain ⟨⟨S, hS₁, hS₂, hS₃⟩, ⟨T, hT₁, hT₂, hT₃⟩⟩ := ⟨hs, hsing⟩,
   rw hadd' at hadd,
   have hνinter : ν (S ∩ T)ᶜ = 0,
-  { rw set.compl_inter,
+  { rw compl_inter,
     refine nonpos_iff_eq_zero.1 (le_trans (measure_union_le _ _) _),
     rw [hT₃, hS₃, add_zero],
     exact le_refl _ },
@@ -243,35 +244,24 @@ begin
     have hf : ν.with_density f (A ∩ (S ∩ T)ᶜ) = 0,
     { refine with_density_absolutely_continuous ν _ _,
       rw ← nonpos_iff_eq_zero,
-      exact hνinter ▸ measure_mono (set.inter_subset_right _ _) },
+      exact hνinter ▸ measure_mono (inter_subset_right _ _) },
     have hrn : ν.with_density (μ.rn_deriv ν) (A ∩ (S ∩ T)ᶜ) = 0,
     { refine with_density_absolutely_continuous ν _ _,
       rw ← nonpos_iff_eq_zero,
-      exact hνinter ▸ measure_mono (set.inter_subset_right _ _) },
+      exact hνinter ▸ measure_mono (inter_subset_right _ _) },
     rw [restrict_apply hA, restrict_apply hA, ← add_zero (s (A ∩ (S ∩ T)ᶜ)), ← hf,
         ← add_apply, ← hadd, add_apply, hrn, add_zero] },
   have heq' : ∀ A : set α, measurable_set A → s A = s.restrict (S ∩ T)ᶜ A,
   { intros A hA,
     have hsinter : s (A ∩ (S ∩ T)) = 0,
     { rw ← nonpos_iff_eq_zero,
-      exact hS₂ ▸ measure_mono
-        (set.subset.trans (set.inter_subset_right _ _) (set.inter_subset_left _ _)) },
-    rw [restrict_apply hA, ← add_zero (s (A ∩ (S ∩ T)ᶜ)), ← hsinter, ← measure_union,
-        ← set.inter_union_distrib_left, set.compl_union_self, set.inter_univ],
-    { exact disjoint.inter_left' _ ( disjoint.inter_right' _ disjoint_compl_left) },
-    { measurability },
-    { measurability } },
+      exact hS₂ ▸ measure_mono ((inter_subset_right _ _).trans (inter_subset_left _ _)) },
+    rw [restrict_apply hA, ← diff_eq, ae_disjoint.measure_diff_left hsinter] },
   ext1 A hA,
   have hμinter : μ.singular_part ν (A ∩ (S ∩ T)) = 0,
   { rw ← nonpos_iff_eq_zero,
-    exact hT₂ ▸ measure_mono
-      (set.subset.trans (set.inter_subset_right _ _) (set.inter_subset_right _ _)) },
-  rw [heq' A hA, heq, ← add_zero ((μ.singular_part ν).restrict (S ∩ T)ᶜ A), ← hμinter,
-      restrict_apply hA, ← measure_union, ← set.inter_union_distrib_left,
-      set.compl_union_self, set.inter_univ],
-  { exact disjoint.inter_left' _ ( disjoint.inter_right' _ disjoint_compl_left) },
-  { measurability },
-  { measurability }
+    exact hT₂ ▸ measure_mono ((inter_subset_right _ _).trans (inter_subset_right _ _)) },
+  rw [heq' A hA, heq, restrict_apply hA, ← diff_eq, ae_disjoint.measure_diff_left hμinter]
 end
 
 lemma singular_part_zero (ν : measure α) : (0 : measure α).singular_part ν = 0 :=
@@ -335,7 +325,7 @@ begin
   obtain ⟨⟨S, hS₁, hS₂, hS₃⟩, ⟨T, hT₁, hT₂, hT₃⟩⟩ := ⟨hs, hsing⟩,
   rw hadd' at hadd,
   have hνinter : ν (S ∩ T)ᶜ = 0,
-  { rw set.compl_inter,
+  { rw compl_inter,
     refine nonpos_iff_eq_zero.1 (le_trans (measure_union_le _ _) _),
     rw [hT₃, hS₃, add_zero],
     exact le_refl _ },
@@ -344,12 +334,11 @@ begin
   { ext1 A hA,
     have hs : s (A ∩ (S ∩ T)) = 0,
     { rw ← nonpos_iff_eq_zero,
-      exact hS₂ ▸ measure_mono
-        (set.subset.trans (set.inter_subset_right _ _) (set.inter_subset_left _ _)) },
+      exact hS₂ ▸ measure_mono ((inter_subset_right _ _).trans (inter_subset_left _ _)) },
     have hsing : μ.singular_part ν (A ∩ (S ∩ T)) = 0,
     { rw ← nonpos_iff_eq_zero,
       exact hT₂ ▸ measure_mono
-        (set.subset.trans (set.inter_subset_right _ _) (set.inter_subset_right _ _)) },
+        ((inter_subset_right _ _).trans (inter_subset_right _ _)) },
     rw [restrict_apply hA, restrict_apply hA, ← add_zero (ν.with_density f (A ∩ (S ∩ T))),
         ← hs, ← add_apply, add_comm, ← hadd, add_apply, hsing, zero_add] },
   have heq' : ∀ A : set α, measurable_set A →
@@ -358,23 +347,16 @@ begin
     have hνfinter : ν.with_density f (A ∩ (S ∩ T)ᶜ) = 0,
     { rw ← nonpos_iff_eq_zero,
       exact with_density_absolutely_continuous ν f hνinter ▸
-        measure_mono (set.inter_subset_right _ _) },
+        measure_mono (inter_subset_right _ _) },
     rw [restrict_apply hA, ← add_zero (ν.with_density f (A ∩ (S ∩ T))), ← hνfinter,
-        ← measure_union, ← set.inter_union_distrib_left, set.union_compl_self, set.inter_univ],
-    { exact disjoint.inter_left' _ (disjoint.inter_right' _ disjoint_compl_right) },
-    { measurability },
-    { measurability } },
+        ← diff_eq, measure_inter_add_diff _ (hS₁.inter hT₁)] },
   ext1 A hA,
   have hνrn : ν.with_density (μ.rn_deriv ν) (A ∩ (S ∩ T)ᶜ) = 0,
   { rw ← nonpos_iff_eq_zero,
     exact with_density_absolutely_continuous ν (μ.rn_deriv ν) hνinter ▸
-      measure_mono (set.inter_subset_right _ _) },
+      measure_mono (inter_subset_right _ _) },
   rw [heq' A hA, heq, ← add_zero ((ν.with_density (μ.rn_deriv ν)).restrict (S ∩ T) A),
-      ← hνrn, restrict_apply hA, ← measure_union, ← set.inter_union_distrib_left,
-      set.union_compl_self, set.inter_univ],
-  { exact disjoint.inter_left' _ (disjoint.inter_right' _ disjoint_compl_right) },
-  { measurability },
-  { measurability }
+      ← hνrn, restrict_apply hA, ← diff_eq, measure_inter_add_diff _ (hS₁.inter hT₁)]
 end
 
 /-- Given measures `μ` and `ν`, if `s` is a measure mutually singular to `ν` and `f` is a
@@ -426,7 +408,7 @@ begin
   have hAmeas : measurable_set A,
   { exact measurable_set.Inter (λ n, (hf₁ n).compl) },
   have hA₂ : ∀ n : ℕ, (μ.to_signed_measure - ((1 / (n + 1) : ℝ≥0) • ν).to_signed_measure) ≤[A] 0,
-  { intro n, exact restrict_le_restrict_subset _ _ (hf₁ n).compl (hf₃ n) (set.Inter_subset _ _) },
+  { intro n, exact restrict_le_restrict_subset _ _ (hf₁ n).compl (hf₃ n) (Inter_subset _ _) },
   have hA₃ : ∀ n : ℕ, μ A ≤ (1 / (n + 1) : ℝ≥0) * ν A,
   { intro n,
     have := nonpos_of_restrict_le_zero _ (hA₂ n),
@@ -464,7 +446,7 @@ begin
   -- since `μ` and `ν` are not mutually singular, `μ A = 0` implies `ν Aᶜ > 0`
   rw mutually_singular at h, push_neg at h,
   have := h _ hAmeas hμ,
-  simp_rw [hA₁, set.compl_Inter, compl_compl] at this,
+  simp_rw [hA₁, compl_Inter, compl_compl] at this,
   -- as `Aᶜ = ⋃ n, f n`, `ν Aᶜ > 0` implies there exists some `n` such that `ν (f n) > 0`
   obtain ⟨n, hn⟩ := exists_measure_pos_of_not_measure_Union_null this,
   -- thus, choosing `f n` as the set `E` suffices
@@ -494,17 +476,17 @@ begin
     by_cases haA : a ∈ A,
     { by_cases f a ≤ g a,
       { simp only,
-        rw [set.indicator_of_mem haA, set.indicator_of_mem, set.indicator_of_not_mem, add_zero],
+        rw [indicator_of_mem haA, indicator_of_mem, indicator_of_not_mem, add_zero],
         simp only [le_refl, max_le_iff, and_true, h],
         { rintro ⟨_, hc⟩, exact false.elim ((not_lt.2 h) hc) },
         { exact ⟨haA, h⟩ } },
       { simp only,
-        rw [set.indicator_of_mem haA, set.indicator_of_mem _ f,
-            set.indicator_of_not_mem, zero_add],
+        rw [indicator_of_mem haA, indicator_of_mem _ f,
+            indicator_of_not_mem, zero_add],
         simp only [true_and, le_refl, max_le_iff, le_of_lt (not_le.1 h)],
         { rintro ⟨_, hc⟩, exact false.elim (h hc) },
         { exact ⟨haA, not_le.1 h⟩ } } },
-    { simp [set.indicator_of_not_mem haA] } },
+    { simp [indicator_of_not_mem haA] } },
   { exact measurable.indicator hg.1 (hA.inter (measurable_set_le hf.1 hg.1)) },
   { exact measurable.indicator hf.1 (hA.inter (measurable_set_lt hg.1 hf.1)) },
   { exact hA.inter (measurable_set_le hf.1 hg.1) },
@@ -520,13 +502,9 @@ begin
   have h₁ := hA.inter (measurable_set_le hf.1 hg.1),
   have h₂ := hA.inter (measurable_set_lt hg.1 hf.1),
   refine le_trans (max_measurable_le f g hf hg A hA) _,
-  refine le_trans (add_le_add (hg.2 _ h₁) (hf.2 _ h₂)) _,
-  { rw [← measure_union _ h₁ h₂],
-    { refine le_of_eq _,
-      congr, convert set.inter_union_compl A _,
-      ext a, simpa },
-    rintro x ⟨⟨-, hx₁⟩, -, hx₂⟩,
-    exact (not_le.2 hx₂) hx₁ }
+  refine (add_le_add (hg.2 _ h₁) (hf.2 _ h₂)).trans_eq _,
+  { simp only [← not_le, ← compl_set_of, ← diff_eq],
+    exact measure_inter_add_diff _ (measurable_set_le hf.1 hg.1) }
 end
 
 lemma supr_succ_eq_sup {α} (f : ℕ → α → ℝ≥0∞) (m : ℕ) (a : α) :
@@ -655,7 +633,7 @@ theorem have_lebesgue_decomposition_of_finite_measure [is_finite_measure μ] [is
     exact supr_le (λ i, (supr_mem_measurable_le _ hf₁ i).2 B hB) },
   haveI : is_finite_measure (ν.with_density ξ),
   { refine is_finite_measure_with_density _,
-    have hle' := hle set.univ measurable_set.univ,
+    have hle' := hle univ measurable_set.univ,
     rw [with_density_apply _ measurable_set.univ, measure.restrict_univ] at hle',
     exact ne_top_of_le_ne_top (measure_ne_top _ _) hle' },
   refine ⟨⟨μ₁, ξ⟩, hξm, _, _⟩,
@@ -673,7 +651,7 @@ theorem have_lebesgue_decomposition_of_finite_measure [is_finite_measure μ] [is
   -- since `E` is positive, we have `∫⁻ a in A ∩ E, ε + ξ a ∂ν ≤ μ (A ∩ E)` for all `A`
     have hε₂ : ∀ A : set α, measurable_set A → ∫⁻ a in A ∩ E, ε + ξ a ∂ν ≤ μ (A ∩ E),
     { intros A hA,
-      have := subset_le_of_restrict_le_restrict _ _ hE₁ hE₃ (set.inter_subset_right A E),
+      have := subset_le_of_restrict_le_restrict _ _ hE₁ hE₃ (inter_subset_right A E),
       rwa [zero_apply, to_signed_measure_sub_apply (hA.inter hE₁),
             measure.sub_apply (hA.inter hE₁) hle,
             ennreal.to_real_sub_of_le _ (ne_of_lt (measure_lt_top _ _)), sub_nonneg,
@@ -696,20 +674,16 @@ theorem have_lebesgue_decomposition_of_finite_measure [is_finite_measure μ] [is
       have : ∫⁻ a in A, (ξ + E.indicator (λ _, ε)) a ∂ν =
             ∫⁻ a in A ∩ E, ε + ξ a ∂ν + ∫⁻ a in A ∩ Eᶜ, ξ a ∂ν,
       { rw [lintegral_add measurable_const hξm, add_assoc,
-            ← lintegral_union (hA.inter hE₁) (hA.inter (hE₁.compl))
-              (disjoint.mono (set.inter_subset_right _ _) (set.inter_subset_right _ _)
-              disjoint_compl_right), set.inter_union_compl],
+            ← lintegral_union (hA.inter hE₁) (hA.inter hE₁.compl)
+              (disjoint.mono (inter_subset_right _ _) (inter_subset_right _ _)
+              disjoint_compl_right), inter_union_compl],
         simp_rw [pi.add_apply],
         rw [lintegral_add hξm (measurable.indicator measurable_const hE₁), add_comm],
         refine congr_fun (congr_arg has_add.add _) _,
         rw [set_lintegral_const, lintegral_indicator _ hE₁, set_lintegral_const,
-            measure.restrict_apply hE₁, set.inter_comm] },
-      conv_rhs { rw ← set.inter_union_compl A E },
-      rw [this, measure_union _ (hA.inter hE₁) (hA.inter hE₁.compl)],
-      { exact add_le_add (hε₂ A hA)
-          (hξle (A ∩ Eᶜ) (hA.inter hE₁.compl)) },
-      { exact disjoint.mono (set.inter_subset_right _ _) (set.inter_subset_right _ _)
-          disjoint_compl_right } },
+            measure.restrict_apply hE₁, inter_comm] },
+      rw [this, ← measure_inter_add_diff A hE₁],
+      exact add_le_add (hε₂ A hA) (hξle (A \ E) (hA.diff hE₁)) },
       have : ∫⁻ a, ξ a + E.indicator (λ _, ε) a ∂ν ≤ Sup (measurable_le_eval ν μ) :=
         le_Sup ⟨ξ + E.indicator (λ _, ε), hξε, rfl⟩,
   -- but this contradicts the maximality of `∫⁻ x, ξ x ∂ν`
@@ -717,7 +691,7 @@ theorem have_lebesgue_decomposition_of_finite_measure [is_finite_measure μ] [is
       rw [hξ₁, lintegral_add hξm (measurable.indicator (measurable_const) hE₁),
           lintegral_indicator _ hE₁, set_lintegral_const],
       refine ennreal.lt_add_right _ (ennreal.mul_pos_iff.2 ⟨ennreal.coe_pos.2 hε₁, hE₂⟩).ne',
-      have := measure_ne_top (ν.with_density ξ) set.univ,
+      have := measure_ne_top (ν.with_density ξ) univ,
       rwa [with_density_apply _ measurable_set.univ, measure.restrict_univ] at this },
   -- since `ν.with_density ξ ≤ μ`, it is clear that `μ = μ₁ + ν.with_density ξ`
   { rw hμ₁, ext1 A hA,
@@ -729,7 +703,7 @@ local attribute [instance] have_lebesgue_decomposition_of_finite_measure
 
 instance {S : μ.finite_spanning_sets_in {s : set α | measurable_set s}} (n : ℕ) :
   is_finite_measure (μ.restrict $ S.set n) :=
-⟨by { rw [restrict_apply measurable_set.univ, set.univ_inter], exact S.finite _ }⟩
+⟨by { rw [restrict_apply measurable_set.univ, univ_inter], exact S.finite _ }⟩
 
 /-- **The Lebesgue decomposition theorem**: Any pair of σ-finite measures `μ` and `ν`
 `have_lebesgue_decomposition`. That is to say, there exist a measure `ξ` and a measurable function
@@ -782,33 +756,33 @@ instance have_lebesgue_decomposition_of_sigma_finite
           { intros j hij,
             rw [hμn, ← nonpos_iff_eq_zero],
             refine le_trans ((singular_part_le _ _) _ ((S.set_mem i).inter (hA₁ i))) (le_of_eq _),
-            rw [restrict_apply ((S.set_mem i).inter (hA₁ i)), set.inter_comm, ← set.inter_assoc],
+            rw [restrict_apply ((S.set_mem i).inter (hA₁ i)), inter_comm, ← inter_assoc],
             have : disjoint (S.set j) (S.set i) := h₂ j i hij,
-            rw set.disjoint_iff_inter_eq_empty at this,
-            rw [this, set.empty_inter, measure_empty] },
+            rw disjoint_iff_inter_eq_empty at this,
+            rw [this, empty_inter, measure_empty] },
           { apply_instance } },
         simp_rw [this, tsum_eq_zero_iff ennreal.summable],
-        intro n, exact measure_mono_null (set.inter_subset_right _ _) (hA₂ n) },
+        intro n, exact measure_mono_null (inter_subset_right _ _) (hA₂ n) },
       { exact h₂.mono (λ i j, disjoint.mono inf_le_left inf_le_left) },
       { exact λ n, (S.set_mem n).inter (hA₁ n) } },
   -- We will now show `ν Bᶜ = 0`. This follows since `Bᶜ = ⋃ n, S.set n ∩ (A n)ᶜ` and thus,
   -- `ν Bᶜ = ∑ i, ν (S.set i ∩ (A i)ᶜ) = ∑ i, (νn i) (A i)ᶜ = 0`
     { have hcompl : is_compl (⋃ n, (S.set n ∩ A n)) (⋃ n, S.set n ∩ (A n)ᶜ),
       { split,
-        { rintro x ⟨hx₁, hx₂⟩, rw set.mem_Union at hx₁ hx₂,
+        { rintro x ⟨hx₁, hx₂⟩, rw mem_Union at hx₁ hx₂,
           obtain ⟨⟨i, hi₁, hi₂⟩, ⟨j, hj₁, hj₂⟩⟩ := ⟨hx₁, hx₂⟩,
           have : i = j,
           { by_contra hij, exact h₂ i j hij ⟨hi₁, hj₁⟩ },
           exact hj₂ (this ▸ hi₂) },
         { intros x hx,
-          simp only [set.mem_Union, set.sup_eq_union, set.mem_inter_eq,
-                    set.mem_union_eq, set.mem_compl_eq, or_iff_not_imp_left],
+          simp only [mem_Union, sup_eq_union, mem_inter_eq,
+                    mem_union_eq, mem_compl_eq, or_iff_not_imp_left],
           intro h, push_neg at h,
-          rw [set.top_eq_univ, ← S.spanning, set.mem_Union] at hx,
+          rw [top_eq_univ, ← S.spanning, mem_Union] at hx,
           obtain ⟨i, hi⟩ := hx,
           exact ⟨i, hi, h i hi⟩ } },
       rw [hcompl.compl_eq, measure_Union, tsum_eq_zero_iff ennreal.summable],
-      { intro n, rw [set.inter_comm, ← restrict_apply (hA₁ n).compl, ← hA₃ n, hνn, h₁] },
+      { intro n, rw [inter_comm, ← restrict_apply (hA₁ n).compl, ← hA₃ n, hνn, h₁] },
       { exact h₂.mono (λ i j, disjoint.mono inf_le_left inf_le_left) },
       { exact λ n, (S.set_mem n).inter (hA₁ n).compl } } },
   -- Finally, it remains to show `μ = ξ + ν.with_density f`. Since `μ = sum μn`, and
@@ -828,10 +802,10 @@ instance have_lebesgue_decomposition_of_sigma_finite
       { rw hsumeq },
       ext1 s hs,
       rw [sum_apply _ hs, tsum_eq_single n, hνn, h₁,
-          restrict_restrict (T.set_mem n), set.inter_self],
+          restrict_restrict (T.set_mem n), inter_self],
       { intros m hm,
-        rw [hνn, h₁, restrict_restrict (T.set_mem n), set.inter_comm,
-            set.disjoint_iff_inter_eq_empty.1 (h₃ m n hm), restrict_empty,
+        rw [hνn, h₁, restrict_restrict (T.set_mem n),
+            disjoint_iff_inter_eq_empty.1 (h₃ n m hm.symm), restrict_empty,
             coe_zero, pi.zero_apply] },
       { apply_instance } },
     { exact λ n, measurable.indicator (measurable_rn_deriv _ _) (S.set_mem n) } },
diff --git a/src/measure_theory/decomposition/radon_nikodym.lean b/src/measure_theory/decomposition/radon_nikodym.lean
index 3de23f002f72e..4e59ac27bcd84 100644
--- a/src/measure_theory/decomposition/radon_nikodym.lean
+++ b/src/measure_theory/decomposition/radon_nikodym.lean
@@ -51,8 +51,7 @@ begin
     suffices : singular_part μ ν set.univ = 0,
     { rw [measure.coe_zero, pi.zero_apply, ← this],
       exact measure_mono (set.subset_univ _) },
-    rw [← set.union_compl_self E, measure_union (@disjoint_compl_right _ E _) hE₁ hE₁.compl,
-        hE₂, zero_add],
+    rw [← measure_add_measure_compl hE₁, hE₂, zero_add],
     have : (singular_part μ ν + ν.with_density (rn_deriv μ ν)) Eᶜ = μ Eᶜ,
     { rw ← hadd },
     rw [measure.coe_add, pi.add_apply, h hE₃] at this,
diff --git a/src/measure_theory/function/continuous_map_dense.lean b/src/measure_theory/function/continuous_map_dense.lean
index 990f3a4d05684..2da80841f71db 100644
--- a/src/measure_theory/function/continuous_map_dense.lean
+++ b/src/measure_theory/function/continuous_map_dense.lean
@@ -110,9 +110,7 @@ begin
       from μu.trans (ennreal.add_lt_add_right ennreal.coe_ne_top μF),
     convert this.le using 1,
     { rw [add_comm, ← measure_union, set.diff_union_of_subset (Fs.trans su)],
-      { exact disjoint_sdiff_self_left },
-      { exact (u_open.sdiff F_closed).measurable_set },
-      { exact F_closed.measurable_set } },
+      exacts [disjoint_sdiff_self_left, F_closed.measurable_set] },
     have : (2:ℝ≥0∞) * η = η + η := by simpa using add_mul (1:ℝ≥0∞) 1 η,
     rw this,
     abel },
diff --git a/src/measure_theory/group/fundamental_domain.lean b/src/measure_theory/group/fundamental_domain.lean
index 7948f9f1cecf6..b74c554c8a1b5 100644
--- a/src/measure_theory/group/fundamental_domain.lean
+++ b/src/measure_theory/group/fundamental_domain.lean
@@ -209,7 +209,7 @@ begin
     calc ∫ x in s, f x ∂μ = ∫ x in ⋃ g : G, g • t, f x ∂(μ.restrict s) :
       by rw [restrict_congr_set (hac ht.Union_smul_ae_eq), restrict_univ]
     ... = ∑' g : G, ∫ x in g • t, f x ∂(μ.restrict s) :
-      integral_Union_of_null_inter ht.measurable_set_smul
+      integral_Union_of_null_inter (λ g, (ht.measurable_set_smul g).null_measurable_set)
         (ht.pairwise_ae_disjoint.mono $ λ i j h, hac h) hfs.integrable.integrable_on
     ... = ∑' g : G, ∫ x in s ∩ g • t, f x ∂μ :
       by simp only [restrict_restrict (ht.measurable_set_smul _), inter_comm]
@@ -222,7 +222,7 @@ begin
     ... = ∑' g : G, ∫ x in g • s, f x ∂(μ.restrict t) :
       by simp only [hf, restrict_restrict (hs.measurable_set_smul _)]
     ... = ∫ x in ⋃ g : G, g • s, f x ∂(μ.restrict t) :
-      (integral_Union_of_null_inter hs.measurable_set_smul
+      (integral_Union_of_null_inter (λ g, (hs.measurable_set_smul g).null_measurable_set)
         (hs.pairwise_ae_disjoint.mono $ λ i j h, hac h) hft.integrable.integrable_on).symm
     ... = ∫ x in t, f x ∂μ :
       by rw [restrict_congr_set (hac hs.Union_smul_ae_eq), restrict_univ] },
diff --git a/src/measure_theory/integral/bochner.lean b/src/measure_theory/integral/bochner.lean
index 960dd4b26d0b6..33c9d90f6b877 100644
--- a/src/measure_theory/integral/bochner.lean
+++ b/src/measure_theory/integral/bochner.lean
@@ -203,16 +203,22 @@ by { ext1 x, simp_rw weighted_smul_apply, congr' 2, }
 lemma weighted_smul_null {s : set α} (h_zero : μ s = 0) : (weighted_smul μ s : F →L[ℝ] F) = 0 :=
 by { ext1 x, rw [weighted_smul_apply, h_zero], simp, }
 
-lemma weighted_smul_union (s t : set α) (hs : measurable_set s) (ht : measurable_set t)
+lemma weighted_smul_union' (s t : set α) (ht : measurable_set t)
   (hs_finite : μ s ≠ ∞) (ht_finite : μ t ≠ ∞) (h_inter : s ∩ t = ∅) :
   (weighted_smul μ (s ∪ t) : F →L[ℝ] F) = weighted_smul μ s + weighted_smul μ t :=
 begin
   ext1 x,
   simp_rw [add_apply, weighted_smul_apply,
-    measure_union (set.disjoint_iff_inter_eq_empty.mpr h_inter) hs ht,
+    measure_union (set.disjoint_iff_inter_eq_empty.mpr h_inter) ht,
     ennreal.to_real_add hs_finite ht_finite, add_smul],
 end
 
+@[nolint unused_arguments]
+lemma weighted_smul_union (s t : set α) (hs : measurable_set s) (ht : measurable_set t)
+  (hs_finite : μ s ≠ ∞) (ht_finite : μ t ≠ ∞) (h_inter : s ∩ t = ∅) :
+  (weighted_smul μ (s ∪ t) : F →L[ℝ] F) = weighted_smul μ s + weighted_smul μ t :=
+weighted_smul_union' s t ht hs_finite ht_finite h_inter
+
 lemma weighted_smul_smul [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class ℝ 𝕜 F]
   (c : 𝕜) (s : set α) (x : F) :
   weighted_smul μ s (c • x) = c • weighted_smul μ s x :=
diff --git a/src/measure_theory/integral/interval_integral.lean b/src/measure_theory/integral/interval_integral.lean
index 4bd09eb2976e8..3c6b84e849595 100644
--- a/src/measure_theory/integral/interval_integral.lean
+++ b/src/measure_theory/integral/interval_integral.lean
@@ -853,9 +853,9 @@ lemma integral_Iic_sub_Iic (ha : integrable_on f (Iic a) μ) (hb : integrable_on
   ∫ x in Iic b, f x ∂μ - ∫ x in Iic a, f x ∂μ = ∫ x in a..b, f x ∂μ :=
 begin
   wlog hab : a ≤ b using [a b] tactic.skip,
-  { rw [sub_eq_iff_eq_add', integral_of_le hab, ← integral_union (Iic_disjoint_Ioc (le_refl _)),
+  { rw [sub_eq_iff_eq_add', integral_of_le hab, ← integral_union (Iic_disjoint_Ioc le_rfl),
       Iic_union_Ioc_eq_Iic hab],
-    exacts [measurable_set_Iic, measurable_set_Ioc, ha, hb.mono_set (λ _, and.right)] },
+    exacts [measurable_set_Ioc, ha, hb.mono_set (λ _, and.right)] },
   { intros ha hb,
     rw [integral_symm, ← this hb ha, neg_sub] }
 end
diff --git a/src/measure_theory/integral/set_integral.lean b/src/measure_theory/integral/set_integral.lean
index db33e43f8f819..def0f021d795a 100644
--- a/src/measure_theory/integral/set_integral.lean
+++ b/src/measure_theory/integral/set_integral.lean
@@ -72,27 +72,22 @@ lemma set_integral_congr_set_ae (hst : s =ᵐ[μ] t) :
   ∫ x in s, f x ∂μ = ∫ x in t, f x ∂μ :=
 by rw measure.restrict_congr_set hst
 
-lemma integral_union (hst : disjoint s t) (hs : measurable_set s) (ht : measurable_set t)
+lemma integral_union_ae (hst : ae_disjoint μ s t) (ht : null_measurable_set t μ)
   (hfs : integrable_on f s μ) (hft : integrable_on 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 hs ht, integral_add_measure hfs hft]
+by simp only [integrable_on, measure.restrict_union₀ hst ht, integral_add_measure hfs hft]
 
-lemma integral_union_ae (hst : (s ∩ t : set α) =ᵐ[μ] (∅ : set α)) (hs : measurable_set s)
-  (ht : measurable_set t) (hfs : integrable_on f s μ) (hft : integrable_on f t μ) :
+lemma integral_union (hst : disjoint s t) (ht : measurable_set t)
+  (hfs : integrable_on f s μ) (hft : integrable_on f t μ) :
   ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ + ∫ x in t, f x ∂μ :=
-begin
-  have : s =ᵐ[μ] s \ t,
-  { refine (hst.mem_iff.mono _).set_eq, simp },
-  rw [← diff_union_self, integral_union disjoint_diff.symm, set_integral_congr_set_ae this],
-  exacts [hs.diff ht, ht, hfs.mono_set (diff_subset _ _), hft]
-end
+integral_union_ae hst.ae_disjoint ht.null_measurable_set hfs hft
 
-lemma integral_diff (hs : measurable_set s) (ht : measurable_set t) (hfs : integrable_on f s μ)
+lemma integral_diff (ht : measurable_set t) (hfs : integrable_on f s μ)
   (hft : integrable_on f t μ) (hts : t ⊆ s) :
   ∫ x in s \ t, f x ∂μ = ∫ x in s, f x ∂μ - ∫ x in t, f x ∂μ :=
 begin
   rw [eq_sub_iff_add_eq, ← integral_union, diff_union_of_subset hts],
-  exacts [disjoint_diff.symm, hs.diff ht, ht, hfs.mono_set (diff_subset _ _), hft]
+  exacts [disjoint_diff.symm, ht, hfs.mono_set (diff_subset _ _), hft]
 end
 
 lemma integral_finset_bUnion {ι : Type*} (t : finset ι) {s : ι → set α}
@@ -104,7 +99,7 @@ begin
   { simp },
   { simp only [finset.coe_insert, finset.forall_mem_insert, set.pairwise_insert,
       finset.set_bUnion_insert] at hs hf h's ⊢,
-    rw [integral_union _ hs.1 _ hf.1 (integrable_on_finset_Union.2 hf.2)],
+    rw [integral_union _ _ hf.1 (integrable_on_finset_Union.2 hf.2)],
     { rw [finset.sum_insert hat, IH hs.2 h's.1 hf.2] },
     { simp only [disjoint_Union_right],
       exact (λ i hi, (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1) },
@@ -127,7 +122,7 @@ lemma integral_univ : ∫ x in univ, f x ∂μ = ∫ x, f x ∂μ := by rw [meas
 
 lemma integral_add_compl (hs : measurable_set s) (hfi : integrable f μ) :
   ∫ x in s, f x ∂μ + ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ :=
-by rw [← integral_union (@disjoint_compl_right (set α) _ _) hs hs.compl
+by rw [← integral_union (@disjoint_compl_right (set α) _ _) hs.compl
     hfi.integrable_on hfi.integrable_on, union_compl_self, integral_univ]
 
 /-- For a function `f` and a measurable set `s`, the integral of `indicator s f`
@@ -162,10 +157,10 @@ begin
   have : ∀ᶠ i in at_top, ν (s i) ∈ Icc (ν S - ε) (ν S + ε),
     from tendsto_measure_Union hsm h_mono (ennreal.Icc_mem_nhds hfi'.ne (ennreal.coe_pos.2 ε0).ne'),
   refine this.mono (λ i hi, _),
-  rw [mem_closed_ball_iff_norm', ← integral_diff hSm (hsm i) hfi (hfi.mono_set hsub) hsub,
+  rw [mem_closed_ball_iff_norm', ← integral_diff (hsm i) hfi (hfi.mono_set hsub) hsub,
     ← coe_nnnorm, nnreal.coe_le_coe, ← ennreal.coe_le_coe],
   refine (ennnorm_integral_le_lintegral_ennnorm _).trans _,
-  rw [← with_density_apply _ (hSm.diff (hsm _)), ← hν, measure_diff hsub hSm (hsm _)],
+  rw [← with_density_apply _ (hSm.diff (hsm _)), ← hν, measure_diff hsub (hsm _)],
   exacts [tsub_le_iff_tsub_le.mp hi.1,
     (hi.2.trans_lt $ ennreal.add_lt_top.2 ⟨hfi', ennreal.coe_lt_top⟩).ne]
 end
@@ -189,7 +184,7 @@ lemma integral_Union {ι : Type*} [encodable ι] {s : ι → set α} {f : α →
 (has_sum.tsum_eq (has_sum_integral_Union hm hd hfi)).symm
 
 lemma has_sum_integral_Union_of_null_inter {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
-  (hm : ∀ i, measurable_set (s i)) (hd : pairwise (λ i j, μ (s i ∩ s j) = 0))
+  (hm : ∀ i, null_measurable_set (s i) μ) (hd : pairwise (ae_disjoint μ on s))
   (hfi : integrable_on f (⋃ i, s i) μ) :
   has_sum (λ n, ∫ a in s n, f a ∂ μ) (∫ a in ⋃ n, s n, f a ∂μ) :=
 begin
@@ -200,7 +195,7 @@ begin
 end
 
 lemma integral_Union_of_null_inter {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
-  (hm : ∀ i, measurable_set (s i)) (hd : pairwise (λ i j, μ (s i ∩ s j) = 0))
+  (hm : ∀ i, null_measurable_set (s i) μ) (hd : pairwise (ae_disjoint μ on s))
   (hfi : integrable_on f (⋃ i, s i) μ) :
   (∫ a in (⋃ n, s n), f a ∂μ) = ∑' n, ∫ a in s n, f a ∂ μ :=
 (has_sum.tsum_eq (has_sum_integral_Union_of_null_inter hm hd hfi)).symm
@@ -216,20 +211,13 @@ begin
   exact ht_eq x hx,
 end
 
-private lemma set_integral_union_eq_left_of_disjoint {f : α → E} (hf : measurable f)
-  (hfi : integrable f μ) (hs : measurable_set s) (ht : measurable_set t) (ht_eq : ∀ x ∈ t, f x = 0)
-  (hs_disj : disjoint s t) :
-  ∫ x in (s ∪ t), f x ∂μ = ∫ x in s, f x ∂μ :=
-by rw [integral_union hs_disj hs ht hfi.integrable_on hfi.integrable_on,
-  set_integral_eq_zero_of_forall_eq_zero hf ht_eq, add_zero]
-
 lemma set_integral_union_eq_left {f : α → E} (hf : measurable f) (hfi : integrable f μ)
-  (hs : measurable_set s) (ht : measurable_set t) (ht_eq : ∀ x ∈ t, f x = 0) :
+  (hs : measurable_set s) (ht_eq : ∀ x ∈ t, f x = 0) :
   ∫ x in (s ∪ t), f x ∂μ = ∫ x in s, f x ∂μ :=
 begin
-  rw [← set.union_diff_self, integral_union,
-    set_integral_eq_zero_of_forall_eq_zero _ (λ x hx, ht_eq x (diff_subset _ _ hx)), add_zero],
-  exacts [hf, disjoint_diff, hs, ht.diff hs, hfi.integrable_on, hfi.integrable_on]
+  rw [← set.union_diff_self, union_comm, integral_union,
+    set_integral_eq_zero_of_forall_eq_zero _ (λ x hx, ht_eq x (diff_subset _ _ hx)), zero_add],
+  exacts [hf, disjoint_diff.symm, hs, hfi.integrable_on, hfi.integrable_on]
 end
 
 lemma set_integral_neg_eq_set_integral_nonpos [linear_order E] [order_closed_topology E]
@@ -240,7 +228,7 @@ begin
     by { ext, simp_rw [set.mem_union_eq, set.mem_set_of_eq], exact le_iff_lt_or_eq, },
   rw h_union,
   exact (set_integral_union_eq_left hf hfi (measurable_set_lt hf measurable_const)
-    (measurable_set_eq_fun hf measurable_const) (λ x hx, hx)).symm,
+    (λ x hx, hx)).symm,
 end
 
 lemma integral_norm_eq_pos_sub_neg {f : α → ℝ} (hf : measurable f) (hfi : integrable f μ) :
diff --git a/src/measure_theory/measure/ae_disjoint.lean b/src/measure_theory/measure/ae_disjoint.lean
index 0586b56c9a6f4..c98a865de429f 100644
--- a/src/measure_theory/measure/ae_disjoint.lean
+++ b/src/measure_theory/measure/ae_disjoint.lean
@@ -82,6 +82,16 @@ union_left_iff.mpr ⟨hs, ht⟩
 lemma union_right (ht : ae_disjoint μ s t) (hu : ae_disjoint μ s u) : ae_disjoint μ s (t ∪ u) :=
 union_right_iff.2 ⟨ht, hu⟩
 
+lemma diff_ae_eq_left (h : ae_disjoint μ s t) : (s \ t : set α) =ᵐ[μ] s :=
+@diff_self_inter _ s t ▸ diff_null_ae_eq_self h
+
+lemma diff_ae_eq_right (h : ae_disjoint μ s t) : (t \ s : set α) =ᵐ[μ] t := h.symm.diff_ae_eq_left
+
+lemma measure_diff_left (h : ae_disjoint μ s t) : μ (s \ t) = μ s := measure_congr h.diff_ae_eq_left
+
+lemma measure_diff_right (h : ae_disjoint μ s t) : μ (t \ s) = μ t :=
+measure_congr h.diff_ae_eq_right
+
 /-- If `s` and `t` are `μ`-a.e. disjoint, then `s \ u` and `t` are disjoint for some measurable null
 set `u`. -/
 lemma exists_disjoint_diff (h : ae_disjoint μ s t) :
diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean
index 497f186fea640..34a33fd2bcd4a 100644
--- a/src/measure_theory/measure/haar_lebesgue.lean
+++ b/src/measure_theory/measure/haar_lebesgue.lean
@@ -440,12 +440,10 @@ by rw [add_haar_closed_ball' μ x hr, add_haar_closed_unit_ball_eq_add_haar_unit
 lemma add_haar_sphere_of_ne_zero (x : E) {r : ℝ} (hr : r ≠ 0) :
   μ (sphere x r) = 0 :=
 begin
-  rcases lt_trichotomy r 0 with h|rfl|h,
+  rcases hr.lt_or_lt with h|h,
   { simp only [empty_diff, measure_empty, ← closed_ball_diff_ball, closed_ball_eq_empty.2 h] },
-  { exact (hr rfl).elim },
   { rw [← closed_ball_diff_ball,
-        measure_diff ball_subset_closed_ball measurable_set_closed_ball measurable_set_ball
-          measure_ball_lt_top.ne,
+        measure_diff ball_subset_closed_ball measurable_set_ball measure_ball_lt_top.ne,
         add_haar_ball_of_pos μ _ h, add_haar_closed_ball μ _ h.le, tsub_self];
     apply_instance }
 end
@@ -454,8 +452,7 @@ lemma add_haar_sphere [nontrivial E] (x : E) (r : ℝ) :
   μ (sphere x r) = 0 :=
 begin
   rcases eq_or_ne r 0 with rfl|h,
-  { simp only [← closed_ball_diff_ball, diff_empty, closed_ball_zero,
-               ball_zero, measure_singleton] },
+  { rw [sphere_zero, measure_singleton] },
   { exact add_haar_sphere_of_ne_zero μ x h }
 end
 
diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean
index f6d03c1458222..978d1b6fa872e 100644
--- a/src/measure_theory/measure/measure_space.lean
+++ b/src/measure_theory/measure/measure_space.lean
@@ -103,13 +103,34 @@ instance ae_is_measurably_generated : is_measurably_generated μ.ae :=
 ⟨λ s hs, let ⟨t, hst, htm, htμ⟩ := exists_measurable_superset_of_null hs in
   ⟨tᶜ, compl_mem_ae_iff.2 htμ, htm.compl, compl_subset_comm.1 hst⟩⟩
 
-lemma measure_union (hd : disjoint s₁ s₂) (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
+lemma measure_union (hd : disjoint s₁ s₂) (h : measurable_set s₂) :
   μ (s₁ ∪ s₂) = μ s₁ + μ s₂ :=
-measure_union₀ h₁.null_measurable_set h₂.null_measurable_set hd
+measure_union₀ h.null_measurable_set hd.ae_disjoint
+
+lemma measure_union' (hd : disjoint s₁ s₂) (h : measurable_set s₁) :
+  μ (s₁ ∪ s₂) = μ s₁ + μ s₂ :=
+measure_union₀' h.null_measurable_set hd.ae_disjoint
+
+lemma measure_inter_add_diff (s : set α) (ht : measurable_set t) :
+  μ (s ∩ t) + μ (s \ t) = μ s :=
+measure_inter_add_diff₀ _ ht.null_measurable_set
+
+lemma measure_diff_add_inter (s : set α) (ht : measurable_set t) :
+  μ (s \ t) + μ (s ∩ t) = μ s :=
+(add_comm _ _).trans (measure_inter_add_diff s ht)
+
+lemma measure_union_add_inter (s : set α) (ht : measurable_set t) :
+  μ (s ∪ t) + μ (s ∩ t) = μ s + μ t :=
+by { rw [← measure_inter_add_diff (s ∪ t) ht, set.union_inter_cancel_right,
+  union_diff_right, ← measure_inter_add_diff s ht], ac_refl }
+
+lemma measure_union_add_inter' (hs : measurable_set s) (t : set α) :
+  μ (s ∪ t) + μ (s ∩ t) = μ s + μ t :=
+by rw [union_comm, inter_comm, measure_union_add_inter t hs, add_comm]
 
 lemma measure_add_measure_compl (h : measurable_set s) :
   μ s + μ sᶜ = μ univ :=
-by { rw [← union_compl_self s, measure_union _ h h.compl], exact disjoint_compl_right }
+by { rw [← measure_union' _ h, union_compl_self], exact disjoint_compl_right }
 
 lemma measure_bUnion {s : set β} {f : β → set α} (hs : countable s)
   (hd : s.pairwise (disjoint on f)) (h : ∀ b ∈ s, measurable_set (f b)) :
@@ -154,12 +175,11 @@ measure_congr $ diff_ae_eq_self.2 h
 lemma measure_diff_null (h : μ s₂ = 0) : μ (s₁ \ s₂) = μ s₁ :=
 measure_diff_null' $ measure_mono_null (inter_subset_right _ _) h
 
-lemma measure_diff (h : s₂ ⊆ s₁) (h₁ : measurable_set s₁) (h₂ : measurable_set s₂)
-  (h_fin : μ s₂ ≠ ∞) :
+lemma measure_diff (h : s₂ ⊆ s₁) (h₂ : measurable_set s₂) (h_fin : μ s₂ ≠ ∞) :
   μ (s₁ \ s₂) = μ s₁ - μ s₂ :=
 begin
   refine (ennreal.add_sub_self' h_fin).symm.trans _,
-  rw [← measure_union disjoint_diff h₂ (h₁.diff h₂), union_diff_cancel h]
+  rw [← measure_union' disjoint_diff h₂, union_diff_cancel h]
 end
 
 lemma le_measure_diff : μ s₁ - μ s₂ ≤ μ (s₁ \ s₂) :=
@@ -168,20 +188,20 @@ calc μ s₁ ≤ μ (s₂ ∪ s₁)        : measure_mono (subset_union_right _
       ... = μ (s₂ ∪ s₁ \ s₂)   : congr_arg μ union_diff_self.symm
       ... ≤ μ s₂ + μ (s₁ \ s₂) : measure_union_le _ _
 
-lemma measure_diff_lt_of_lt_add (hs : measurable_set s) (ht : measurable_set t) (hst : s ⊆ t)
+lemma measure_diff_lt_of_lt_add (hs : measurable_set s) (hst : s ⊆ t)
   (hs' : μ s ≠ ∞) {ε : ℝ≥0∞} (h : μ t < μ s + ε) : μ (t \ s) < ε :=
 begin
-  rw [measure_diff hst ht hs hs'], rw add_comm at h,
+  rw [measure_diff hst hs hs'], rw add_comm at h,
   exact ennreal.sub_lt_of_lt_add (measure_mono hst) h
 end
 
-lemma measure_diff_le_iff_le_add (hs : measurable_set s) (ht : measurable_set t) (hst : s ⊆ t)
+lemma measure_diff_le_iff_le_add (hs : measurable_set s) (hst : s ⊆ t)
   (hs' : μ s ≠ ∞) {ε : ℝ≥0∞} : μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε :=
-by rwa [measure_diff hst ht hs hs', tsub_le_iff_left]
+by rwa [measure_diff hst hs hs', tsub_le_iff_left]
 
-lemma measure_eq_measure_of_null_diff {s t : set α}
-  (hst : s ⊆ t) (h_nulldiff : μ (t.diff s) = 0) : μ s = μ t :=
-by { rw [←diff_diff_cancel_left hst, ←@measure_diff_null _ _ _ t _ h_nulldiff], refl, }
+lemma measure_eq_measure_of_null_diff {s t : set α} (hst : s ⊆ t) (h_nulldiff : μ (t \ s) = 0) :
+  μ s = μ t :=
+measure_congr (hst.eventually_le.antisymm $ ae_le_set.mpr h_nulldiff)
 
 lemma measure_eq_measure_of_between_null_diff {s₁ s₂ s₃ : set α}
   (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃) (h_nulldiff : μ (s₃ \ s₁) = 0) :
@@ -205,7 +225,7 @@ lemma measure_eq_measure_larger_of_between_null_diff {s₁ s₂ s₃ : set α}
 (measure_eq_measure_of_between_null_diff h12 h23 h_nulldiff).2
 
 lemma measure_compl (h₁ : measurable_set s) (h_fin : μ s ≠ ∞) : μ (sᶜ) = μ univ - μ s :=
-by { rw compl_eq_univ_diff, exact measure_diff (subset_univ s) measurable_set.univ h₁ h_fin }
+by { rw compl_eq_univ_diff, exact measure_diff (subset_univ s) h₁ h_fin }
 
 lemma sum_measure_le_measure_univ {s : finset ι} {t : ι → set α} (h : ∀ i ∈ s, measurable_set (t i))
   (H : set.pairwise ↑s (disjoint on t)) :
@@ -220,34 +240,6 @@ begin
   exact supr_le (λ s, sum_measure_le_measure_univ (λ i hi, hs i) (λ i hi j hj hij, H i j hij))
 end
 
-/-- If `sᵢ` is a countable family of measurable sets such that all pairwise intersections have
-measure `0`, then there exists a subordinate family `tᵢ ⊆ sᵢ` of measurable pairwise disjoint sets
-such that `tᵢ =ᵐ[μ] sᵢ`. -/
-lemma exists_subordinate_pairwise_disjoint [encodable ι] {s : ι → set α}
-  (h : ∀ i, measurable_set (s i)) (hd : pairwise (λ i j, μ (s i ∩ s j) = 0)) :
-  ∃ t : ι → set α, (∀ i, t i ⊆ s i) ∧ (∀ i, s i =ᵐ[μ] t i) ∧ (∀ i, measurable_set (t i)) ∧
-    pairwise (disjoint on t) :=
-begin
-  set t : ι → set α := λ i, s i \ ⋃ j ∈ ({i}ᶜ : set ι), s j,
-  refine ⟨t, λ i, diff_subset _ _, λ i, _, λ i, (h i).diff $
-    measurable_set.bUnion (countable_encodable _) $ λ j hj, h j, _⟩,
-  { refine eventually_le.antisymm _ (diff_subset _ _).eventually_le,
-    rw [ae_le_set, sdiff_sdiff_right_self, inf_eq_inter],
-    simp only [inter_Union, measure_bUnion_null_iff (countable_encodable _)],
-    exact λ j hj, hd _ _ (ne.symm hj) },
-  { rintros i j hne x ⟨⟨hsi, -⟩, -, Hj⟩,
-    exact Hj (mem_bUnion hne hsi) }
-end
-
-lemma measure_Union_of_null_inter [encodable ι] {f : ι → set α} (h : ∀ i, measurable_set (f i))
-  (hn : pairwise ((λ S T, μ (S ∩ T) = 0) on f)) : μ (⋃ i, f i) = ∑' i, μ (f i) :=
-begin
-  rcases exists_subordinate_pairwise_disjoint h hn with ⟨t, ht_sub, ht_eq, htm, htd⟩,
-  calc μ (⋃ i, f i) = μ (⋃ i, t i)  : measure_congr (eventually_eq.countable_Union ht_eq)
-                ... = ∑' i, μ (t i) : measure_Union htd htm
-                ... = ∑' i, μ (f i) : tsum_congr (λ i, measure_congr (ht_eq i).symm)
-end
-
 /-- Pigeonhole principle for measure spaces: if `∑' i, μ (s i) > μ univ`, then
 one of the intersections `s i ∩ s j` is not empty. -/
 lemma exists_nonempty_inter_of_measure_univ_lt_tsum_measure {m : measurable_space α} (μ : measure α)
@@ -316,16 +308,15 @@ begin
   have : ∀ t ⊆ s k, μ t ≠ ∞, from λ t ht, ne_top_of_le_ne_top hk (measure_mono ht),
   rw [← ennreal.sub_sub_cancel (by exact hk) (infi_le _ k), ennreal.sub_infi,
     ← ennreal.sub_sub_cancel (by exact hk) (measure_mono (Inter_subset _ k)),
-    ← measure_diff (Inter_subset _ k) (h k) (measurable_set.Inter h) (this _ (Inter_subset _ k)),
+    ← measure_diff (Inter_subset _ k) (measurable_set.Inter h) (this _ (Inter_subset _ k)),
     diff_Inter, measure_Union_eq_supr],
   { congr' 1,
     refine le_antisymm (supr_le_supr2 $ λ i, _) (supr_le_supr $ λ i, _),
     { rcases hd i k with ⟨j, hji, hjk⟩,
       use j,
-      rw [← measure_diff hjk (h _) (h _) (this _ hjk)],
+      rw [← measure_diff hjk (h _) (this _ hjk)],
       exact measure_mono (diff_subset_diff_right hji) },
-    { rw [tsub_le_iff_right, ← measure_union disjoint_diff.symm ((h k).diff (h i)) (h i),
-        set.union_comm],
+    { rw [tsub_le_iff_right, ← measure_union disjoint_diff.symm (h i), set.union_comm],
       exact measure_mono (diff_subset_iff.1 $ subset.refl _) } },
   { exact λ i, (h k).diff (h i) },
   { exact hd.mono_comp _ (λ _ _, diff_subset_diff_right) }
@@ -439,17 +430,7 @@ measure.of_measurable (λ s _, m s) m.empty
   (λ f hf hd, m.Union_eq_of_caratheodory (λ i, h _ (hf i)) hd)
 
 lemma le_to_outer_measure_caratheodory (μ : measure α) : ms ≤ μ.to_outer_measure.caratheodory :=
-begin
-  assume s hs,
-  rw to_outer_measure_eq_induced_outer_measure,
-  refine outer_measure.of_function_caratheodory (λ t, le_infi $ λ ht, _),
-  rw [← measure_eq_extend (ht.inter hs),
-    ← measure_eq_extend (ht.diff hs),
-    ← measure_union _ (ht.inter hs) (ht.diff hs),
-    inter_union_diff],
-  exact le_refl _,
-  exact λ x ⟨⟨_, h₁⟩, _, h₂⟩, h₂ h₁
-end
+λ s hs t, (measure_inter_add_diff _ hs).symm
 
 @[simp] lemma to_measure_to_outer_measure (m : outer_measure α) (h : ms ≤ m.caratheodory) :
   (m.to_measure h).to_outer_measure = m.trim := rfl
@@ -485,18 +466,6 @@ end outer_measure
 variables {m0 : measurable_space α} [measurable_space β] [measurable_space γ]
 variables {μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : measure α} {s s' t : set α}
 
-lemma measure_inter_add_diff (s : set α) (ht : measurable_set t) :
-  μ (s ∩ t) + μ (s \ t) = μ s :=
-(le_to_outer_measure_caratheodory μ _ ht _).symm
-
-lemma measure_union_add_inter (s : set α) (ht : measurable_set t) :
-  μ (s ∪ t) + μ (s ∩ t) = μ s + μ t :=
-by { rw [← measure_inter_add_diff (s ∪ t) ht, set.union_inter_cancel_right,
-  union_diff_right, ← measure_inter_add_diff s ht], ac_refl }
-
-lemma measure_union_add_inter' (hs : measurable_set s) (t : set α) :
-  μ (s ∪ t) + μ (s ∩ t) = μ s + μ t :=
-by rw [union_comm, inter_comm, measure_union_add_inter t hs, add_comm]
 namespace measure
 
 /-- If `u` is a superset of `t` with the same measure (both sets possibly non-measurable), then
@@ -953,30 +922,38 @@ by rw [measure.restrict_eq_zero, h]
 
 @[simp] lemma restrict_univ : μ.restrict univ = μ := ext $ λ s hs, by simp [hs]
 
-lemma restrict_union_apply (h : disjoint (t ∩ s) (t ∩ s')) (hs : measurable_set s)
-  (hs' : measurable_set s') (ht : measurable_set t) :
-  μ.restrict (s ∪ s') t = μ.restrict s t + μ.restrict s' t :=
-begin
-  simp only [restrict_apply, ht, set.inter_union_distrib_left],
-  exact measure_union h (ht.inter hs) (ht.inter hs'),
-end
-
-lemma restrict_union (h : disjoint s t) (hs : measurable_set s) (ht : measurable_set t) :
-  μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t :=
-ext $ λ t' ht', restrict_union_apply (h.mono inf_le_right inf_le_right) hs ht ht'
-
-lemma restrict_union_add_inter (s : set α) (ht : measurable_set t) :
+lemma restrict_union_add_inter₀ (s : set α) (ht : null_measurable_set t μ) :
   μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t :=
 begin
   ext1 u hu,
   simp only [add_apply, restrict_apply hu, inter_union_distrib_left],
-  convert measure_union_add_inter (u ∩ s) (hu.inter ht) using 3,
+  convert measure_union_add_inter₀ (u ∩ s) (hu.null_measurable_set.inter ht) using 3,
   rw [set.inter_left_comm (u ∩ s), set.inter_assoc, ← set.inter_assoc u u, set.inter_self]
 end
 
+lemma restrict_union_add_inter (s : set α) (ht : measurable_set t) :
+  μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t :=
+restrict_union_add_inter₀ s ht.null_measurable_set
+
+lemma restrict_union_add_inter' (hs : measurable_set s) (t : set α) :
+  μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t :=
+by simpa only [union_comm, inter_comm, add_comm] using restrict_union_add_inter t hs
+
+lemma restrict_union₀ (h : ae_disjoint μ s t) (ht : null_measurable_set t μ) :
+  μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t :=
+by simp [← restrict_union_add_inter₀ s ht, restrict_zero_set h]
+
+lemma restrict_union (h : disjoint s t) (ht : measurable_set t) :
+  μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t :=
+restrict_union₀ h.ae_disjoint ht.null_measurable_set
+
+lemma restrict_union' (h : disjoint s t) (hs : measurable_set s) :
+  μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t :=
+by rw [union_comm, restrict_union h.symm hs, add_comm]
+
 @[simp] lemma restrict_add_restrict_compl (hs : measurable_set s) :
   μ.restrict s + μ.restrict sᶜ = μ :=
-by rw [← restrict_union (@disjoint_compl_right (set α) _ _) hs hs.compl,
+by rw [← restrict_union (@disjoint_compl_right (set α) _ _) hs.compl,
     union_compl_self, restrict_univ]
 
 @[simp] lemma restrict_compl_add_restrict (hs : measurable_set s) :
@@ -992,19 +969,19 @@ begin
 end
 
 lemma restrict_Union_apply_ae [encodable ι] {s : ι → set α}
-  (hd : pairwise (λ i j, μ (s i ∩ s j) = 0))
+  (hd : pairwise (ae_disjoint μ on s))
   (hm : ∀ i, measurable_set (s i)) {t : set α} (ht : measurable_set t) :
   μ.restrict (⋃ i, s i) t = ∑' i, μ.restrict (s i) t :=
 begin
   simp only [restrict_apply, ht, inter_Union],
-  exact measure_Union_of_null_inter (λ i, ht.inter (hm _)) (λ i j hne, measure_mono_null
-    (inter_subset_inter (inter_subset_right _ _) (inter_subset_right _ _)) (hd i j hne))
+  exact measure_Union₀ (hd.mono $ λ i j h, h.mono (inter_subset_right _ _) (inter_subset_right _ _))
+    (λ i, (ht.inter (hm i)).null_measurable_set)
 end
 
 lemma restrict_Union_apply [encodable ι] {s : ι → set α} (hd : pairwise (disjoint on s))
   (hm : ∀ i, measurable_set (s i)) {t : set α} (ht : measurable_set t) :
   μ.restrict (⋃ i, s i) t = ∑' i, μ.restrict (s i) t :=
-restrict_Union_apply_ae (λ i j hij, by simp [set.disjoint_iff_inter_eq_empty.1 (hd i j hij)]) hm ht
+restrict_Union_apply_ae (hd.mono $ λ i j h, h.ae_disjoint) hm ht
 
 lemma restrict_Union_apply_eq_supr [encodable ι] {s : ι → set α}
   (hm : ∀ i, measurable_set (s i)) (hd : directed (⊆) s) {t : set α} (ht : measurable_set t) :
diff --git a/src/measure_theory/measure/measure_space_def.lean b/src/measure_theory/measure/measure_space_def.lean
index d3af2502bb853..57b7457faf9b0 100644
--- a/src/measure_theory/measure/measure_space_def.lean
+++ b/src/measure_theory/measure/measure_space_def.lean
@@ -368,6 +368,9 @@ lemma diff_ae_eq_self : (s \ t : set α) =ᵐ[μ] s ↔ μ (s ∩ t) = 0 :=
 by simp [eventually_le_antisymm_iff, ae_le_set, diff_diff_right,
   diff_diff, diff_eq_empty.2 (set.subset_union_right _ _)]
 
+lemma diff_null_ae_eq_self (ht : μ t = 0) : (s \ t : set α) =ᵐ[μ] s :=
+diff_ae_eq_self.mpr (measure_mono_null (inter_subset_right _ _) ht)
+
 lemma ae_eq_set {s t : set α} :
   s =ᵐ[μ] t ↔ μ (s \ t) = 0 ∧ μ (t \ s) = 0 :=
 by simp [eventually_le_antisymm_iff, ae_le_set]
@@ -514,5 +517,4 @@ lemma measurable.comp_ae_measurable [measurable_space δ] {f : α → δ} {g : 
   (hg : measurable g) (hf : ae_measurable f μ) : ae_measurable (g ∘ f) μ :=
 ⟨g ∘ hf.mk f, hg.comp hf.measurable_mk, eventually_eq.fun_comp hf.ae_eq_mk _⟩
 
-
 end
diff --git a/src/measure_theory/measure/null_measurable.lean b/src/measure_theory/measure/null_measurable.lean
index 4145f604f3325..45833bfa72536 100644
--- a/src/measure_theory/measure/null_measurable.lean
+++ b/src/measure_theory/measure/null_measurable.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 -/
-import measure_theory.measure.measure_space_def
+import measure_theory.measure.ae_disjoint
 
 /-!
 # Null measurable sets and complete measures
@@ -212,6 +212,22 @@ lemma exists_measurable_subset_ae_eq (h : null_measurable_set s μ) :
 
 end null_measurable_set
 
+/-- If `sᵢ` is a countable family of (null) measurable pairwise `μ`-a.e. disjoint sets, then there
+exists a subordinate family `tᵢ ⊆ sᵢ` of measurable pairwise disjoint sets such that
+`tᵢ =ᵐ[μ] sᵢ`. -/
+lemma exists_subordinate_pairwise_disjoint [encodable ι] {s : ι → set α}
+  (h : ∀ i, null_measurable_set (s i) μ) (hd : pairwise (ae_disjoint μ on s)) :
+  ∃ t : ι → set α, (∀ i, t i ⊆ s i) ∧ (∀ i, s i =ᵐ[μ] t i) ∧ (∀ i, measurable_set (t i)) ∧
+    pairwise (disjoint on t) :=
+begin
+  choose t ht_sub htm ht_eq using λ i, (h i).exists_measurable_subset_ae_eq,
+  rcases exists_null_pairwise_disjoint_diff hd with ⟨u, hum, hu₀, hud⟩,
+  exact ⟨λ i, t i \ u i, λ i, (diff_subset _ _).trans (ht_sub _),
+    λ i, (ht_eq _).symm.trans (diff_null_ae_eq_self (hu₀ i)).symm,
+    λ i, (htm i).diff (hum i), hud.mono $
+      λ i j h, h.mono (diff_subset_diff_left (ht_sub i)) (diff_subset_diff_left (ht_sub j))⟩
+end
+
 lemma measure_Union {m0 : measurable_space α} {μ : measure α} [encodable ι] {f : ι → set α}
   (hn : pairwise (disjoint on f)) (h : ∀ i, measurable_set (f i)) :
   μ (⋃ i, f i) = ∑' i, μ (f i) :=
@@ -224,24 +240,60 @@ begin
 end
 
 lemma measure_Union₀ [encodable ι] {f : ι → set α}
-  (hn : pairwise (disjoint on f)) (h : ∀ i, null_measurable_set (f i) μ) :
+  (hd : pairwise (ae_disjoint μ on f)) (h : ∀ i, null_measurable_set (f i) μ) :
   μ (⋃ i, f i) = ∑' i, μ (f i) :=
 begin
-  refine (measure_Union_le _).antisymm _,
-  choose s hsf hsm hs_eq using λ i, (h i).exists_measurable_subset_ae_eq,
-  have hsd : pairwise (disjoint on s), from hn.mono (λ i j h, h.mono (hsf i) (hsf j)),
-  simp only [← measure_congr (hs_eq _), ← measure_Union hsd hsm],
-  exact measure_mono (Union_subset_Union hsf)
+  rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, ht_sub, ht_eq, htm, htd⟩,
+  calc μ (⋃ i, f i) = μ (⋃ i, t i) : measure_congr (eventually_eq.countable_Union ht_eq)
+  ... = ∑' i, μ (t i) : measure_Union htd htm
+  ... = ∑' i, μ (f i) : tsum_congr (λ i, measure_congr (ht_eq _).symm)
 end
 
-lemma measure_union₀ (hs : null_measurable_set s μ) (ht : null_measurable_set t μ)
-  (hd : disjoint s t) :
+lemma measure_union₀_aux (hs : null_measurable_set s μ) (ht : null_measurable_set t μ)
+  (hd : ae_disjoint μ s t) :
   μ (s ∪ t) = μ s + μ t :=
 begin
   rw [union_eq_Union, measure_Union₀, tsum_fintype, fintype.sum_bool, cond, cond],
-  exacts [pairwise_disjoint_on_bool.2 hd, λ b, bool.cases_on b ht hs]
+  exacts [(pairwise_on_bool ae_disjoint.symmetric).2 hd, λ b, bool.cases_on b ht hs]
+end
+
+/-- A null measurable set `t` is Carathéodory measurable: for any `s`, we have
+`μ (s ∩ t) + μ (s \ t) = μ s`. -/
+lemma measure_inter_add_diff₀ (s : set α) (ht : null_measurable_set t μ) :
+  μ (s ∩ t) + μ (s \ t) = μ s :=
+begin
+  refine le_antisymm _ _,
+  { rcases exists_measurable_superset μ s with ⟨s', hsub, hs'm, hs'⟩,
+    replace hs'm : null_measurable_set s' μ := hs'm.null_measurable_set,
+    calc μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) :
+      add_le_add (measure_mono $ inter_subset_inter_left _ hsub)
+        (measure_mono $ diff_subset_diff_left hsub)
+    ... = μ (s' ∩ t ∪ s' \ t) :
+      (measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) $
+        (@disjoint_inf_sdiff _ s' t _).ae_disjoint).symm
+    ... = μ s' : congr_arg μ (inter_union_diff _ _)
+    ... = μ s : hs' },
+  { calc μ s = μ (s ∩ t ∪ s \ t) : by rw inter_union_diff
+    ... ≤ μ (s ∩ t) + μ (s \ t) : measure_union_le _ _ }
 end
 
+lemma measure_union_add_inter₀ (s : set α) (ht : null_measurable_set t μ) :
+  μ (s ∪ t) + μ (s ∩ t) = μ s + μ t :=
+by rw [← measure_inter_add_diff₀ (s ∪ t) ht, union_inter_cancel_right, union_diff_right,
+  ← measure_inter_add_diff₀ s ht, add_comm, ← add_assoc, add_right_comm]
+
+lemma measure_union_add_inter₀' (hs : null_measurable_set s μ) (t : set α) :
+  μ (s ∪ t) + μ (s ∩ t) = μ s + μ t :=
+by rw [union_comm, inter_comm, measure_union_add_inter₀ t hs, add_comm]
+
+lemma measure_union₀ (ht : null_measurable_set t μ) (hd : ae_disjoint μ s t) :
+  μ (s ∪ t) = μ s + μ t :=
+by rw [← measure_union_add_inter₀ s ht, hd.eq, add_zero]
+
+lemma measure_union₀' (hs : null_measurable_set s μ) (hd : ae_disjoint μ s t) :
+  μ (s ∪ t) = μ s + μ t :=
+by rw [union_comm, measure_union₀ hs hd.symm, add_comm]
+
 section measurable_singleton_class
 
 variable [measurable_singleton_class (null_measurable_space α μ)]
@@ -362,7 +414,7 @@ namespace measure
 def completion {_ : measurable_space α} (μ : measure α) :
   @measure_theory.measure (null_measurable_space α μ) _ :=
 { to_outer_measure := μ.to_outer_measure,
-  m_Union := λ s hs hd, measure_Union₀ hd hs,
+  m_Union := λ s hs hd, measure_Union₀ (hd.mono $ λ i j h, h.ae_disjoint) hs,
   trimmed := begin
     refine le_antisymm (λ s, _) (outer_measure.le_trim _),
     rw outer_measure.trim_eq_infi, simp only [to_outer_measure_apply],
diff --git a/src/measure_theory/measure/regular.lean b/src/measure_theory/measure/regular.lean
index f0f7ce1174f47..aaf1e014018ad 100644
--- a/src/measure_theory/measure/regular.lean
+++ b/src/measure_theory/measure/regular.lean
@@ -268,14 +268,13 @@ begin
     exact ⟨U, AU, U_open, hU.le⟩ }
 end
 
-lemma _root_.measurable_set.exists_is_open_diff_lt [opens_measurable_space α]
-  [outer_regular μ] {A : set α} (hA : measurable_set A)
-  (hA' : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
+lemma _root_.measurable_set.exists_is_open_diff_lt [outer_regular μ] {A : set α}
+  (hA : measurable_set A) (hA' : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
   ∃ U ⊇ A, is_open U ∧ μ U < ∞ ∧ μ (U \ A) < ε :=
 begin
   rcases A.exists_is_open_lt_add hA' hε with ⟨U, hAU, hUo, hU⟩,
   use [U, hAU, hUo, hU.trans_le le_top],
-  exact measure_diff_lt_of_lt_add hA hUo.measurable_set hAU hA' hU,
+  exact measure_diff_lt_of_lt_add hA hAU hA' hU,
 end
 
 protected lemma map [opens_measurable_space α] [measurable_space β] [topological_space β]
@@ -343,7 +342,7 @@ variables {p q : set α → Prop} {U s : set α} {ε r : ℝ≥0∞}
 
 /-- If a measure is inner regular (using closed or compact sets), then every measurable set of
 finite measure can by approximated by a (closed or compact) subset. -/
-lemma measurable_set_of_open [opens_measurable_space α] [outer_regular μ]
+lemma measurable_set_of_open [outer_regular μ]
   (H : inner_regular μ p is_open) (h0 : p ∅) (hd : ∀ ⦃s U⦄, p s → is_open U → p (s \ U)) :
   inner_regular μ p (λ s, measurable_set s ∧ μ s ≠ ∞) :=
 begin
@@ -477,13 +476,13 @@ by simp_rw [ne.def, ← measure_univ_eq_zero, is_open_univ.measure_eq_supr_is_co
 /-- If `μ` is a regular measure, then any measurable set of finite measure can be approximated by a
 compact subset. See also `measurable_set.exists_is_compact_lt_add` and
 `measurable_set.exists_lt_is_compact_of_ne_top`. -/
-lemma inner_regular_measurable [opens_measurable_space α] [regular μ] :
+lemma inner_regular_measurable [regular μ] :
   inner_regular μ is_compact (λ s, measurable_set s ∧ μ s ≠ ∞) :=
 regular.inner_regular.measurable_set_of_open is_compact_empty (λ _ _, is_compact.diff)
 
 /-- If `μ` is a regular measure, then any measurable set of finite measure can be approximated by a
 compact subset. See also `measurable_set.exists_lt_is_compact_of_ne_top`. -/
-lemma _root_.measurable_set.exists_is_compact_lt_add [opens_measurable_space α]
+lemma _root_.measurable_set.exists_is_compact_lt_add
   [regular μ] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
   ∃ K ⊆ A, is_compact K ∧ μ A < μ K + ε :=
 regular.inner_regular_measurable.exists_subset_lt_add is_compact_empty ⟨hA, h'A⟩ h'A hε
@@ -496,22 +495,20 @@ lemma _root_.measurable_set.exists_is_compact_diff_lt [opens_measurable_space α
   ∃ K ⊆ A, is_compact K ∧ μ (A \ K) < ε :=
 begin
   rcases hA.exists_is_compact_lt_add h'A hε with ⟨K, hKA, hKc, hK⟩,
-  exact ⟨K, hKA, hKc, measure_diff_lt_of_lt_add hKc.measurable_set hA hKA
+  exact ⟨K, hKA, hKc, measure_diff_lt_of_lt_add hKc.measurable_set hKA
     (ne_top_of_le_ne_top h'A $ measure_mono hKA) hK⟩
 end
 
 /-- If `μ` is a regular measure, then any measurable set of finite measure can be approximated by a
 compact subset. See also `measurable_set.exists_is_compact_lt_add`. -/
-lemma _root_.measurable_set.exists_lt_is_compact_of_ne_top [regular μ]
-  [opens_measurable_space α] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ≠ ∞)
-  {r : ℝ≥0∞} (hr : r < μ A) :
+lemma _root_.measurable_set.exists_lt_is_compact_of_ne_top [regular μ] ⦃A : set α⦄
+  (hA : measurable_set A) (h'A : μ A ≠ ∞) {r : ℝ≥0∞} (hr : r < μ A) :
   ∃ K ⊆ A, is_compact K ∧ r < μ K :=
 regular.inner_regular_measurable ⟨hA, h'A⟩ _ hr
 
 /-- Given a regular measure, any measurable set of finite mass can be approximated from
 inside by compact sets. -/
-lemma _root_.measurable_set.measure_eq_supr_is_compact_of_ne_top
-  [opens_measurable_space α] [regular μ]
+lemma _root_.measurable_set.measure_eq_supr_is_compact_of_ne_top [regular μ]
   ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ≠ ∞) :
   μ A = (⨆ (K ⊆ A) (h : is_compact K), μ K) :=
 regular.inner_regular_measurable.measure_eq_supr ⟨hA, h'A⟩
@@ -558,16 +555,15 @@ lemma _root_.is_open.measure_eq_supr_is_closed ⦃U : set α⦄ (hU : is_open U)
   μ U = (⨆ (F ⊆ U) (h : is_closed F), μ F) :=
 weakly_regular.inner_regular.measure_eq_supr hU
 
-lemma inner_regular_measurable [opens_measurable_space α] [weakly_regular μ] :
+lemma inner_regular_measurable [weakly_regular μ] :
   inner_regular μ is_closed (λ s, measurable_set s ∧ μ s ≠ ∞) :=
 weakly_regular.inner_regular.measurable_set_of_open is_closed_empty
   (λ _ _ h₁ h₂, h₁.inter h₂.is_closed_compl)
 
 /-- If `s` is a measurable set, a weakly regular measure `μ` is finite on `s`, and `ε` is a positive
 number, then there exist a closed set `K ⊆ s` such that `μ s < μ K + ε`. -/
-lemma _root_.measurable_set.exists_is_closed_lt_add [weakly_regular μ]
-  [opens_measurable_space α] {s : set α} (hs : measurable_set s) (hμs : μ s ≠ ∞)
-  {ε : ℝ≥0∞} (hε : ε ≠ 0) :
+lemma _root_.measurable_set.exists_is_closed_lt_add [weakly_regular μ] {s : set α}
+  (hs : measurable_set s) (hμs : μ s ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
   ∃ K ⊆ s, is_closed K ∧ μ s < μ K + ε :=
 inner_regular_measurable.exists_subset_lt_add is_closed_empty ⟨hs, hμs⟩ hμs hε
 
@@ -576,22 +572,21 @@ lemma _root_.measurable_set.exists_is_closed_diff_lt [opens_measurable_space α]
   ∃ F ⊆ A, is_closed F ∧ μ (A \ F) < ε :=
 begin
   rcases hA.exists_is_closed_lt_add h'A hε with ⟨F, hFA, hFc, hF⟩,
-  exact ⟨F, hFA, hFc, measure_diff_lt_of_lt_add hFc.measurable_set hA hFA
+  exact ⟨F, hFA, hFc, measure_diff_lt_of_lt_add hFc.measurable_set hFA
     (ne_top_of_le_ne_top h'A $ measure_mono hFA) hF⟩
 end
 
 /-- Given a weakly regular measure, any measurable set of finite mass can be approximated from
 inside by closed sets. -/
 lemma _root_.measurable_set.exists_lt_is_closed_of_ne_top [weakly_regular μ]
-  [opens_measurable_space α] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ≠ ∞)
-  {r : ℝ≥0∞} (hr : r < μ A) :
+  ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ≠ ∞) {r : ℝ≥0∞} (hr : r < μ A) :
   ∃ K ⊆ A, is_closed K ∧ r < μ K :=
 inner_regular_measurable ⟨hA, h'A⟩ _ hr
 
 /-- Given a weakly regular measure, any measurable set of finite mass can be approximated from
 inside by closed sets. -/
-lemma _root_.measurable_set.measure_eq_supr_is_closed_of_ne_top [opens_measurable_space α]
-  [weakly_regular μ] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ≠ ∞) :
+lemma _root_.measurable_set.measure_eq_supr_is_closed_of_ne_top [weakly_regular μ] ⦃A : set α⦄
+  (hA : measurable_set A) (h'A : μ A ≠ ∞) :
   μ A = (⨆ (K ⊆ A) (h : is_closed K), μ K) :=
 inner_regular_measurable.measure_eq_supr ⟨hA, h'A⟩
 
diff --git a/src/measure_theory/measure/stieltjes.lean b/src/measure_theory/measure/stieltjes.lean
index 49e364e6487ac..9847059fad6fa 100644
--- a/src/measure_theory/measure/stieltjes.lean
+++ b/src/measure_theory/measure/stieltjes.lean
@@ -313,7 +313,7 @@ begin
   rcases le_or_lt a b with hab|hab,
   { have A : disjoint {a} (Ioc a b), by simp,
     simp [← Icc_union_Ioc_eq_Icc le_rfl hab, -singleton_union, ← ennreal.of_real_add, f.left_lim_le,
-      measure_union A (measurable_set_singleton a) measurable_set_Ioc, f.mono hab] },
+      measure_union A measurable_set_Ioc, f.mono hab] },
   { simp only [hab, measure_empty, Icc_eq_empty, not_le],
     symmetry,
     simp [ennreal.of_real_eq_zero, f.le_left_lim hab] }
@@ -329,7 +329,7 @@ begin
     have D : f b - f a = (f b - f.left_lim b) + (f.left_lim b - f a), by abel,
     have := f.measure_Ioc a b,
     simp only [←Ioo_union_Icc_eq_Ioc hab le_rfl, measure_singleton,
-      measure_union A measurable_set_Ioo (measurable_set_singleton b), Icc_self] at this,
+      measure_union A (measurable_set_singleton b), Icc_self] at this,
     rw [D, ennreal.of_real_add, add_comm] at this,
     { simpa only [ennreal.add_right_inj ennreal.of_real_ne_top] },
     { simp only [f.left_lim_le, sub_nonneg] },
@@ -344,7 +344,7 @@ begin
     simp [ennreal.of_real_eq_zero, f.left_lim_le_left_lim hab] },
   { have A : disjoint {a} (Ioo a b) := by simp,
     simp [← Icc_union_Ioo_eq_Ico le_rfl hab, -singleton_union, hab.ne, f.left_lim_le,
-      measure_union A (measurable_set_singleton a) measurable_set_Ioo, f.le_left_lim hab,
+      measure_union A measurable_set_Ioo, f.le_left_lim hab,
       ← ennreal.of_real_add] }
 end