refactor(measure_theory): make volume a bundled measure (leanprover…

…-community#3075)

This way we can `apply` and `rw` lemmas about `measure`s without
introducing a `volume`-specific version.

src/data/set/disjointed.lean

@@ -17,6 +17,11 @@ variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}
 /-- A relation `p` holds pairwise if `p i j` for all `i ≠ j`. -/
 def pairwise {α : Type*} (p : α → α → Prop) := ∀i j, i ≠ j → p i j
 
+theorem set.pairwise_on.on_injective {s : set α} {r : α → α → Prop} (hs : pairwise_on s r)
+  {f : β → α} (hf : function.injective f) (hfs : ∀ x, f x ∈ s) :
+  pairwise (r on f) :=
+λ i j hij, hs _ (hfs i) _ (hfs j) (hf.ne hij)
+
 theorem pairwise_on_bool {r} (hr : symmetric r) {a b : α} :
   pairwise (r on (λ c, cond c a b)) ↔ r a b :=
 by simp [pairwise, bool.forall_bool, function.on_fun];
@@ -26,6 +31,9 @@ theorem pairwise_disjoint_on_bool [semilattice_inf_bot α] {a b : α} :
   pairwise (disjoint on (λ c, cond c a b)) ↔ disjoint a b :=
 pairwise_on_bool $ λ _ _, disjoint.symm
 
+theorem pairwise.pairwise_on {p : α → α → Prop} (h : pairwise p) (s : set α) : s.pairwise_on p :=
+λ x hx y hy, h x y
+
 namespace set
 
 /-- If `f : ℕ → set α` is a sequence of sets, then `disjointed f` is

src/measure_theory/ae_eq_fun.lean

@@ -85,10 +85,7 @@ variables (α β)
 
 /-- The equivalence relation of being almost everywhere equal -/
 instance ae_eq_fun.setoid : setoid { f : α → β // measurable f } :=
-⟨ λf g, ∀ₘ a, f.1 a = g.1 a,
-  assume ⟨f, hf⟩, by filter_upwards [] assume a, rfl,
-  assume ⟨f, hf⟩ ⟨g, hg⟩ hfg, by filter_upwards [hfg] assume a, eq.symm,
-  assume ⟨f, hf⟩ ⟨g, hg⟩ ⟨h, hh⟩ hfg hgh, by filter_upwards [hfg, hgh] assume a, eq.trans ⟩
+⟨λf g, ∀ₘ a, f.1 a = g.1 a, λ f, ae_eq_refl f, λ f g, ae_eq_symm, λ f g h, ae_eq_trans⟩
 
 /-- The space of equivalence classes of measurable functions, where two measurable functions are
     equivalent if they agree almost everywhere, i.e., they differ on a set of measure `0`.  -/
@@ -188,7 +185,7 @@ by { rw comp₂_eq_mk_to_fun, apply all_ae_mk_to_fun }
 def lift_pred (p : β → Prop) (f : α →ₘ β) : Prop :=
 quotient.lift_on f (λf, ∀ₘ a, p (f.1 a))
 begin
-  assume f g h, dsimp, refine propext (all_ae_congr _),
+  assume f g h, dsimp, refine propext (eventually_congr _),
   filter_upwards [h], simp {contextual := tt}
 end
 
@@ -276,10 +273,10 @@ comp₂_to_fun _ _ _ _
 instance : add_monoid (α →ₘ γ) :=
 { zero      := 0,
   add       := (+),
-  add_zero  := by rintros ⟨a⟩; exact quotient.sound (all_ae_of_all $ assume a, add_zero _),
-  zero_add  := by rintros ⟨a⟩; exact quotient.sound (all_ae_of_all $ assume a, zero_add _),
+  add_zero  := by rintros ⟨a⟩; exact quotient.sound (ae_of_all _ $ assume a, add_zero _),
+  zero_add  := by rintros ⟨a⟩; exact quotient.sound (ae_of_all _ $ assume a, zero_add _),
   add_assoc :=
-    by rintros ⟨a⟩ ⟨b⟩ ⟨c⟩; exact quotient.sound (all_ae_of_all $ assume a, add_assoc _ _ _) }
+    by rintros ⟨a⟩ ⟨b⟩ ⟨c⟩; exact quotient.sound (ae_of_all _ $ assume a, add_assoc _ _ _) }
 
 end add_monoid
 
