diff --git a/src/measure_theory/constructions/prod.lean b/src/measure_theory/constructions/prod.lean
index b9092bd1daf90..0d51a0813cf78 100644
--- a/src/measure_theory/constructions/prod.lean
+++ b/src/measure_theory/constructions/prod.lean
@@ -207,7 +207,7 @@ begin
     suffices : measurable (λ x, c * ν (prod.mk x ⁻¹' s)),
     { simpa [lintegral_indicator _ (m hs)] },
     exact (measurable_measure_prod_mk_left hs).const_mul _ },
-  { rintro f g - hf hg h2f h2g, simp_rw [pi.add_apply, lintegral_add (hf.comp m) (hg.comp m)],
+  { rintro f g - hf hg h2f h2g, simp_rw [pi.add_apply, lintegral_add_left (hf.comp m)],
     exact h2f.add h2g },
   { intros f hf h2f h3f,
     have := measurable_supr h3f,
@@ -705,8 +705,7 @@ begin
     simp [lintegral_indicator, m hs, hs, lintegral_const_mul, measurable_measure_prod_mk_left hs,
       prod_apply] },
   { rintro f g - hf hg h2f h2g,
-    simp [lintegral_add, measurable.lintegral_prod_right', hf.comp m, hg.comp m,
-      hf, hg, h2f, h2g] },
+    simp [lintegral_add_left, measurable.lintegral_prod_right', hf.comp m, hf, h2f, h2g] },
   { intros f hf h2f h3f,
     have kf : ∀ x n, measurable (λ y, f n (x, y)) := λ x n, (hf n).comp m,
     have k2f : ∀ x, monotone (λ n y, f n (x, y)) := λ x i j hij y, h2f hij (x, y),
diff --git a/src/measure_theory/decomposition/lebesgue.lean b/src/measure_theory/decomposition/lebesgue.lean
index 2aea14562056c..fde7982e70363 100644
--- a/src/measure_theory/decomposition/lebesgue.lean
+++ b/src/measure_theory/decomposition/lebesgue.lean
@@ -294,7 +294,7 @@ begin
     ((measurable_rn_deriv μ₁ ν).add (measurable_rn_deriv μ₂ ν))
     ((have_lebesgue_decomposition_spec _ _).2.1.add_left (have_lebesgue_decomposition_spec _ _).2.1)
     _).symm,
-  erw with_density_add (measurable_rn_deriv μ₁ ν) (measurable_rn_deriv μ₂ ν),
+  erw with_density_add_left (measurable_rn_deriv μ₁ ν),
   conv_rhs { rw [add_assoc, add_comm (μ₂.singular_part ν), ← add_assoc, ← add_assoc] },
   rw [← have_lebesgue_decomposition_add μ₁ ν, add_assoc,
       add_comm (ν.with_density (μ₂.rn_deriv ν)),
@@ -627,7 +627,7 @@ theorem have_lebesgue_decomposition_of_finite_measure [is_finite_measure μ] [is
             le_sub_iff_add_le, ← ennreal.to_real_add, ennreal.to_real_le_to_real,
             measure.coe_smul, pi.smul_apply, with_density_apply _ (hA.inter hE₁),
             show ε • ν (A ∩ E) = (ε : ℝ≥0∞) * ν (A ∩ E), by refl,
-            ← set_lintegral_const, ← lintegral_add measurable_const hξm] at this,
+            ← set_lintegral_const, ← lintegral_add_left measurable_const] at this,
       { rw [ne.def, ennreal.add_eq_top, not_or_distrib],
         exact ⟨ne_of_lt (measure_lt_top _ _), ne_of_lt (measure_lt_top _ _)⟩ },
       { exact ne_of_lt (measure_lt_top _ _) },
@@ -642,18 +642,17 @@ theorem have_lebesgue_decomposition_of_finite_measure [is_finite_measure μ] [is
     { refine ⟨measurable.add hξm (measurable.indicator measurable_const hE₁), λ A hA, _⟩,
       have : ∫⁻ a in A, (ξ + E.indicator (λ _, ε)) a ∂ν =
             ∫⁻ a in A ∩ E, ε + ξ a ∂ν + ∫⁻ a in A \ E, ξ a ∂ν,
-      { simp only [lintegral_add measurable_const hξm, add_assoc, pi.add_apply, inter_comm E,
-          lintegral_inter_add_diff _ _ hE₁, lintegral_add hξm (measurable_const.indicator hE₁),
-          lintegral_indicator _ hE₁, set_lintegral_const, measure.restrict_apply hE₁],
-        exact add_comm _ _ },
+      { simp only [lintegral_add_left measurable_const, lintegral_add_left hξm,
+          set_lintegral_const, add_assoc, lintegral_inter_add_diff _ _ hE₁, pi.add_apply,
+          lintegral_indicator _ hE₁, restrict_apply hE₁],
+        rw [inter_comm, add_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 ∂ν`
       refine not_lt.2 this _,
-      rw [hξ₁, lintegral_add hξm (measurable.indicator (measurable_const) hE₁),
-          lintegral_indicator _ hE₁, set_lintegral_const],
+      rw [hξ₁, lintegral_add_left hξm, 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 ξ) univ,
       rwa [with_density_apply _ measurable_set.univ, measure.restrict_univ] at this },
diff --git a/src/measure_theory/function/ae_eq_fun.lean b/src/measure_theory/function/ae_eq_fun.lean
index 528c545b60fdf..ca4f7b3bccf45 100644
--- a/src/measure_theory/function/ae_eq_fun.lean
+++ b/src/measure_theory/function/ae_eq_fun.lean
@@ -674,7 +674,7 @@ by rw [← lintegral_mk, mk_coe_fn]
 induction_on f $ λ f hf, (lintegral_eq_zero_iff' hf.ae_measurable).trans mk_eq_mk.symm
 
 lemma lintegral_add (f g : α →ₘ[μ] ℝ≥0∞) : lintegral (f + g) = lintegral f + lintegral g :=
-induction_on₂ f g $ λ f hf g hg, by simp [lintegral_add' hf.ae_measurable hg.ae_measurable]
+induction_on₂ f g $ λ f hf g hg, by simp [lintegral_add_left' hf.ae_measurable]
 
 lemma lintegral_mono {f g : α →ₘ[μ] ℝ≥0∞} : f ≤ g → lintegral f ≤ lintegral g :=
 induction_on₂ f g $ λ f hf g hg hfg, lintegral_mono_ae hfg
diff --git a/src/measure_theory/function/ae_eq_of_integral.lean b/src/measure_theory/function/ae_eq_of_integral.lean
index 1ebaa6d706f9d..a40d35e30114b 100644
--- a/src/measure_theory/function/ae_eq_of_integral.lean
+++ b/src/measure_theory/function/ae_eq_of_integral.lean
@@ -182,7 +182,7 @@ begin
     have A : ∫⁻ x in s, g x ∂μ + ε * μ s ≤ ∫⁻ x in s, g x ∂μ + 0 := calc
       ∫⁻ x in s, g x ∂μ + ε * μ s = ∫⁻ x in s, g x ∂μ + ∫⁻ x in s, ε ∂μ :
         by simp only [lintegral_const, set.univ_inter, measurable_set.univ, measure.restrict_apply]
-      ... = ∫⁻ x in s, (g x + ε) ∂μ : (lintegral_add hg measurable_const).symm
+      ... = ∫⁻ x in s, (g x + ε) ∂μ : (lintegral_add_right _ measurable_const).symm
       ... ≤ ∫⁻ x in s, f x ∂μ : set_lintegral_mono (hg.add measurable_const) hf (λ x hx, hx.1.1)
       ... ≤ ∫⁻ x in s, g x ∂μ + 0 : by { rw [add_zero], exact h s s_meas s_lt_top },
     have B : ∫⁻ x in s, g x ∂μ ≠ ∞,
diff --git a/src/measure_theory/function/jacobian.lean b/src/measure_theory/function/jacobian.lean
index 768357ad79535..322b12560fe52 100644
--- a/src/measure_theory/function/jacobian.lean
+++ b/src/measure_theory/function/jacobian.lean
@@ -891,10 +891,7 @@ begin
       rw ← this,
     end
   ... = ∫⁻ x in s, ennreal.of_real (|(f' x).det|) ∂μ + 2 * ε * μ s :
-    begin
-      rw lintegral_add' (ae_measurable_of_real_abs_det_fderiv_within μ hs hf') ae_measurable_const,
-      simp only [lintegral_const, measurable_set.univ, measure.restrict_apply, univ_inter],
-    end
+    by simp only [lintegral_add_right' _ ae_measurable_const, set_lintegral_const]
 end
 
 lemma add_haar_image_le_lintegral_abs_det_fderiv_aux2 (hs : measurable_set s) (h's : μ s ≠ ∞)
@@ -1034,11 +1031,10 @@ begin
                       ennreal.of_real_coe_nnreal]
     end
   ... = ∑' n, (ennreal.of_real (|(A n).det|) * μ (s ∩ t n) + ε * μ (s ∩ t n)) :
-    by simp only [measurable_const, lintegral_const, lintegral_add, measurable_set.univ,
-                  eq_self_iff_true, measure.restrict_apply, univ_inter]
+    by simp only [set_lintegral_const, lintegral_add_right _ measurable_const]
   ... ≤ ∑' n, ((μ (f '' (s ∩ t n)) + ε * μ (s ∩ t n)) + ε * μ (s ∩ t n)) :
     begin
-      refine ennreal.tsum_le_tsum (λ n, add_le_add _ le_rfl),
+      refine ennreal.tsum_le_tsum (λ n, add_le_add_right _ _),
       exact (hδ (A n)).2.2 _ _ (ht n),
     end
   ... = μ (f '' s) + 2 * ε * μ s :
diff --git a/src/measure_theory/function/l1_space.lean b/src/measure_theory/function/l1_space.lean
index 6bdcf7f78f368..e77b7e39868b5 100644
--- a/src/measure_theory/function/l1_space.lean
+++ b/src/measure_theory/function/l1_space.lean
@@ -68,21 +68,25 @@ lemma lintegral_norm_eq_lintegral_edist (f : α → β) :
 by simp only [of_real_norm_eq_coe_nnnorm, edist_eq_coe_nnnorm]
 
 lemma lintegral_edist_triangle {f g h : α → β}
-  (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ)
-  (hh : ae_strongly_measurable h μ) :
+  (hf : ae_strongly_measurable f μ) (hh : ae_strongly_measurable h μ) :
   ∫⁻ a, edist (f a) (g a) ∂μ ≤ ∫⁻ a, edist (f a) (h a) ∂μ + ∫⁻ a, edist (g a) (h a) ∂μ :=
 begin
-  rw ← lintegral_add' (hf.edist hh) (hg.edist hh),
+  rw ← lintegral_add_left' (hf.edist hh),
   refine lintegral_mono (λ a, _),
   apply edist_triangle_right
 end
 
 lemma lintegral_nnnorm_zero : ∫⁻ a : α, ∥(0 : β)∥₊ ∂μ = 0 := by simp
 
-lemma lintegral_nnnorm_add
-  {f : α → β} {g : α → γ} (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) :
+lemma lintegral_nnnorm_add_left
+  {f : α → β} (hf : ae_strongly_measurable f μ) (g : α → γ) :
   ∫⁻ a, ∥f a∥₊ + ∥g a∥₊ ∂μ = ∫⁻ a, ∥f a∥₊ ∂μ + ∫⁻ a, ∥g a∥₊ ∂μ :=
-lintegral_add' hf.ennnorm hg.ennnorm
+lintegral_add_left' hf.ennnorm _
+
+lemma lintegral_nnnorm_add_right
+  (f : α → β) {g : α → γ} (hg : ae_strongly_measurable g μ) :
+  ∫⁻ a, ∥f a∥₊ + ∥g a∥₊ ∂μ = ∫⁻ a, ∥f a∥₊ ∂μ + ∫⁻ a, ∥g a∥₊ ∂μ :=
+lintegral_add_right' _ hg.ennnorm
 
 lemma lintegral_nnnorm_neg {f : α → β} :
   ∫⁻ a, ∥(-f) a∥₊ ∂μ = ∫⁻ a, ∥f a∥₊ ∂μ :=
@@ -560,9 +564,8 @@ lemma lintegral_edist_lt_top {f g : α → β}
   (hf : integrable f μ) (hg : integrable g μ) :
   ∫⁻ a, edist (f a) (g a) ∂μ < ∞ :=
 lt_of_le_of_lt
-  (lintegral_edist_triangle hf.ae_strongly_measurable hg.ae_strongly_measurable
-    (ae_strongly_measurable_const : ae_strongly_measurable (λa, (0 : β)) μ))
-  (ennreal.add_lt_top.2 $ by { simp_rw ← has_finite_integral_iff_edist,
+  (lintegral_edist_triangle hf.ae_strongly_measurable ae_strongly_measurable_zero)
+  (ennreal.add_lt_top.2 $ by { simp_rw [pi.zero_apply, ← has_finite_integral_iff_edist],
                                exact ⟨hf.has_finite_integral, hg.has_finite_integral⟩ })
 
 variables (α β μ)
@@ -570,12 +573,11 @@ variables (α β μ)
 by simp [integrable, ae_strongly_measurable_const]
 variables {α β μ}
 
-lemma integrable.add' {f g : α → β} (hf : integrable f μ)
-  (hg : integrable g μ) :
+lemma integrable.add' {f g : α → β} (hf : integrable f μ) (hg : integrable g μ) :
   has_finite_integral (f + g) μ :=
 calc ∫⁻ a, ∥f a + g a∥₊ ∂μ ≤ ∫⁻ a, ∥f a∥₊ + ∥g a∥₊ ∂μ :
   lintegral_mono (λ a, by exact_mod_cast nnnorm_add_le _ _)
-... = _ : lintegral_nnnorm_add hf.ae_strongly_measurable hg.ae_strongly_measurable
+... = _ : lintegral_nnnorm_add_left hf.ae_strongly_measurable _
 ... < ∞ : add_lt_top.2 ⟨hf.has_finite_integral, hg.has_finite_integral⟩
 
 lemma integrable.add
diff --git a/src/measure_theory/function/lp_space.lean b/src/measure_theory/function/lp_space.lean
index 353a865f65161..a7a904cf1d668 100644
--- a/src/measure_theory/function/lp_space.lean
+++ b/src/measure_theory/function/lp_space.lean
@@ -746,7 +746,7 @@ lemma snorm_add_lt_top_of_one_le {f g : α → E} (hf : mem_ℒp f p μ) (hg : m
 lt_of_le_of_lt (snorm_add_le hf.1 hg.1 hq1) (ennreal.add_lt_top.mpr ⟨hf.2, hg.2⟩)
 
 lemma snorm'_add_lt_top_of_le_one
-  {f g : α → E} (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ)
+  {f g : α → E} (hf : ae_strongly_measurable f μ)
   (hf_snorm : snorm' f q μ < ∞) (hg_snorm : snorm' g q μ < ∞) (hq_pos : 0 < q) (hq1 : q ≤ 1) :
   snorm' (f + g) q μ < ∞ :=
 calc (∫⁻ a, ↑∥(f + g) a∥₊ ^ q ∂μ) ^ (1 / q)
@@ -765,11 +765,9 @@ end
 ... < ∞ :
 begin
   refine ennreal.rpow_lt_top_of_nonneg (by simp [hq_pos.le] : 0 ≤ 1 / q) _,
-  rw [lintegral_add' (hf.ennnorm.pow_const q)
-    (hg.ennnorm.pow_const q), ennreal.add_ne_top, ←lt_top_iff_ne_top,
-    ←lt_top_iff_ne_top],
-  exact ⟨lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top hq_pos hf_snorm,
-    lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top hq_pos hg_snorm⟩,
+  rw [lintegral_add_left' (hf.ennnorm.pow_const q), ennreal.add_ne_top],
+  exact ⟨(lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top hq_pos hf_snorm).ne,
+    (lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top hq_pos hg_snorm).ne⟩,
 end
 
 lemma snorm_add_lt_top {f g : α → E} (hf : mem_ℒp f p μ) (hg : mem_ℒp g p μ) :
@@ -788,7 +786,7 @@ begin
   { rwa [← ennreal.one_to_real, @ennreal.to_real_le_to_real p 1 hp_top ennreal.coe_ne_top], },
   rw snorm_eq_snorm' h0 hp_top,
   rw [mem_ℒp, snorm_eq_snorm' h0 hp_top] at hf hg,
-  exact snorm'_add_lt_top_of_le_one hf.1 hg.1 hf.2 hg.2 hp_pos hp1_real,
+  exact snorm'_add_lt_top_of_le_one hf.1 hf.2 hg.2 hp_pos hp1_real,
 end
 
 section map_measure
diff --git a/src/measure_theory/integral/lebesgue.lean b/src/measure_theory/integral/lebesgue.lean
index a882e24bf3c8a..772d72b9ca0a9 100644
--- a/src/measure_theory/integral/lebesgue.lean
+++ b/src/measure_theory/integral/lebesgue.lean
@@ -1040,6 +1040,10 @@ lintegral_mono
 @[simp] lemma lintegral_const (c : ℝ≥0∞) : ∫⁻ a, c ∂μ = c * μ univ :=
 by rw [← simple_func.const_lintegral, ← simple_func.lintegral_eq_lintegral, simple_func.coe_const]
 
+lemma lintegral_zero : ∫⁻ a:α, 0 ∂μ = 0 := by simp
+
+lemma lintegral_zero_fun : lintegral μ (0 : α → ℝ≥0∞) = 0 := lintegral_zero
+
 @[simp] lemma lintegral_one : ∫⁻ a, (1 : ℝ≥0∞) ∂μ = μ univ :=
 by rw [lintegral_const, one_mul]
 
@@ -1049,6 +1053,31 @@ by rw [lintegral_const, measure.restrict_apply_univ]
 lemma set_lintegral_one (s) : ∫⁻ a in s, 1 ∂μ = μ s :=
 by rw [set_lintegral_const, one_mul]
 
+section
+
+variable (μ)
+
+/-- For any function `f : α → ℝ≥0∞`, there exists a measurable function `g ≤ f` with the same
+integral. -/
+lemma exists_measurable_le_lintegral_eq (f : α → ℝ≥0∞) :
+  ∃ g : α → ℝ≥0∞, measurable g ∧ g ≤ f ∧ ∫⁻ a, f a ∂μ = ∫⁻ a, g a ∂μ :=
+begin
+  cases eq_or_ne (∫⁻ a, f a ∂μ) 0 with h₀ h₀,
+  { exact ⟨0, measurable_zero, zero_le f, h₀.trans lintegral_zero.symm⟩ },
+  rcases exists_seq_strict_mono_tendsto' h₀.bot_lt with ⟨L, hL_mono, hLf, hL_tendsto⟩,
+  have : ∀ n, ∃ g : α → ℝ≥0∞, measurable g ∧ g ≤ f ∧ L n < ∫⁻ a, g a ∂μ,
+  { intro n,
+    simpa only [← supr_lintegral_measurable_le_eq_lintegral f, lt_supr_iff, exists_prop]
+      using (hLf n).2 },
+  choose g hgm hgf hLg,
+  refine ⟨λ x, ⨆ n, g n x, measurable_supr hgm, λ x, supr_le (λ n, hgf n x), le_antisymm _ _⟩,
+  { refine le_of_tendsto' hL_tendsto (λ n, (hLg n).le.trans $ lintegral_mono $ λ x, _),
+    exact le_supr (λ n, g n x) n },
+  { exact lintegral_mono (λ x, supr_le $ λ n, hgf n x) }
+end
+
+end
+
 /-- `∫⁻ a in s, f a ∂μ` is defined as the supremum of integrals of simple functions
 `φ : α →ₛ ℝ≥0∞` such that `φ ≤ f`. This lemma says that it suffices to take
 functions `φ : α →ₛ ℝ≥0`. -/
@@ -1335,8 +1364,18 @@ begin
   exact (hl δ δ0).mono (λ i, hδ _)
 end
 
-@[simp] lemma lintegral_add {f g : α → ℝ≥0∞} (hf : measurable f) (hg : measurable g) :
-  (∫⁻ a, f a + g a ∂μ) = (∫⁻ a, f a ∂μ) + (∫⁻ a, g a ∂μ) :=
+/-- The sum of the lower Lebesgue integrals of two functions is less than or equal to the integral
+of their sum. The other inequality needs one of these functions to be (a.e.-)measurable. -/
+lemma le_lintegral_add (f g : α → ℝ≥0∞) : ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ ≤ ∫⁻ a, f a + g a ∂μ :=
+begin
+  dunfold lintegral,
+  refine ennreal.bsupr_add_bsupr_le' ⟨0, zero_le f⟩  ⟨0, zero_le g⟩ (λ f' hf' g' hg', _),
+  exact le_supr₂_of_le (f' + g') (add_le_add hf' hg') (add_lintegral _ _).ge
+end
+
+-- Use stronger lemmas `lintegral_add_left`/`lintegral_add_right` instead
+lemma lintegral_add_aux {f g : α → ℝ≥0∞} (hf : measurable f) (hg : measurable g) :
+  ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ :=
 calc (∫⁻ a, f a + g a ∂μ) =
     (∫⁻ a, (⨆n, (eapprox f n : α → ℝ≥0∞) a) + (⨆n, (eapprox g n : α → ℝ≥0∞) a) ∂μ) :
     by simp only [supr_eapprox_apply, hf, hg]
@@ -1362,20 +1401,36 @@ calc (∫⁻ a, f a + g a ∂μ) =
   ... = (∫⁻ a, f a ∂μ) + (∫⁻ a, g a ∂μ) :
     by rw [lintegral_eq_supr_eapprox_lintegral hf, lintegral_eq_supr_eapprox_lintegral hg]
 
-lemma lintegral_add' {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
-  (∫⁻ a, f a + g a ∂μ) = (∫⁻ a, f a ∂μ) + (∫⁻ a, g a ∂μ) :=
-calc (∫⁻ a, f a + g a ∂μ) = (∫⁻ a, hf.mk f a + hg.mk g a ∂μ) :
-  lintegral_congr_ae (eventually_eq.add hf.ae_eq_mk hg.ae_eq_mk)
-... = (∫⁻ a, hf.mk f a ∂μ) + (∫⁻ a, hg.mk g a ∂μ) : lintegral_add hf.measurable_mk hg.measurable_mk
-... = (∫⁻ a, f a ∂μ) + (∫⁻ a, g a ∂μ) : begin
-  congr' 1,
-  { exact lintegral_congr_ae hf.ae_eq_mk.symm },
-  { exact lintegral_congr_ae hg.ae_eq_mk.symm },
-end
-
-lemma lintegral_zero : (∫⁻ a:α, 0 ∂μ) = 0 := by simp
-
-lemma lintegral_zero_fun : (∫⁻ a:α, (0 : α → ℝ≥0∞) a ∂μ) = 0 := by simp
+/-- If `f g : α → ℝ≥0∞` are two functions and one of them is (a.e.) measurable, then the Lebesgue
+integral of `f + g` equals the sum of integrals. This lemma assumes that `f` is integrable, see also
+`measure_theory.lintegral_add_right` and primed versions of these lemmas. -/
+@[simp] lemma lintegral_add_left {f : α → ℝ≥0∞} (hf : measurable f) (g : α → ℝ≥0∞) :
+  ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ :=
+begin
+  refine le_antisymm _ (le_lintegral_add _ _),
+  rcases exists_measurable_le_lintegral_eq μ (λ a, f a + g a) with ⟨φ, hφm, hφ_le, hφ_eq⟩,
+  calc ∫⁻ a, f a + g a ∂μ = ∫⁻ a, φ a ∂μ : hφ_eq
+  ... ≤ ∫⁻ a, f a + (φ a - f a) ∂μ        : lintegral_mono (λ a, le_add_tsub)
+  ... = ∫⁻ a, f a ∂μ + ∫⁻ a, φ a - f a ∂μ : lintegral_add_aux hf (hφm.sub hf)
+  ... ≤ ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ       :
+    add_le_add_left (lintegral_mono $ λ a, tsub_le_iff_left.2 $ hφ_le a) _
+end
+
+lemma lintegral_add_left' {f : α → ℝ≥0∞} (hf : ae_measurable f μ) (g : α → ℝ≥0∞) :
+  ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ :=
+by rw [lintegral_congr_ae hf.ae_eq_mk, ← lintegral_add_left hf.measurable_mk,
+  lintegral_congr_ae (hf.ae_eq_mk.add (ae_eq_refl g))]
+
+lemma lintegral_add_right' (f : α → ℝ≥0∞) {g : α → ℝ≥0∞} (hg : ae_measurable g μ) :
+  ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ :=
+by simpa only [add_comm] using lintegral_add_left' hg f
+
+/-- If `f g : α → ℝ≥0∞` are two functions and one of them is (a.e.) measurable, then the Lebesgue
+integral of `f + g` equals the sum of integrals. This lemma assumes that `g` is integrable, see also
+`measure_theory.lintegral_add_left` and primed versions of these lemmas. -/
+@[simp] lemma lintegral_add_right (f : α → ℝ≥0∞) {g : α → ℝ≥0∞} (hg : measurable g) :
+  ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ :=
+lintegral_add_right' f hg.ae_measurable
 
 @[simp] lemma lintegral_smul_measure (c : ℝ≥0∞) (f : α → ℝ≥0∞) :
   ∫⁻ a, f a ∂ (c • μ) = c * ∫⁻ a, f a ∂μ :=
@@ -1427,16 +1482,21 @@ begin
   exact measure.restrict_eq_zero.2 hs',
 end
 
-lemma lintegral_finset_sum (s : finset β) {f : β → α → ℝ≥0∞} (hf : ∀ b ∈ s, measurable (f b)) :
+lemma lintegral_finset_sum' (s : finset β) {f : β → α → ℝ≥0∞}
+  (hf : ∀ b ∈ s, ae_measurable (f b) μ) :
   (∫⁻ a, ∑ b in s, f b a ∂μ) = ∑ b in s, ∫⁻ a, f b a ∂μ :=
 begin
   induction s using finset.induction_on with a s has ih,
   { simp },
   { simp only [finset.sum_insert has],
     rw [finset.forall_mem_insert] at hf,
-    rw [lintegral_add hf.1 (s.measurable_sum hf.2), ih hf.2] }
+    rw [lintegral_add_left' hf.1, ih hf.2] }
 end
 
+lemma lintegral_finset_sum (s : finset β) {f : β → α → ℝ≥0∞} (hf : ∀ b ∈ s, measurable (f b)) :
+  (∫⁻ a, ∑ b in s, f b a ∂μ) = ∑ b in s, ∫⁻ a, f b a ∂μ :=
+lintegral_finset_sum' s (λ b hb, (hf b hb).ae_measurable)
+
 @[simp] lemma lintegral_const_mul (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : measurable f) :
   (∫⁻ a, r * f a ∂μ) = r * (∫⁻ a, f a ∂μ) :=
 calc (∫⁻ a, r * f a ∂μ) = (∫⁻ a, (⨆n, (const α r * eapprox f n) a) ∂μ) :
@@ -1466,7 +1526,7 @@ begin
   rw [lintegral, ennreal.mul_supr],
   refine supr_le (λs, _),
   rw [ennreal.mul_supr],
-  simp only [supr_le_iff, ge_iff_le],
+  simp only [supr_le_iff],
   assume hs,
   rw [← simple_func.const_mul_lintegral, lintegral],
   refine le_supr_of_le (const α r * s) (le_supr_of_le (λx, _) le_rfl),
@@ -1536,6 +1596,12 @@ begin
     simp [hφ x, hs, indicator_le_indicator] }
 end
 
+lemma lintegral_indicator₀ (f : α → ℝ≥0∞) {s : set α} (hs : null_measurable_set s μ) :
+  ∫⁻ a, s.indicator f a ∂μ = ∫⁻ a in s, f a ∂μ :=
+by rw [← lintegral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.to_measurable_ae_eq),
+  lintegral_indicator _ (measurable_set_to_measurable _ _),
+  measure.restrict_congr_set hs.to_measurable_ae_eq]
+
 lemma set_lintegral_eq_const {f : α → ℝ≥0∞} (hf : measurable f) (r : ℝ≥0∞) :
   ∫⁻ x in {x | f x = r}, f x ∂μ = r * μ {x | f x = r} :=
 begin
@@ -1546,31 +1612,39 @@ begin
   exact hf (measurable_set_singleton r)
 end
 
-/-- **Markov's inequality** also known as **Chebyshev's first inequality**. For a version assuming
-`ae_measurable`, see `mul_meas_ge_le_lintegral₀`. -/
-lemma mul_meas_ge_le_lintegral {f : α → ℝ≥0∞} (hf : measurable f) (ε : ℝ≥0∞) :
-  ε * μ {x | ε ≤ f x} ≤ ∫⁻ a, f a ∂μ :=
+/-- A version of **Markov's inequality** for two functions. It doesn't follow from the standard
+Markov's inequality because we only assume measurability of `g`, not `f`. -/
+lemma lintegral_add_mul_meas_add_le_le_lintegral {f g : α → ℝ≥0∞} (hle : f ≤ᵐ[μ] g)
+  (hg : ae_measurable g μ) (ε : ℝ≥0∞) :
+  ∫⁻ a, f a ∂μ + ε * μ {x | f x + ε ≤ g x} ≤ ∫⁻ a, g a ∂μ :=
 begin
-  have : measurable_set {a : α | ε ≤ f a }, from hf measurable_set_Ici,
-  rw [← simple_func.restrict_const_lintegral _ this, ← simple_func.lintegral_eq_lintegral],
-  refine lintegral_mono (λ a, _),
-  simp only [restrict_apply _ this],
-  exact indicator_apply_le id
+  rcases exists_measurable_le_lintegral_eq μ f with ⟨φ, hφm, hφ_le, hφ_eq⟩,
+  calc ∫⁻ x, f x ∂μ + ε * μ {x | f x + ε ≤ g x} = ∫⁻ x, φ x ∂μ + ε * μ {x | f x + ε ≤ g x} :
+    by rw [hφ_eq]
+  ... ≤ ∫⁻ x, φ x ∂μ + ε * μ {x | φ x + ε ≤ g x} :
+    add_le_add_left (mul_le_mul_left'
+      (measure_mono $ λ x, (add_le_add_right (hφ_le _) _).trans) _) _
+  ... = ∫⁻ x, φ x + indicator {x | φ x + ε ≤ g x} (λ _, ε) x ∂μ :
+    begin
+      rw [lintegral_add_left hφm, lintegral_indicator₀, set_lintegral_const],
+      exact measurable_set_le (hφm.null_measurable.measurable'.add_const _) hg.null_measurable
+    end
+  ... ≤ ∫⁻ x, g x ∂μ : lintegral_mono_ae (hle.mono $ λ x hx₁, _),
+  simp only [indicator_apply], split_ifs with hx₂,
+  exacts [hx₂, (add_zero _).trans_le $ (hφ_le x).trans hx₁]
 end
 
 /-- **Markov's inequality** also known as **Chebyshev's first inequality**. -/
 lemma mul_meas_ge_le_lintegral₀ {f : α → ℝ≥0∞} (hf : ae_measurable f μ) (ε : ℝ≥0∞) :
   ε * μ {x | ε ≤ f x} ≤ ∫⁻ a, f a ∂μ :=
-begin
-  have A : μ {x | ε ≤ f x} = μ {x | ε ≤ hf.mk f x},
-  { apply eventually_eq.measure_eq,
-    filter_upwards [hf.ae_eq_mk] with x hx,
-    change (ε ≤ f x) = (ε ≤ hf.mk f x),
-    simp [hx] },
-  have B : ∫⁻ a, f a ∂μ = ∫⁻ a, hf.mk f a ∂μ := lintegral_congr_ae hf.ae_eq_mk,
-  rw [A, B],
-  exact mul_meas_ge_le_lintegral hf.measurable_mk ε,
-end
+by simpa only [lintegral_zero, zero_add]
+  using lintegral_add_mul_meas_add_le_le_lintegral (ae_of_all _ $ λ x, zero_le (f x)) hf ε
+
+/-- **Markov's inequality** also known as **Chebyshev's first inequality**. For a version assuming
+`ae_measurable`, see `mul_meas_ge_le_lintegral₀`. -/
+lemma mul_meas_ge_le_lintegral {f : α → ℝ≥0∞} (hf : measurable f) (ε : ℝ≥0∞) :
+  ε * μ {x | ε ≤ f x} ≤ ∫⁻ a, f a ∂μ :=
+mul_meas_ge_le_lintegral₀ hf.ae_measurable ε
 
 lemma lintegral_eq_top_of_measure_eq_top_pos {f : α → ℝ≥0∞} (hf : ae_measurable f μ)
   (hμf : 0 < μ {x | f x = ∞}) : ∫⁻ x, f x ∂μ = ∞ :=
@@ -1585,34 +1659,33 @@ lemma meas_ge_le_lintegral_div {f : α → ℝ≥0∞} (hf : ae_measurable f μ)
 (ennreal.le_div_iff_mul_le (or.inl hε) (or.inl hε')).2 $
 by { rw [mul_comm], exact mul_meas_ge_le_lintegral₀ hf ε }
 
-@[simp] lemma lintegral_eq_zero_iff {f : α → ℝ≥0∞} (hf : measurable f) :
-  ∫⁻ a, f a ∂μ = 0 ↔ (f =ᵐ[μ] 0) :=
-begin
-  refine iff.intro (assume h, _) (assume h, _),
-  { have : ∀n:ℕ, ∀ᵐ a ∂μ, f a < n⁻¹,
-    { assume n,
-      rw [ae_iff, ← nonpos_iff_eq_zero, ← @ennreal.zero_div n⁻¹,
-        ennreal.le_div_iff_mul_le, mul_comm],
-      simp only [not_lt],
-      -- TODO: why `rw ← h` fails with "not an equality or an iff"?
-      exacts [h ▸ mul_meas_ge_le_lintegral hf n⁻¹,
-        or.inl (ennreal.inv_ne_zero.2 ennreal.coe_nat_ne_top),
-        or.inr ennreal.zero_ne_top] },
-    refine (ae_all_iff.2 this).mono (λ a ha, _),
-    by_contradiction h,
-    rcases ennreal.exists_inv_nat_lt h with ⟨n, hn⟩,
-    exact (lt_irrefl _ $ lt_trans hn $ ha n).elim },
-  { calc ∫⁻ a, f a ∂μ = ∫⁻ a, 0 ∂μ : lintegral_congr_ae h
-      ... = 0 : lintegral_zero }
+lemma ae_eq_of_ae_le_of_lintegral_le {f g : α → ℝ≥0∞} (hfg : f ≤ᵐ[μ] g)
+  (hf : ∫⁻ x, f x ∂μ ≠ ∞) (hg : ae_measurable g μ) (hgf : ∫⁻ x, g x ∂μ ≤ ∫⁻ x, f x ∂μ) :
+  f =ᵐ[μ] g :=
+begin
+  have : ∀ n : ℕ, ∀ᵐ x ∂μ, g x < f x + n⁻¹,
+  { intro n,
+    simp only [ae_iff, not_lt],
+    have : ∫⁻ x, f x ∂μ + (↑n)⁻¹ * μ {x : α | f x + n⁻¹ ≤ g x} ≤ ∫⁻ x, f x ∂μ,
+      from (lintegral_add_mul_meas_add_le_le_lintegral hfg hg n⁻¹).trans hgf,
+    rw [(ennreal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this,
+    exact this.resolve_left (ennreal.inv_ne_zero.2 ennreal.coe_nat_ne_top) },
+  refine hfg.mp ((ae_all_iff.2 this).mono (λ x hlt hle, hle.antisymm _)),
+  suffices : tendsto (λ n : ℕ, f x + n⁻¹) at_top (𝓝 (f x)),
+    from ge_of_tendsto' this (λ i, (hlt i).le),
+  simpa only [inv_top, add_zero]
+    using tendsto_const_nhds.add (ennreal.tendsto_inv_iff.2 ennreal.tendsto_nat_nhds_top)
 end
 
 @[simp] lemma lintegral_eq_zero_iff' {f : α → ℝ≥0∞} (hf : ae_measurable f μ) :
-  ∫⁻ a, f a ∂μ = 0 ↔ (f =ᵐ[μ] 0) :=
-begin
-  have : ∫⁻ a, f a ∂μ = ∫⁻ a, hf.mk f a ∂μ := lintegral_congr_ae hf.ae_eq_mk,
-  rw [this, lintegral_eq_zero_iff hf.measurable_mk],
-  exact ⟨λ H, hf.ae_eq_mk.trans H, λ H, hf.ae_eq_mk.symm.trans H⟩
-end
+  ∫⁻ a, f a ∂μ = 0 ↔ f =ᵐ[μ] 0 :=
+have ∫⁻ a : α, 0 ∂μ ≠ ∞, by simpa only [lintegral_zero] using zero_ne_top,
+⟨λ h, (ae_eq_of_ae_le_of_lintegral_le (ae_of_all _ $ zero_le f) this hf
+  (h.trans lintegral_zero.symm).le).symm, λ h, (lintegral_congr_ae h).trans lintegral_zero⟩
+
+@[simp] lemma lintegral_eq_zero_iff {f : α → ℝ≥0∞} (hf : measurable f) :
+  ∫⁻ a, f a ∂μ = 0 ↔ f =ᵐ[μ] 0 :=
+lintegral_eq_zero_iff' hf.ae_measurable
 
 lemma lintegral_pos_iff_support {f : α → ℝ≥0∞} (hf : measurable f) :
   0 < ∫⁻ a, f a ∂μ ↔ 0 < μ (function.support f) :=
@@ -1643,62 +1716,56 @@ calc
   ... = ⨆n, (∫⁻ a, f n a ∂μ) :
     by simp only [lintegral_congr_ae (g_eq_f.mono $ λ a ha, ha _)]
 
-lemma lintegral_sub {f g : α → ℝ≥0∞} (hf : measurable f) (hg : measurable g)
+lemma lintegral_sub {f g : α → ℝ≥0∞} (hg : measurable g)
   (hg_fin : ∫⁻ a, g a ∂μ ≠ ∞) (h_le : g ≤ᵐ[μ] f) :
   ∫⁻ a, f a - g a ∂μ = ∫⁻ a, f a ∂μ - ∫⁻ a, g a ∂μ :=
 begin
-  rw [← ennreal.add_left_inj hg_fin,
-        tsub_add_cancel_of_le (lintegral_mono_ae h_le),
-      ← lintegral_add (hf.sub hg) hg],
-  refine lintegral_congr_ae (h_le.mono $ λ x hx, _),
-  exact tsub_add_cancel_of_le hx
+  refine ennreal.eq_sub_of_add_eq hg_fin _,
+  rw [← lintegral_add_right _ hg],
+  exact lintegral_congr_ae (h_le.mono $ λ x hx, tsub_add_cancel_of_le hx)
 end
 
-lemma lintegral_sub_le (f g : α → ℝ≥0∞)
-  (hf : measurable f) (hg : measurable g) (h : f ≤ᵐ[μ] g) :
+lemma lintegral_sub_le (f g : α → ℝ≥0∞) (hf : measurable f) :
   ∫⁻ x, g x ∂μ - ∫⁻ x, f x ∂μ ≤ ∫⁻ x, g x - f x ∂μ :=
 begin
+  rw tsub_le_iff_right,
   by_cases hfi : ∫⁻ x, f x ∂μ = ∞,
-  { rw [hfi, ennreal.sub_top],
-    exact bot_le },
-  { rw lintegral_sub hg hf hfi h,
-    refl' }
+  { rw [hfi, ennreal.add_top],
+    exact le_top },
+  { rw [← lintegral_add_right _ hf],
+    exact lintegral_mono (λ x, le_tsub_add) }
 end
 
-lemma lintegral_strict_mono_of_ae_le_of_ae_lt_on {f g : α → ℝ≥0∞}
-  (hf : measurable f) (hg : measurable g) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (h_le : f ≤ᵐ[μ] g)
-  {s : set α} (hμs : μ s ≠ 0) (h : ∀ᵐ x ∂μ, x ∈ s → f x < g x) :
+lemma lintegral_strict_mono_of_ae_le_of_frequently_ae_lt {f g : α → ℝ≥0∞} (hg : ae_measurable g μ)
+  (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (h_le : f ≤ᵐ[μ] g) (h : ∃ᵐ x ∂μ, f x ≠ g x) :
   ∫⁻ x, f x ∂μ < ∫⁻ x, g x ∂μ :=
 begin
-  rw [← tsub_pos_iff_lt, ← lintegral_sub hg hf hfi h_le],
-  by_contra hnlt,
-  rw [not_lt, nonpos_iff_eq_zero, lintegral_eq_zero_iff (hg.sub hf), filter.eventually_eq] at hnlt,
-  simp only [ae_iff, tsub_eq_zero_iff_le, pi.zero_apply, not_lt, not_le] at hnlt h,
-  refine hμs _,
-  push_neg at h,
-  have hs_eq : s = {a : α | a ∈ s ∧ g a ≤ f a} ∪ {a : α | a ∈ s ∧ f a < g a},
-  { ext1 x,
-    simp_rw [set.mem_union, set.mem_set_of_eq, ← not_le],
-    tauto, },
-  rw hs_eq,
-  refine measure_union_null h (measure_mono_null _ hnlt),
-  simp,
+  contrapose! h,
+  simp only [not_frequently, ne.def, not_not],
+  exact ae_eq_of_ae_le_of_lintegral_le h_le hfi hg h
 end
 
+lemma lintegral_strict_mono_of_ae_le_of_ae_lt_on {f g : α → ℝ≥0∞}
+  (hg : ae_measurable g μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (h_le : f ≤ᵐ[μ] g)
+  {s : set α} (hμs : μ s ≠ 0) (h : ∀ᵐ x ∂μ, x ∈ s → f x < g x) :
+  ∫⁻ x, f x ∂μ < ∫⁻ x, g x ∂μ :=
+lintegral_strict_mono_of_ae_le_of_frequently_ae_lt hg hfi h_le $
+  ((frequently_ae_mem_iff.2 hμs).and_eventually h).mono $ λ x hx, (hx.2 hx.1).ne
+
 lemma lintegral_strict_mono {f g : α → ℝ≥0∞} (hμ : μ ≠ 0)
-  (hf : measurable f) (hg : measurable g) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (h : ∀ᵐ x ∂μ, f x < g x) :
+  (hg : ae_measurable g μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (h : ∀ᵐ x ∂μ, f x < g x) :
   ∫⁻ x, f x ∂μ < ∫⁻ x, g x ∂μ :=
 begin
   rw [ne.def, ← measure.measure_univ_eq_zero] at hμ,
-  refine lintegral_strict_mono_of_ae_le_of_ae_lt_on hf hg hfi (ae_le_of_ae_lt h) hμ _,
+  refine lintegral_strict_mono_of_ae_le_of_ae_lt_on hg hfi (ae_le_of_ae_lt h) hμ _,
   simpa using h,
 end
 
 lemma set_lintegral_strict_mono {f g : α → ℝ≥0∞} {s : set α}
-  (hsm : measurable_set s) (hs : μ s ≠ 0) (hf : measurable f) (hg : measurable g)
+  (hsm : measurable_set s) (hs : μ s ≠ 0) (hg : measurable g)
   (hfi : ∫⁻ x in s, f x ∂μ ≠ ∞) (h : ∀ᵐ x ∂μ, x ∈ s → f x < g x) :
   ∫⁻ x in s, f x ∂μ < ∫⁻ x in s, g x ∂μ :=
-lintegral_strict_mono (by simp [hs]) hf hg hfi ((ae_restrict_iff' hsm).mpr h)
+lintegral_strict_mono (by simp [hs]) hg.ae_measurable hfi ((ae_restrict_iff' hsm).mpr h)
 
 /-- Monotone convergence theorem for nonincreasing sequences of functions -/
 lemma lintegral_infi_ae
@@ -1712,7 +1779,7 @@ have fn_le_f0' : (⨅n, ∫⁻ a, f n a ∂μ) ≤ ∫⁻ a, f 0 a ∂μ, from i
 show ∫⁻ a, f 0 a ∂μ - ∫⁻ a, ⨅n, f n a ∂μ = ∫⁻ a, f 0 a ∂μ - (⨅n, ∫⁻ a, f n a ∂μ), from
 calc
   ∫⁻ a, f 0 a ∂μ - (∫⁻ a, ⨅n, f n a ∂μ) = ∫⁻ a, f 0 a - ⨅n, f n a ∂μ:
-    (lintegral_sub (h_meas 0) (measurable_infi h_meas)
+    (lintegral_sub (measurable_infi h_meas)
     (ne_top_of_le_ne_top h_fin $ lintegral_mono (assume a, infi_le _ _))
     (ae_of_all _ $ assume a, infi_le _ _)).symm
   ... = ∫⁻ a, ⨆n, f 0 a - f n a ∂μ : congr rfl (funext (assume a, ennreal.sub_infi))
@@ -1727,7 +1794,7 @@ calc
       induction n with n ih,
       {exact le_rfl}, {exact le_trans (h n) ih}
     end,
-    congr_arg supr $ funext $ assume n, lintegral_sub (h_meas _) (h_meas _)
+    congr_arg supr $ funext $ assume n, lintegral_sub (h_meas _)
       (ne_top_of_le_ne_top h_fin $ lintegral_mono_ae $ h_mono n) (h_mono n)
   ... = ∫⁻ a, f 0 a ∂μ - ⨅n, ∫⁻ a, f n a ∂μ : ennreal.sub_infi.symm
 
@@ -2154,15 +2221,19 @@ begin
   exact lintegral_congr_ae (ae_restrict_of_ae h)
 end
 
-lemma with_density_add {f g : α → ℝ≥0∞} (hf : measurable f) (hg : measurable g) :
+lemma with_density_add_left {f : α → ℝ≥0∞} (hf : measurable f) (g : α → ℝ≥0∞) :
   μ.with_density (f + g) = μ.with_density f + μ.with_density g :=
 begin
   refine measure.ext (λ s hs, _),
   rw [with_density_apply _ hs, measure.add_apply,
-      with_density_apply _ hs, with_density_apply _ hs, ← lintegral_add hf hg],
+      with_density_apply _ hs, with_density_apply _ hs, ← lintegral_add_left hf],
   refl,
 end
 
+lemma with_density_add_right (f : α → ℝ≥0∞) {g : α → ℝ≥0∞} (hg : measurable g) :
+  μ.with_density (f + g) = μ.with_density f + μ.with_density g :=
+by simpa only [add_comm] using with_density_add_left hg f
+
 lemma with_density_smul (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : measurable f) :
   μ.with_density (r • f) = r • μ.with_density f :=
 begin
@@ -2588,8 +2659,8 @@ begin
     suffices h_trim_s : μ.trim hm s = μ s, by rw h_trim_s,
     exact trim_measurable_set_eq hm hs, },
   { intros f g hfg hf hg hf_prop hg_prop,
-    have h_m := lintegral_add hf hg,
-    have h_m0 := lintegral_add (measurable.mono hf hm le_rfl) (measurable.mono hg hm le_rfl),
+    have h_m := lintegral_add_left hf g,
+    have h_m0 := lintegral_add_left (measurable.mono hf hm le_rfl) g,
     rwa [hf_prop, hg_prop, ← h_m0] at h_m, },
   { intros f hf hf_mono hf_prop,
     rw lintegral_supr hf hf_mono,
diff --git a/src/measure_theory/integral/mean_inequalities.lean b/src/measure_theory/integral/mean_inequalities.lean
index 9363fa2c1fb80..ea58ec559bf9c 100644
--- a/src/measure_theory/integral/mean_inequalities.lean
+++ b/src/measure_theory/integral/mean_inequalities.lean
@@ -49,8 +49,8 @@ variables {α : Type*} [measurable_space α] {μ : measure α}
 namespace ennreal
 
 lemma lintegral_mul_le_one_of_lintegral_rpow_eq_one {p q : ℝ} (hpq : p.is_conjugate_exponent q)
-  {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hg : ae_measurable g μ)
-  (hf_norm : ∫⁻ a, (f a)^p ∂μ = 1) (hg_norm : ∫⁻ a, (g a)^q ∂μ = 1) :
+  {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hf_norm : ∫⁻ a, (f a)^p ∂μ = 1)
+  (hg_norm : ∫⁻ a, (g a)^q ∂μ = 1) :
   ∫⁻ a, (f * g) a ∂μ ≤ 1 :=
 begin
   calc ∫⁻ (a : α), ((f * g) a) ∂μ
@@ -59,11 +59,11 @@ begin
   ... = 1 :
   begin
     simp only [div_eq_mul_inv],
-    rw lintegral_add',
-    { rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const'' _ (hg.pow_const q),
-        hf_norm, hg_norm, ← div_eq_mul_inv, ← div_eq_mul_inv, hpq.inv_add_inv_conj_ennreal], },
+    rw lintegral_add_left',
+    { rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm,
+        ← div_eq_mul_inv, ← div_eq_mul_inv, hpq.inv_add_inv_conj_ennreal],
+      simp [hpq.symm.pos], },
     { exact (hf.pow_const _).mul_const _, },
-    { exact (hg.pow_const _).mul_const _, },
   end
 end
 
@@ -86,16 +86,17 @@ begin
 end
 
 lemma lintegral_rpow_fun_mul_inv_snorm_eq_one {p : ℝ} (hp0_lt : 0 < p) {f : α → ℝ≥0∞}
-  (hf : ae_measurable f μ) (hf_nonzero : ∫⁻ a, (f a)^p ∂μ ≠ 0) (hf_top : ∫⁻ a, (f a)^p ∂μ ≠ ⊤) :
+  (hf_nonzero : ∫⁻ a, (f a)^p ∂μ ≠ 0) (hf_top : ∫⁻ a, (f a)^p ∂μ ≠ ⊤) :
   ∫⁻ c, (fun_mul_inv_snorm f p μ c)^p ∂μ = 1 :=
 begin
   simp_rw fun_mul_inv_snorm_rpow hp0_lt,
-  rw [lintegral_mul_const'' _ (hf.pow_const p), mul_inv_cancel hf_nonzero hf_top],
+  rw [lintegral_mul_const', mul_inv_cancel hf_nonzero hf_top],
+  rwa inv_ne_top
 end
 
 /-- Hölder's inequality in case of finite non-zero integrals -/
 lemma lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top {p q : ℝ} (hpq : p.is_conjugate_exponent q)
-  {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hg : ae_measurable g μ)
+  {f g : α → ℝ≥0∞} (hf : ae_measurable f μ)
   (hf_nontop : ∫⁻ a, (f a)^p ∂μ ≠ ⊤) (hg_nontop : ∫⁻ a, (g a)^q ∂μ ≠ ⊤)
   (hf_nonzero : ∫⁻ a, (f a)^p ∂μ ≠ 0) (hg_nonzero : ∫⁻ a, (g a)^q ∂μ ≠ 0) :
   ∫⁻ a, (f * g) a ∂μ ≤ (∫⁻ a, (f a)^p ∂μ)^(1/p) * (∫⁻ a, (g a)^q ∂μ)^(1/q) :=
@@ -116,37 +117,32 @@ begin
     rw lintegral_mul_const' (npf * nqg) _ (by simp [hf_nontop, hg_nontop, hf_nonzero, hg_nonzero]),
     nth_rewrite 1 ←one_mul (npf * nqg),
     refine mul_le_mul _ (le_refl (npf * nqg)),
-    have hf1 := lintegral_rpow_fun_mul_inv_snorm_eq_one hpq.pos hf hf_nonzero hf_nontop,
-    have hg1 := lintegral_rpow_fun_mul_inv_snorm_eq_one hpq.symm.pos hg hg_nonzero hg_nontop,
-    exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _)
-      (hg.mul_const _) hf1 hg1,
+    have hf1 := lintegral_rpow_fun_mul_inv_snorm_eq_one hpq.pos hf_nonzero hf_nontop,
+    have hg1 := lintegral_rpow_fun_mul_inv_snorm_eq_one hpq.symm.pos hg_nonzero hg_nontop,
+    exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _) hf1 hg1,
   end
 end
 
-lemma ae_eq_zero_of_lintegral_rpow_eq_zero {p : ℝ} (hp0_lt : 0 < p) {f : α → ℝ≥0∞}
+lemma ae_eq_zero_of_lintegral_rpow_eq_zero {p : ℝ} (hp0 : 0 ≤ p) {f : α → ℝ≥0∞}
   (hf : ae_measurable f μ) (hf_zero : ∫⁻ a, (f a)^p ∂μ = 0) :
   f =ᵐ[μ] 0 :=
 begin
   rw lintegral_eq_zero_iff' (hf.pow_const p) at hf_zero,
   refine filter.eventually.mp hf_zero (filter.eventually_of_forall (λ x, _)),
   dsimp only,
-  rw [pi.zero_apply, rpow_eq_zero_iff],
-  intro hx,
-  cases hx,
-  { exact hx.left, },
-  { exfalso,
-    linarith, },
+  rw [pi.zero_apply, ← not_imp_not],
+  exact λ hx, (rpow_pos_of_nonneg (pos_iff_ne_zero.2 hx) hp0).ne'
 end
 
-lemma lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero {p : ℝ} (hp0_lt : 0 < p)
+lemma lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero {p : ℝ} (hp0 : 0 ≤ p)
   {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hf_zero : ∫⁻ a, (f a)^p ∂μ = 0) :
   ∫⁻ a, (f * g) a ∂μ = 0 :=
 begin
   rw ←@lintegral_zero_fun α _ μ,
   refine lintegral_congr_ae _,
   suffices h_mul_zero : f * g =ᵐ[μ] 0 * g , by rwa zero_mul at h_mul_zero,
-  have hf_eq_zero : f =ᵐ[μ] 0, from ae_eq_zero_of_lintegral_rpow_eq_zero hp0_lt hf hf_zero,
-  exact filter.eventually_eq.mul hf_eq_zero (ae_eq_refl g),
+  have hf_eq_zero : f =ᵐ[μ] 0, from ae_eq_zero_of_lintegral_rpow_eq_zero hp0 hf hf_zero,
+  exact hf_eq_zero.mul (ae_eq_refl g),
 end
 
 lemma lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top {p q : ℝ} (hp0_lt : 0 < p) (hq0 : 0 ≤ q)
@@ -167,25 +163,24 @@ theorem lintegral_mul_le_Lp_mul_Lq (μ : measure α) {p q : ℝ} (hpq : p.is_con
   ∫⁻ a, (f * g) a ∂μ ≤ (∫⁻ a, (f a)^p ∂μ) ^ (1/p) * (∫⁻ a, (g a)^q ∂μ) ^ (1/q) :=
 begin
   by_cases hf_zero : ∫⁻ a, (f a) ^ p ∂μ = 0,
-  { refine le_trans (le_of_eq _) (zero_le _),
-    exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.pos hf hf_zero, },
+  { refine eq.trans_le _ (zero_le _),
+    exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.nonneg hf hf_zero, },
   by_cases hg_zero : ∫⁻ a, (g a) ^ q ∂μ = 0,
-  { refine le_trans (le_of_eq _) (zero_le _),
+  { refine eq.trans_le _ (zero_le _),
     rw mul_comm,
-    exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.symm.pos hg hg_zero, },
+    exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.symm.nonneg hg hg_zero, },
   by_cases hf_top : ∫⁻ a, (f a) ^ p ∂μ = ⊤,
   { exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.pos hpq.symm.nonneg hf_top hg_zero, },
   by_cases hg_top : ∫⁻ a, (g a) ^ q ∂μ = ⊤,
   { rw [mul_comm, mul_comm ((∫⁻ (a : α), (f a) ^ p ∂μ) ^ (1 / p))],
     exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.symm.pos hpq.nonneg hg_top hf_zero, },
   -- non-⊤ non-zero case
-  exact ennreal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top hpq hf hg hf_top hg_top hf_zero
-    hg_zero,
+  exact ennreal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top hpq hf hf_top hg_top hf_zero hg_zero
 end
 
 lemma lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top {p : ℝ}
   {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hf_top : ∫⁻ a, (f a) ^ p ∂μ < ⊤)
-  (hg : ae_measurable g μ) (hg_top : ∫⁻ a, (g a) ^ p ∂μ < ⊤) (hp1 : 1 ≤ p) :
+  (hg_top : ∫⁻ a, (g a) ^ p ∂μ < ⊤) (hp1 : 1 ≤ p) :
   ∫⁻ a, ((f + g) a) ^ p ∂μ < ⊤ :=
 begin
   have hp0_lt : 0 < p, from lt_of_lt_of_le zero_lt_one hp1,
@@ -216,14 +211,12 @@ begin
   end
   ... < ⊤ :
   begin
-    rw [lintegral_add', lintegral_const_mul'' _ (hf.pow_const p),
-      lintegral_const_mul'' _ (hg.pow_const p), ennreal.add_lt_top],
-    { have h_two : (2 : ℝ≥0∞) ^ (p - 1) < ⊤,
-      from ennreal.rpow_lt_top_of_nonneg (by simp [hp1]) ennreal.coe_ne_top,
-      repeat {rw ennreal.mul_lt_top_iff},
-      simp [hf_top, hg_top, h_two], },
-    { exact (hf.pow_const _).const_mul _ },
-    { exact (hg.pow_const _).const_mul _ },
+    have h_two : (2 : ℝ≥0∞) ^ (p - 1) ≠ ⊤,
+      from ennreal.rpow_ne_top_of_nonneg (by simp [hp1]) ennreal.coe_ne_top,
+    rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p),
+      lintegral_const_mul' _ _ h_two, ennreal.add_lt_top],
+    { exact ⟨ennreal.mul_lt_top h_two hf_top.ne, ennreal.mul_lt_top h_two hg_top.ne⟩ },
+    { exact (hf.pow_const p).const_mul _ }
   end
 end
 
@@ -317,7 +310,7 @@ begin
       = ∫⁻ (a : α), (f a + g a) * (f + g) a ^ (p - 1) ∂μ,
     from rfl,
     simp_rw [h_add_apply, add_mul],
-    rw lintegral_add' (hf.mul h_add_m) (hg.mul h_add_m),
+    rw lintegral_add_left' (hf.mul h_add_m),
   end
     ... ≤ ((∫⁻ a, (f a)^p ∂μ) ^ (1/p) + (∫⁻ a, (g a)^p ∂μ) ^ (1/p))
       * (∫⁻ a, (f a + g a)^p ∂μ) ^ (1/q) :
@@ -371,7 +364,7 @@ begin
   by_cases h1 : p = 1,
   { refine le_of_eq _,
     simp_rw [h1, one_div_one, ennreal.rpow_one],
-    exact lintegral_add' hf hg, },
+    exact lintegral_add_left' hf _, },
   have hp1_lt : 1 < p, by { refine lt_of_le_of_ne hp1 _, symmetry, exact h1, },
   have hpq := real.is_conjugate_exponent_conjugate_exponent hp1_lt,
   by_cases h0 : ∫⁻ a, ((f+g) a) ^ p ∂ μ = 0,
@@ -380,7 +373,7 @@ begin
   have htop : ∫⁻ a, ((f+g) a) ^ p ∂ μ ≠ ⊤,
   { rw ← ne.def at hf_top hg_top,
     rw ← lt_top_iff_ne_top at hf_top hg_top ⊢,
-    exact lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top hf hf_top hg hg_top hp1, },
+    exact lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top hf hf_top hg_top hp1, },
   exact lintegral_Lp_add_le_aux hpq hf hf_top hg hg_top h0 htop,
 end
 
diff --git a/src/measure_theory/integral/vitali_caratheodory.lean b/src/measure_theory/integral/vitali_caratheodory.lean
index aca51ddb1aa95..2a07f64a0eab1 100644
--- a/src/measure_theory/integral/vitali_caratheodory.lean
+++ b/src/measure_theory/integral/vitali_caratheodory.lean
@@ -136,9 +136,10 @@ begin
     rcases h₂ (ennreal.half_pos ε0).ne' with ⟨g₂, f₂_le_g₂, g₂cont, g₂int⟩,
     refine ⟨λ x, g₁ x + g₂ x, λ x, add_le_add (f₁_le_g₁ x) (f₂_le_g₂ x), g₁cont.add g₂cont, _⟩,
     simp only [simple_func.coe_add, ennreal.coe_add, pi.add_apply],
-    rw [lintegral_add f₁.measurable.coe_nnreal_ennreal f₂.measurable.coe_nnreal_ennreal,
-        lintegral_add g₁cont.measurable.coe_nnreal_ennreal g₂cont.measurable.coe_nnreal_ennreal],
+    rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal,
+        lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal],
     convert add_le_add g₁int g₂int using 1,
+    simp only [],
     conv_lhs { rw ← ennreal.add_halves ε },
     abel }
 end
@@ -199,7 +200,7 @@ begin
   { calc ∫⁻ (x : α), g x ∂μ
         ≤ ∫⁻ (x : α), f x + w x ∂μ + ε / 2 : gint
     ... = ∫⁻ (x : α), f x ∂ μ + ∫⁻ (x : α), w x ∂ μ + (ε / 2) :
-      by rw lintegral_add fmeas.coe_nnreal_ennreal wmeas.coe_nnreal_ennreal
+      by rw lintegral_add_right _ wmeas.coe_nnreal_ennreal
     ... ≤ ∫⁻ (x : α), f x ∂ μ + ε / 2 + ε / 2 :
       add_le_add_right (add_le_add_left wint.le _) _
     ... = ∫⁻ (x : α), f x ∂μ + ε : by rw [add_assoc, ennreal.add_halves] },
@@ -231,7 +232,7 @@ begin
       rw this,
       exact (f_lt_g0 x).trans_le le_self_add } },
   { calc ∫⁻ x, g0 x + g1 x ∂μ =  ∫⁻ x, g0 x ∂μ + ∫⁻ x, g1 x ∂μ :
-      lintegral_add g0_cont.measurable g1_cont.measurable
+      lintegral_add_left g0_cont.measurable _
     ... ≤ (∫⁻ x, f x ∂μ + ε / 2) + (0 + ε / 2) :
       begin
         refine add_le_add _ _,
@@ -345,16 +346,17 @@ begin
           simpa using hc,
         end } },
   { have A : ∫⁻ (x : α), f₁ x ∂μ + ∫⁻ (x : α), f₂ x ∂μ ≠ ⊤,
-      by rwa ← lintegral_add f₁.measurable.coe_nnreal_ennreal f₂.measurable.coe_nnreal_ennreal ,
+      by rwa ← lintegral_add_left f₁.measurable.coe_nnreal_ennreal,
     rcases h₁ (ennreal.add_ne_top.1 A).1 (ennreal.half_pos ε0).ne'
       with ⟨g₁, f₁_le_g₁, g₁cont, g₁int⟩,
     rcases h₂ (ennreal.add_ne_top.1 A).2 (ennreal.half_pos ε0).ne'
       with ⟨g₂, f₂_le_g₂, g₂cont, g₂int⟩,
     refine ⟨λ x, g₁ x + g₂ x, λ x, add_le_add (f₁_le_g₁ x) (f₂_le_g₂ x), g₁cont.add g₂cont, _⟩,
     simp only [simple_func.coe_add, ennreal.coe_add, pi.add_apply],
-    rw [lintegral_add f₁.measurable.coe_nnreal_ennreal f₂.measurable.coe_nnreal_ennreal,
-        lintegral_add g₁cont.measurable.coe_nnreal_ennreal g₂cont.measurable.coe_nnreal_ennreal],
+    rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal,
+        lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal],
     convert add_le_add g₁int g₂int using 1,
+    simp only [],
     conv_lhs { rw ← ennreal.add_halves ε },
     abel }
 end
diff --git a/src/measure_theory/measure/finite_measure_weak_convergence.lean b/src/measure_theory/measure/finite_measure_weak_convergence.lean
index 48b58a3c8b60a..31b4fd3860900 100644
--- a/src/measure_theory/measure/finite_measure_weak_convergence.lean
+++ b/src/measure_theory/measure/finite_measure_weak_convergence.lean
@@ -217,8 +217,7 @@ lemma test_against_nn_add (μ : finite_measure α) (f₁ f₂ : α →ᵇ ℝ≥
 begin
   simp only [←ennreal.coe_eq_coe, bounded_continuous_function.coe_add, ennreal.coe_add,
              pi.add_apply, test_against_nn_coe_eq],
-  apply lintegral_add;
-  exact bounded_continuous_function.nnreal.to_ennreal_comp_measurable _,
+  exact lintegral_add_left (bounded_continuous_function.nnreal.to_ennreal_comp_measurable _) _
 end
 
 lemma test_against_nn_smul [is_scalar_tower R ℝ≥0 ℝ≥0] [pseudo_metric_space R] [has_zero R]
diff --git a/src/probability/integration.lean b/src/probability/integration.lean
index 25f55ffae3231..54b2110888339 100644
--- a/src/probability/integration.lean
+++ b/src/probability/integration.lean
@@ -59,8 +59,8 @@ begin
     have h_measM_f' : measurable f', from h_meas_f'.mono hMf le_rfl,
     have h_measM_g : measurable g, from h_meas_g.mono hMf le_rfl,
     simp_rw [pi.add_apply, right_distrib],
-    rw [lintegral_add (h_mul_indicator _ h_measM_f') (h_mul_indicator _ h_measM_g),
-      lintegral_add h_measM_f' h_measM_g, right_distrib, h_ind_f', h_ind_g] },
+    rw [lintegral_add_left (h_mul_indicator _ h_measM_f'),
+      lintegral_add_left h_measM_f', right_distrib, h_ind_f', h_ind_g] },
   { intros f h_meas_f h_mono_f h_ind_f,
     have h_measM_f : ∀ n, measurable (f n), from λ n, (h_meas_f n).mono hMf le_rfl,
     simp_rw [ennreal.supr_mul],
@@ -93,8 +93,7 @@ begin
     have h_measM_f' : measurable f', from h_measMg_f'.mono hMg le_rfl,
     have h_measM_g : measurable g, from h_measMg_g.mono hMg le_rfl,
     simp_rw [pi.add_apply, left_distrib],
-    rw [lintegral_add h_measM_f' h_measM_g,
-      lintegral_add (h_measM_f.mul h_measM_f') (h_measM_f.mul h_measM_g),
+    rw [lintegral_add_left h_measM_f', lintegral_add_left (h_measM_f.mul h_measM_f'),
       left_distrib, h_ind_f', h_ind_g'] },
   { intros f' h_meas_f' h_mono_f' h_ind_f',
     have h_measM_f' : ∀ n, measurable (f' n), from λ n, (h_meas_f' n).mono hMg le_rfl,