@@ -308,7 +305,7 @@ lemma neg_to_fun (f : α →ₘ γ) : ∀ₘ a, (-f).to_fun a = - f.to_fun a :=
 variables [second_countable_topology γ]
 instance : add_group (α →ₘ γ) :=
 { neg          := has_neg.neg,
-  add_left_neg := by rintros ⟨a⟩; exact quotient.sound (all_ae_of_all $ assume a, add_left_neg _),
+  add_left_neg := by rintros ⟨a⟩; exact quotient.sound (ae_of_all _ $ assume a, add_left_neg _),
   .. ae_eq_fun.add_monoid }
 
 @[simp] lemma mk_sub_mk (f g : α → γ) (hf hg) :
@@ -472,7 +469,7 @@ variables {γ : Type*} [metric_space γ] [second_countable_topology γ] [measura
 lemma edist_mk_mk' {f g : α → γ} (hf hg) :
   edist (mk f hf) (mk g hg) = ∫⁻ x, nndist (f x) (g x) :=
 show  (∫⁻ x, edist (f x) (g x)) =  ∫⁻ x, nndist (f x) (g x), from
-lintegral_congr_ae $all_ae_of_all $ assume a, edist_nndist _ _
+lintegral_congr_ae $ ae_of_all _ $ assume a, edist_nndist _ _
 
 lemma edist_to_fun' (f g : α →ₘ γ) : edist f g = ∫⁻ x, nndist (f.to_fun x) (g.to_fun x) :=
 by conv_lhs { rw [self_eq_mk f, self_eq_mk g, edist_mk_mk'] }

src/measure_theory/bochner_integration.lean

@@ -284,7 +284,7 @@ begin
   by_cases eq : f a = g a,
   { dsimp only [pair_apply], rw eq },
   { have : volume ((pair f g) ⁻¹' {(f a, g a)}) = 0,
-    { refine volume_mono_null (assume a' ha', _) h,
+    { refine measure_mono_null (assume a' ha', _) h,
       simp only [set.mem_preimage, mem_singleton_iff, pair_apply, prod.mk.inj_iff] at ha',
       show f a' ≠ g a',
       rwa [ha'.1, ha'.2] },
@@ -664,7 +664,7 @@ lemma dist_to_simple_func (f g : α →₁ₛ β) : dist f g =
   ennreal.to_real (∫⁻ x, edist (f.to_simple_func x) (g.to_simple_func x)) :=
 begin
   rw [dist_eq, l1.dist_to_fun, ennreal.to_real_eq_to_real],
-  { rw lintegral_rw₂, repeat { exact all_ae_eq_symm (to_simple_func_eq_to_fun _) } },
+  { rw lintegral_rw₂, repeat { exact ae_eq_symm (to_simple_func_eq_to_fun _) } },
   { exact l1.lintegral_edist_to_fun_lt_top _ _ },
   { exact lintegral_edist_to_simple_func_lt_top _ _ }
 end
@@ -705,7 +705,8 @@ end
 end to_simple_func
 
 section coe_to_l1
-/-! The embedding of integrable simple functions `α →₁ₛ β` into L1 is a uniform and dense embedding. -/
+/-! The embedding of integrable simple functions `α →₁ₛ β` into L1 is a uniform and dense
+embedding. -/
 
 lemma exists_simple_func_near (f : α →₁ β) {ε : ℝ} (ε0 : 0 < ε) :
   ∃ s : α →₁ₛ β, dist f s < ε :=

src/measure_theory/giry_monad.lean

@@ -71,11 +71,11 @@ measurable_of_measurable_coe _ $ assume s hs,
 lemma measurable_integral (f : α → ennreal) (hf : measurable f) :
   measurable (λμ : measure α, μ.integral f) :=
 suffices measurable (λμ : measure α,
-  (⨆n:ℕ, @simple_func.integral α { μ := μ } (simple_func.eapprox f n)) : _ → ennreal),
+  (⨆n:ℕ, @simple_func.integral α { volume := μ } (simple_func.eapprox f n)) : _ → ennreal),
 begin
   convert this,
   funext μ,
-  exact @lintegral_eq_supr_eapprox_integral α {μ := μ} f hf
+  exact @lintegral_eq_supr_eapprox_integral α {volume := μ} f hf
 end,
 measurable_supr $ assume n,
   begin
@@ -113,8 +113,8 @@ begin
   apply lintegral_eq_supr_eapprox_integral,
   { exact hf },
   have : ∀n x,
-    @volume α { μ := join m} (⇑(simple_func.eapprox (λ (a : α), f a) n) ⁻¹' {x}) =
-    m.integral (λμ, @volume α { μ := μ } ((⇑(simple_func.eapprox (λ (a : α), f a) n) ⁻¹' {x}))) :=
+    @volume α { volume := join m} (⇑(simple_func.eapprox (λ (a : α), f a) n) ⁻¹' {x}) =
+    m.integral (λμ, @volume α { volume := μ } ((⇑(simple_func.eapprox (λ (a : α), f a) n) ⁻¹' {x}))) :=
     assume n x, join_apply (simple_func.measurable_sn _ _),
   conv {
     to_lhs,
@@ -143,12 +143,12 @@ begin
     exact hf _ _ },
   specialize this (λn, simple_func.range (simple_func.eapprox f n)),
   specialize this
-    (λn r μ, @volume α { μ := μ } (⇑(simple_func.eapprox (λ (a : α), f a) n) ⁻¹' {r})),
+    (λn r μ, @volume α { volume := μ } (⇑(simple_func.eapprox (λ (a : α), f a) n) ⁻¹' {r})),
   refine this _ _; clear this,
   { assume n r,
     apply measurable_coe,
     exact simple_func.measurable_sn _ _ },
-  { change monotone (λn μ, @simple_func.integral α {μ := μ} (simple_func.eapprox f n)),
+  { change monotone (λn μ, @simple_func.integral α {volume := μ} (simple_func.eapprox f n)),
     assume n m h μ,
     apply simple_func.integral_le_integral,
     apply simple_func.monotone_eapprox,

src/measure_theory/integration.lean

@@ -387,7 +387,7 @@ lemma volume_bUnion_preimage (s : finset β) (f : α →ₛ β) :
   volume (⋃b ∈ s, f ⁻¹' {b}) = ∑ b in s, volume (f ⁻¹' {b}) :=
 begin
   /- Taking advantage of the fact that `f ⁻¹' {b}` are disjoint for `b ∈ s`. -/
-  rw [volume_bUnion_finset],
+  rw [measure_bUnion_finset],
   { simp only [pairwise_on, (on), finset.mem_coe, ne.def],
     rintros _ _ _ _ ne _ ⟨h₁, h₂⟩,
     simp only [mem_singleton_iff, mem_preimage] at h₁ h₂,
@@ -509,7 +509,7 @@ calc (restrict (const α c) s).integral = c * volume ((const α c) ⁻¹' {c} 
       { assume empty,
         have : (@const α ennreal _ c) ⁻¹' {c} ∩ s = ∅,
         { ext a, exfalso, exact h ⟨a⟩ },
-        simp only [this, volume_empty, mul_zero] } }
+        simp only [this, measure_empty, mul_zero] } }
   end
   ... = c * volume s : by rw [this, univ_inter]
 
@@ -541,7 +541,7 @@ begin
   by_cases eq : f a = g a,
   { dsimp only [pair_apply], rw eq },
   { have : volume ((pair f g) ⁻¹' {(f a, g a)}) = 0,
-    { refine volume_mono_null (assume a' ha', _) h,
+    { refine measure_mono_null (assume a' ha', _) h,
       simp at ha',
       show f a' ≠ g a',
       rwa [ha'.1, ha'.2] },
@@ -600,9 +600,9 @@ begin
       rw [coe_map, @preimage_comp _ _ _ f g, preimage_subset_preimage_iff],
       { simp only [set.mem_preimage, set.mem_singleton, set.singleton_subset_iff] },
       { rw set.singleton_subset_iff, rw mem_range at b_mem, exact b_mem },
-    exact lt_of_le_of_lt (volume_mono this) (h (g b) gb0) },
+    exact lt_of_le_of_lt (measure_mono this) (h (g b) gb0) },
   { rw ← preimage_eq_empty_iff at b_mem,
-    rw [b_mem, volume_empty],
+    rw [b_mem, measure_empty],
     exact with_top.zero_lt_top }
 end
 
@@ -613,9 +613,9 @@ begin
   rw [pair_preimage_singleton],
   rw [ne.def, prod.eq_iff_fst_eq_snd_eq, not_and_distrib] at hbc,
   refine or.elim hbc (λ h : b≠0, _) (λ h : c≠0, _),
-  { calc _ ≤ volume (f ⁻¹' {b}) : volume_mono (set.inter_subset_left _ _)
+  { calc _ ≤ volume (f ⁻¹' {b}) : measure_mono (set.inter_subset_left _ _)
       ... < ⊤ : hf _ h },
-  { calc _ ≤ volume (g ⁻¹' {c}) : volume_mono (set.inter_subset_right _ _)
+  { calc _ ≤ volume (g ⁻¹' {c}) : measure_mono (set.inter_subset_right _ _)
       ... < ⊤ : hg _ h },
 end
 
@@ -625,7 +625,7 @@ begin
   rw integral, apply sum_lt_top,
   intros a ha,
   have : f ⁻¹' {⊤} = -{a : α | f a < ⊤}, { ext, simp },
-  have vol_top : volume (f ⁻¹' {⊤}) = 0, { rw [this, volume, ← measure.mem_a_e_iff], exact h₁ },
+  have vol_top : volume (f ⁻¹' {⊤}) = 0, { rw [this, ← mem_ae_iff], exact h₁ },
   by_cases hat : a = ⊤,
   { rw [hat, vol_top, mul_zero], exact with_top.zero_lt_top },
   { by_cases haz : a = 0,
@@ -647,7 +647,7 @@ begin
     rcases h with ⟨h, h'⟩,
     refine or.elim h (λh, by contradiction) (λh, h) },
   { rw ← preimage_eq_empty_iff at b_mem,
-    rw [b_mem, volume_empty],
+    rw [b_mem, measure_empty],
     exact with_top.zero_lt_top }
 end
 
@@ -699,7 +699,7 @@ begin
     refine le_supr_of_le (s.map ennreal.to_nnreal) (le_supr_of_le this (le_of_eq $ integral_congr _ _ _)),
     exact filter.mem_sets_of_superset h (assume a ha, (ennreal.coe_to_nnreal ha).symm) },
   { have h_vol_s : volume {a : α | s a = ⊤} ≠ 0,
-      from mt volume_zero_iff_all_ae_nmem.1 h,
+      from mt measure_zero_iff_ae_nmem.1 h,
     let n : ℕ → (α →ₛ nnreal) := λn, restrict (const α (n : nnreal)) (s ⁻¹' {⊤}),
     have n_le_s : ∀i, (n i).map c ≤ s,
     { assume i a,
@@ -787,7 +787,7 @@ begin
     ... ≤ ∑ r in (rs.map c).range, (⨆n, r * volume ((rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a})) :
       le_of_eq (finset.sum_congr rfl $ assume x hx,
         begin
-          rw [volume, measure_Union_eq_supr_nat _ (mono x), ennreal.mul_supr],
+          rw [measure_Union_eq_supr_nat _ (mono x), ennreal.mul_supr],
           { assume i,
             refine ((rs.map c).preimage_measurable _).inter _,
             exact (hf i).preimage is_measurable_Ici }
@@ -797,7 +797,7 @@ begin
         refine le_of_eq _,
         rw [ennreal.finset_sum_supr_nat],
         assume p i j h,
-        exact canonically_ordered_semiring.mul_le_mul (le_refl _) (volume_mono $ mono p h)
+        exact canonically_ordered_semiring.mul_le_mul (le_refl _) (measure_mono $ mono p h)
       end
     ... ≤ (⨆n:ℕ, ((rs.map c).restrict {a | (rs.map c) a ≤ f n a}).integral) :
     begin
@@ -922,8 +922,8 @@ lemma lintegral_le_lintegral_ae {f g : α → ennreal} (h : ∀ₘ a, f a ≤ g
   (∫⁻ a, f a) ≤ (∫⁻ a, g a) :=
 begin
   rcases exists_is_measurable_superset_of_measure_eq_zero h with ⟨t, hts, ht, ht0⟩,
-  have : - t ∈ (@measure_space.μ α _).a_e,
-  { rw [measure.mem_a_e_iff, compl_compl, ht0] },
+  have : - t ∈ (@volume α _).ae,
+  { rw [mem_ae_iff, compl_compl, ht0] },
   refine (supr_le $ assume s, supr_le $ assume hfs,
     le_supr_of_le (s.restrict (- t)) $ le_supr_of_le _ _),
   { assume a,
@@ -985,14 +985,14 @@ begin
   refine iff.intro (assume h, _) (assume h, _),
   { have : ∀n:ℕ, ∀ₘ a, f a < n⁻¹,
     { assume n,
-      rw [all_ae_iff, ← le_zero_iff_eq, ← @ennreal.zero_div n⁻¹,
+      rw [ae_iff, ← le_zero_iff_eq, ← @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_volume_ge_le_lintegral hf n⁻¹,
         or.inl (ennreal.inv_ne_zero.2 ennreal.coe_nat_ne_top),
         or.inr ennreal.zero_ne_top] },
-    refine (all_ae_all_iff.2 this).mono (λ a ha, _),
+    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 },
@@ -1005,12 +1005,12 @@ lemma lintegral_supr_ae {f : ℕ → α → ennreal} (hf : ∀n, measurable (f n
   (h_mono : ∀n, ∀ₘ a, f n a ≤ f n.succ a) :
   (∫⁻ a, ⨆n, f n a) = (⨆n, ∫⁻ a, f n a) :=
 let ⟨s, hs⟩ := exists_is_measurable_superset_of_measure_eq_zero
-                       (all_ae_iff.1 (all_ae_all_iff.2 h_mono)) in
+                       (ae_iff.1 (ae_all_iff.2 h_mono)) in
 let g := λ n a, if a ∈ s then 0 else f n a in
 have g_eq_f : ∀ₘ a, ∀n, g n a = f n a,
   begin
     have := hs.2.2, rw [← compl_compl s] at this,
-    filter_upwards [(measure.mem_a_e_iff (-s)).2 this] assume a ha n, if_neg ha
+    filter_upwards [(mem_ae_iff (-s)).2 this] assume a ha n, if_neg ha
   end,
 calc
   (∫⁻ a, ⨆n, f n a) = (∫⁻ a, ⨆n, g n a) :
@@ -1061,15 +1061,15 @@ calc
     (calc
       (∫⁻ a, ⨅n, f n a)  ≤ lintegral (f 0) : lintegral_mono (assume a, infi_le _ _)
           ... < ⊤ : h_fin  )
-    (all_ae_of_all $ assume a, infi_le _ _)).symm
+    (ae_of_all _ $ assume a, infi_le _ _)).symm
   ... = ∫⁻ a, ⨆n, f 0 a - f n a : congr rfl (funext (assume a, ennreal.sub_infi))
   ... = ⨆n, ∫⁻ a, f 0 a - f n a :
     lintegral_supr_ae
       (assume n, (h_meas 0).ennreal_sub (h_meas n))
       (assume n, by
         filter_upwards [h_mono n] assume a ha, ennreal.sub_le_sub (le_refl _) ha)
   ... = ⨆n, lintegral (f 0) - ∫⁻ a, f n a :
-    have h_mono : ∀ₘ a, ∀n:ℕ, f n.succ a ≤ f n a := all_ae_all_iff.2 h_mono,
+    have h_mono : ∀ₘ a, ∀n:ℕ, f n.succ a ≤ f n a := ae_all_iff.2 h_mono,
     have h_mono : ∀n, ∀ₘa, f n a ≤ f 0 a := assume n,
     begin
       filter_upwards [h_mono], simp only [mem_set_of_eq], assume a, assume h, induction n with n ih,
@@ -1087,7 +1087,7 @@ lemma lintegral_infi
   {f : ℕ → α → ennreal} (h_meas : ∀n, measurable (f n))
   (h_mono : ∀ ⦃m n⦄, m ≤ n → f n ≤ f m) (h_fin : lintegral (f 0) < ⊤) :
   (∫⁻ a, ⨅n, f n a) = (⨅n, ∫⁻ a, f n a) :=
-lintegral_infi_ae h_meas (λ n, all_ae_of_all $ h_mono $ le_of_lt n.lt_succ_self) h_fin
+lintegral_infi_ae h_meas (λ n, ae_of_all _ $ h_mono $ le_of_lt n.lt_succ_self) h_fin
 
 section priority
 -- for some reason the next proof fails without changing the priority of this instance
@@ -1121,7 +1121,7 @@ calc
       { assume n, exact measurable_bsupr _ hf_meas },
       { assume n m hnm a, exact (supr_le_supr_of_subset $ λ i hi, le_trans hnm hi) },
       { refine lt_of_le_of_lt (lintegral_le_lintegral_ae _) h_fin,
-        refine (all_ae_all_iff.2 h_bound).mono (λ n hn, _),
+        refine (ae_all_iff.2 h_bound).mono (λ n hn, _),
         exact supr_le (λ i, supr_le $ λ hi, hn i) }
     end
   ... = ∫⁻ a, limsup at_top (λn, f n a) :
@@ -1245,11 +1245,11 @@ end lintegral
 namespace measure
 
 def integral [measurable_space α] (m : measure α) (f : α → ennreal) : ennreal :=
-@lintegral α { μ := m } f
+@lintegral α { volume := m } f
 
 variables [measurable_space α] {m : measure α}
 
-@[simp] lemma integral_zero : m.integral (λa, 0) = 0 := @lintegral_zero α { μ := m }
+@[simp] lemma integral_zero : m.integral (λa, 0) = 0 := @lintegral_zero α { volume := m }
 
 lemma integral_map [measurable_space β] {f : β → ennreal} {g : α → β}
   (hf : measurable f) (hg : measurable g) : (map g m).integral f = m.integral (f ∘ g) :=
@@ -1264,10 +1264,10 @@ begin
 end
 
 lemma integral_dirac (a : α) {f : α → ennreal} (hf : measurable f) : (dirac a).integral f = f a :=
-have ∀f:α →ₛ ennreal, @simple_func.integral α {μ := dirac a} f = f a,
+have ∀f:α →ₛ ennreal, @simple_func.integral α {volume := dirac a} f = f a,
 begin
   assume f,
-  have : ∀r, @volume α { μ := dirac a } (⇑f ⁻¹' {r}) = ⨆ h : f a = r, 1,
+  have : ∀r, @volume α { volume := dirac a } (⇑f ⁻¹' {r}) = ⨆ h : f a = r, 1,
   { assume r,
     transitivity,
     apply dirac_apply,

src/measure_theory/l1_space.lean

@@ -99,7 +99,7 @@ begin
 end
 
 lemma integrable_congr_ae {f g : α → β} (h : ∀ₘ a, f a = g a) : integrable f ↔ integrable g :=
-iff.intro (λhf, integrable_of_ae_eq hf h) (λhg, integrable_of_ae_eq hg (all_ae_eq_symm h))
+iff.intro (λhf, integrable_of_ae_eq hf h) (λhg, integrable_of_ae_eq hg (ae_eq_symm h))
 
 lemma integrable_of_le_ae {f : α → β} {g : α → γ} (h : ∀ₘ a, ∥f a∥ ≤ ∥g a∥) (hg : integrable g) :
   integrable f :=
@@ -112,7 +112,7 @@ end
 
 lemma integrable_of_le {f : α → β} {g : α → γ} (h : ∀a, ∥f a∥ ≤ ∥g a∥) (hg : integrable g) :
   integrable f :=
-integrable_of_le_ae (all_ae_of_all h) hg
+integrable_of_le_ae (ae_of_all _ h) hg
 
 lemma lintegral_nnnorm_eq_lintegral_edist (f : α → β) :
   (∫⁻ a, nnnorm (f a)) = ∫⁻ a, edist (f a) 0 :=
@@ -252,7 +252,7 @@ lemma all_ae_of_real_f_le_bound (h_bound : ∀ n, ∀ₘ a, ∥F n a∥ ≤ boun
   ∀ₘ a, ennreal.of_real ∥f a∥ ≤ ennreal.of_real (bound a) :=
 begin
   have F_le_bound := all_ae_of_real_F_le_bound h_bound,
-  rw ← all_ae_all_iff at F_le_bound,
+  rw ← ae_all_iff at F_le_bound,
   apply F_le_bound.mp ((all_ae_tendsto_of_real_norm h_lim).mono _),
   assume a tendsto_norm F_le_bound,
   exact le_of_tendsto' at_top_ne_bot tendsto_norm (F_le_bound)

src/measure_theory/lebesgue_measure.lean

@@ -233,7 +233,7 @@ instance : measure_space ℝ :=
   trimmed := lebesgue_outer_trim }⟩
 
 @[simp] theorem lebesgue_to_outer_measure :
-  (measure_space.μ : measure ℝ).to_outer_measure = lebesgue_outer := rfl
+  (volume : measure ℝ).to_outer_measure = lebesgue_outer := rfl
 
 end measure_theory
 
@@ -264,7 +264,7 @@ lemma real.volume_lt_top_of_bounded {s : set ℝ} (h : bounded s) : volume s < 
 begin
   rw [real.bounded_iff_bdd_below_bdd_above, bdd_below_bdd_above_iff_subset_interval] at h,
   rcases h with ⟨a, b, h⟩,
-  calc volume s ≤ volume [a, b] : volume_mono h
+  calc volume s ≤ volume [a, b] : measure_mono h
     ... < ⊤ : by { rw real.volume_interval, exact ennreal.coe_lt_top }
 end