diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index fe664a7e..cde2f7c2 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -33,7 +33,7 @@ Below, I will try to give a translation of some notation/conventions. We use mat
 | `Kₛ(x, y)`       | `Ks s x y`       |         |
 | `T_* f(x)`       | `nontangentialOperator K f x`       | The associated nontangential Calderon Zygmund operator |
 | `T_Q^θ f(x)`       | `linearizedNontangentialOperator Q θ K f x`       | The linearized associated nontangential Calderon Zygmund operator |
-| `T f(x)`       | `CarlesonOperator K f x` | The generalized Carleson operator        |
+| `T f(x)`       | `carlesonOperator K f x` | The generalized Carleson operator        |
 | `T_Q f(x)`       | `linearizedCarlesonOperator Q K f x` | The linearized generalized Carleson operator        |
 | `T_𝓝^θ f(x)`       | `nontangentialMaximalFunction K θ f x` |   |
 | `Tₚ f(x)`       | `carlesonOn p f x`       |         |
diff --git a/Carleson/AntichainOperator.lean b/Carleson/AntichainOperator.lean
index 3d9160ce..f96591af 100644
--- a/Carleson/AntichainOperator.lean
+++ b/Carleson/AntichainOperator.lean
@@ -146,12 +146,12 @@ lemma MaximalBoundAntichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤
         /- simp only [T, indicator, if_pos hxE, mul_ite, mul_zero, ENNReal.coe_le_coe,
           ← NNReal.coe_le_coe, coe_nnnorm] -/
         /- simp only [T, indicator, if_pos hxE]
-        apply le_trans (MeasureTheory.ennnorm_integral_le_lintegral_ennnorm _)
-        apply MeasureTheory.lintegral_mono
+        apply le_trans (ennnorm_integral_le_lintegral_ennnorm _)
+        apply lintegral_mono
         intro z w -/
         simp only [carlesonOn, indicator, if_pos hxE]
-        apply le_trans (MeasureTheory.ennnorm_integral_le_lintegral_ennnorm _)
-        apply MeasureTheory.lintegral_mono
+        apply le_trans (ennnorm_integral_le_lintegral_ennnorm _)
+        apply lintegral_mono
         intro z w
         simp only [nnnorm_mul, coe_mul, some_eq_coe', Nat.cast_pow,
           Nat.cast_ofNat, zpow_neg, mul_ite, mul_zero]
@@ -194,7 +194,7 @@ lemma MaximalBoundAntichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤
     _ = (2 : ℝ≥0)^(5*a + 101*a^3) * ⨍⁻ y, ‖f y‖₊ ∂volume.restrict (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)) := by
       congr 2
 
-      --apply MeasureTheory.Measure.restrict_congr_set
+      --apply Measure.restrict_congr_set
       --refine ae_eq_of_subset_of_measure_ge ?_ ?_ ?_ ?_
       --sorry
       sorry
@@ -282,7 +282,7 @@ lemma Dens2Antichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) (
       apply mul_le_mul_of_nonneg_right _ (zero_le _)
       have h2 : (2 : ℝ≥0∞) ^ (107 * a ^ 3) = ‖(2 : ℝ) ^ (107 * a ^ 3)‖₊ := by
         simp only [nnnorm_pow, nnnorm_two, ENNReal.coe_pow, coe_ofNat]
-      rw [h2, ← MeasureTheory.eLpNorm_const_smul]
+      rw [h2, ← eLpNorm_const_smul]
       apply eLpNorm_mono_nnnorm
       intro z
       have MB_top : MB volume (↑𝔄) 𝔠 (fun 𝔭 ↦ 8 * ↑D ^ 𝔰 𝔭) f z ≠ ⊤ := by
diff --git a/Carleson/Classical/CarlesonOnTheRealLine.lean b/Carleson/Classical/CarlesonOnTheRealLine.lean
index e89f8394..03b429c4 100644
--- a/Carleson/Classical/CarlesonOnTheRealLine.lean
+++ b/Carleson/Classical/CarlesonOnTheRealLine.lean
@@ -11,8 +11,6 @@ import Carleson.Classical.CarlesonOperatorReal
 import Carleson.Classical.VanDerCorput
 
 import Mathlib.Analysis.Fourier.AddCircle
-import Mathlib.MeasureTheory.Integral.IntervalIntegral
-import Mathlib.Analysis.SpecialFunctions.Integrals
 
 noncomputable section
 
@@ -596,12 +594,12 @@ lemma carlesonOperatorReal_le_carlesonOperator : T ≤ carlesonOperator K := by
 lemma rcarleson {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G)
     (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
     ∫⁻ x in G, T f x ≤
-    ENNReal.ofReal (C10_0_1 4 2) * (MeasureTheory.volume G) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ := by
+    ENNReal.ofReal (C10_0_1 4 2) * (volume G) ^ (2 : ℝ)⁻¹ * (volume F) ^ (2 : ℝ)⁻¹ := by
   have conj_exponents : Real.IsConjExponent 2 2 := by rw [Real.isConjExponent_iff_eq_conjExponent] <;> norm_num
   calc ∫⁻ x in G, T f x
     _ ≤ ∫⁻ x in G, carlesonOperator K f x :=
-      MeasureTheory.lintegral_mono (carlesonOperatorReal_le_carlesonOperator _)
-    _ ≤ ENNReal.ofReal (C10_0_1 4 2) * (MeasureTheory.volume G) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ :=
+      lintegral_mono (carlesonOperatorReal_le_carlesonOperator _)
+    _ ≤ ENNReal.ofReal (C10_0_1 4 2) * (volume G) ^ (2 : ℝ)⁻¹ * (volume F) ^ (2 : ℝ)⁻¹ :=
       two_sided_metric_carleson (a := 4) (by norm_num) (by simp) conj_exponents hF hG Hilbert_strong_2_2 f hmf hf
 
 end section
diff --git a/Carleson/Classical/CarlesonOperatorReal.lean b/Carleson/Classical/CarlesonOperatorReal.lean
index e402dfcd..a298f655 100644
--- a/Carleson/Classical/CarlesonOperatorReal.lean
+++ b/Carleson/Classical/CarlesonOperatorReal.lean
@@ -5,6 +5,8 @@ import Carleson.Classical.HilbertKernel
 
 noncomputable section
 
+open MeasureTheory
+
 --TODO: avoid this extra definition?
 def carlesonOperatorReal (K : ℝ → ℝ → ℂ) (f : ℝ → ℂ) (x : ℝ) : ENNReal :=
   ⨆ (n : ℤ) (r : ℝ) (_ : 0 < r) (_ : r < 1),
@@ -24,8 +26,8 @@ lemma annulus_real_eq {x r R: ℝ} (r_nonneg : 0 ≤ r) : {y | dist x y ∈ Set.
     · exact ⟨by right; linarith, by constructor <;> linarith⟩
 
 lemma annulus_real_volume {x r R : ℝ} (hr : r ∈ Set.Icc 0 R) :
-    MeasureTheory.volume {y | dist x y ∈ Set.Ioo r R} = ENNReal.ofReal (2 * (R - r)) := by
-  rw [annulus_real_eq hr.1, MeasureTheory.measure_union _ measurableSet_Ioo, Real.volume_Ioo, Real.volume_Ioo, ← ENNReal.ofReal_add (by linarith [hr.2]) (by linarith [hr.2])]
+    volume {y | dist x y ∈ Set.Ioo r R} = ENNReal.ofReal (2 * (R - r)) := by
+  rw [annulus_real_eq hr.1, measure_union _ measurableSet_Ioo, Real.volume_Ioo, Real.volume_Ioo, ← ENNReal.ofReal_add (by linarith [hr.2]) (by linarith [hr.2])]
   ring_nf
   rw [Set.disjoint_iff]
   intro y hy
@@ -72,7 +74,7 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
     congr with _
     congr with _
     congr 2
-    rw [← MeasureTheory.integral_indicator annulus_measurableSet]
+    rw [← integral_indicator annulus_measurableSet]
   rw [this]
   set Q : Set ℝ := Rat.cast '' Set.univ with Qdef
   have hQ : Dense Q ∧ Countable Q := by
@@ -108,7 +110,7 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
       · apply isOpen_Ioo
       · rw [Sdef]
         constructor <;> linarith [hr.1]
-    apply MeasureTheory.continuousAt_of_dominated _  h_bound
+    apply continuousAt_of_dominated _  h_bound
     · have F_bound_on_set :  ∀ a ∈ {y | dist x y ∈ Set.Ioo (r / 2) 1},
           ‖f a * K x a * (Complex.I * ↑n * ↑a).exp‖ ≤ B * ‖2 ^ (2 : ℝ) / (2 * (r / 2))‖ := by
         intro a ha
@@ -130,13 +132,13 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
                 exact ha.1.le
       rw [bound_def, Fdef]
       conv => pattern ‖_‖; rw [norm_indicator_eq_indicator_norm]
-      rw [MeasureTheory.integrable_indicator_iff annulus_measurableSet]
-      apply MeasureTheory.Measure.integrableOn_of_bounded
+      rw [integrable_indicator_iff annulus_measurableSet]
+      apply Measure.integrableOn_of_bounded
       · rw [annulus_real_volume (by constructor <;> linarith [hr.1, hr.2])]
         exact ENNReal.ofReal_ne_top
       · apply ((Measurable.of_uncurry_left (measurable_mul_kernel f_measurable)).norm).aestronglyMeasurable
       · --interesting part
-        rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
+        rw [ae_restrict_iff' annulus_measurableSet]
         simp_rw [norm_norm]
         apply Filter.Eventually.of_forall
         apply F_bound_on_set
@@ -200,8 +202,8 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
         rcases this with h | h
         · left; linarith
         · right; linarith
-      rw [MeasureTheory.ae_iff]
-      exact MeasureTheory.measure_mono_null subset_finite (Finset.measure_zero _ _)
+      rw [ae_iff]
+      exact measure_mono_null subset_finite (Finset.measure_zero _ _)
     · exact Filter.Eventually.of_forall fun r ↦ ((Measurable.of_uncurry_left
         (measurable_mul_kernel f_measurable)).indicator annulus_measurableSet).aestronglyMeasurable
   rw [this]
@@ -210,7 +212,7 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
   intro r _
   apply measurable_coe_nnreal_ennreal.comp (measurable_nnnorm.comp _)
   rw [← stronglyMeasurable_iff_measurable]
-  apply MeasureTheory.StronglyMeasurable.integral_prod_right
+  apply StronglyMeasurable.integral_prod_right
   rw [stronglyMeasurable_iff_measurable, Fdef]
   exact (measurable_mul_kernel f_measurable).indicator (measurable_dist measurableSet_Ioo)
 
@@ -252,7 +254,7 @@ lemma carlesonOperatorReal_mul {f : ℝ → ℂ} {x : ℝ} {a : ℝ} (ha : 0 < a
   apply NNReal.eq
   simp only [coe_nnnorm, NNReal.coe_mul]
   rw [← Real.norm_of_nonneg (@NNReal.zero_le_coe a.toNNReal), ← Complex.norm_real, ← norm_mul,
-    ← MeasureTheory.integral_mul_left, Real.coe_toNNReal a ha.le]
+    ← integral_mul_left, Real.coe_toNNReal a ha.le]
   congr with y
   field_simp
   rw [mul_div_cancel_left₀]
diff --git a/Carleson/Classical/ClassicalCarleson.lean b/Carleson/Classical/ClassicalCarleson.lean
index 025efd63..1f7c3b35 100644
--- a/Carleson/Classical/ClassicalCarleson.lean
+++ b/Carleson/Classical/ClassicalCarleson.lean
@@ -214,7 +214,7 @@ theorem carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Perio
     intro x
     conv => pattern S_ _ _ _; rw [partialFourierSum_periodic]
     conv => pattern f _; rw [periodic_f]
-  apply MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict MeasureTheory.Ico_ae_eq_Icc.symm
+  apply ae_restrict_of_ae_eq_of_ae_restrict Ico_ae_eq_Icc.symm
   rw [zero_add]
 
   -- Show a.e. convergence on [0,2π]
diff --git a/Carleson/Classical/ControlApproximationEffect.lean b/Carleson/Classical/ControlApproximationEffect.lean
index 8668996d..7fbf077e 100644
--- a/Carleson/Classical/ControlApproximationEffect.lean
+++ b/Carleson/Classical/ControlApproximationEffect.lean
@@ -17,10 +17,11 @@ noncomputable section
 local notation "T" => carlesonOperatorReal K
 local notation "S_" => partialFourierSum
 
+open MeasureTheory
 
 
 /- TODO: might be generalized. -/
-lemma ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {f g : X → ENNReal} {E : Set X} (hE : MeasurableSet E)
+lemma ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : Measure X) {f g : X → ENNReal} {E : Set X} (hE : MeasurableSet E)
     (hf : Measurable f) (hg : Measurable g) {a : ENNReal} (h : ∀ x ∈ E, a ≤ f x + g x) :
     ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ (∀ x ∈ E', a / 2 ≤ g x)) := by
   set Ef := E ∩ f⁻¹' (Set.Ici (a / 2)) with Ef_def
@@ -52,7 +53,7 @@ lemma ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : MeasureTheory.Me
       gcongr
     _ ≤ 2 * (μ Ef + μ Eg) := by
       gcongr
-      exact MeasureTheory.measure_union_le _ _
+      exact measure_union_le _ _
     _ = 2 * μ Ef + 2 * μ Eg := by ring
     _ < μ E + μ E := by
       gcongr
@@ -147,18 +148,18 @@ lemma le_iSup_of_tendsto {α β} [TopologicalSpace α] [CompleteLinearOrder α]
   rcases this.exists with ⟨x, hx⟩
   exact lt_of_lt_of_le hx (le_iSup _ _)
 
-lemma integrable_annulus {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {r : ℝ} (r_nonneg : 0 ≤ r) (rle1 : r < 1) :
-    MeasureTheory.Integrable (fun x ↦ f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1}) := by
-  rw [← MeasureTheory.IntegrableOn, annulus_real_eq r_nonneg]
-  apply MeasureTheory.IntegrableOn.union <;>
+lemma integrable_annulus {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-Real.pi) (3 * Real.pi)) {r : ℝ} (r_nonneg : 0 ≤ r) (rle1 : r < 1) :
+    Integrable (fun x ↦ f x) (volume.restrict {y | dist x y ∈ Set.Ioo r 1}) := by
+  rw [← IntegrableOn, annulus_real_eq r_nonneg]
+  apply IntegrableOn.union <;>
   · rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith)]
     apply hf.mono_set
     rw [Set.uIcc_of_le (by linarith), Set.uIcc_of_le (by linarith [Real.pi_pos])]
     intro y hy
     constructor <;> linarith [hx.1, hx.2, hy.1, hy.2, Real.two_le_pi]
 
-lemma intervalIntegrable_mul_dirichletKernel' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
-    IntervalIntegrable (fun y ↦ f y * dirichletKernel' N (x - y)) MeasureTheory.volume (x - Real.pi) (x + Real.pi) := by
+lemma intervalIntegrable_mul_dirichletKernel' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
+    IntervalIntegrable (fun y ↦ f y * dirichletKernel' N (x - y)) volume (x - Real.pi) (x + Real.pi) := by
   apply (hf.mono_set _).mul_bdd (dirichletKernel'_measurable.comp (measurable_id.const_sub _)).aestronglyMeasurable
   · use (2 * N + 1)
     intro y
@@ -167,8 +168,8 @@ lemma intervalIntegrable_mul_dirichletKernel' {x : ℝ} (hx : x ∈ Set.Icc 0 (2
     apply Set.Icc_subset_Icc
     all_goals linarith [hx.1, hx.2, Real.pi_pos]
 
-lemma intervalIntegrable_mul_dirichletKernel'_max {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
-    IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) MeasureTheory.volume (x - Real.pi) (x + Real.pi) := by
+lemma intervalIntegrable_mul_dirichletKernel'_max {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
+    IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) volume (x - Real.pi) (x + Real.pi) := by
   conv => pattern ((f _) * _); rw [← mul_assoc]
   apply intervalIntegrable_mul_dirichletKernel' hx (IntervalIntegrable.mul_bdd hf (Complex.measurable_ofReal.comp ((Measurable.const_sub (_root_.continuous_abs.measurable.comp (measurable_id.const_sub _)) _).max measurable_const)).aestronglyMeasurable _)
   use 1
@@ -177,20 +178,20 @@ lemma intervalIntegrable_mul_dirichletKernel'_max {x : ℝ} (hx : x ∈ Set.Icc
   rw [_root_.abs_of_nonneg (le_max_right _ _)]
   simp
 
-lemma intervalIntegrable_mul_dirichletKernel'_max' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
-    IntervalIntegrable (fun y ↦ f y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) MeasureTheory.volume (x - Real.pi) (x + Real.pi) := by
+lemma intervalIntegrable_mul_dirichletKernel'_max' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
+    IntervalIntegrable (fun y ↦ f y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) volume (x - Real.pi) (x + Real.pi) := by
   conv => pattern ((f _) * _); rw [mul_sub]
   exact (intervalIntegrable_mul_dirichletKernel' hx hf).sub (intervalIntegrable_mul_dirichletKernel'_max hx hf)
 
-lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) :
+lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) :
       ∫ (y : ℝ) in x - Real.pi..x + Real.pi,
         g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))
     = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1},
         g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by
   calc _
     _ = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 Real.pi}, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by
-      rw [annulus_real_eq (le_refl 0), MeasureTheory.integral_union (by simp) measurableSet_Ioo, ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← MeasureTheory.integral_union (Set.disjoint_of_subset_right Set.Ioo_subset_Ioc_self (by simp)) measurableSet_Ioo,
-        intervalIntegral.integral_of_le (by linarith [Real.pi_pos]), MeasureTheory.integral_Ioc_eq_integral_Ioo,
+      rw [annulus_real_eq (le_refl 0), integral_union (by simp) measurableSet_Ioo, ← integral_Ioc_eq_integral_Ioo, ← integral_union (Set.disjoint_of_subset_right Set.Ioo_subset_Ioc_self (by simp)) measurableSet_Ioo,
+        intervalIntegral.integral_of_le (by linarith [Real.pi_pos]), integral_Ioc_eq_integral_Ioo,
         sub_zero, add_zero, Set.Ioc_union_Ioo_eq_Ioo (by linarith [Real.pi_pos]) (by linarith [Real.pi_pos])]
       --TODO: Many similar goals => improve this further?
       · rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith [Real.pi_pos])]
@@ -205,7 +206,7 @@ lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g MeasureT
       · apply Set.Icc_subset_Icc_right (by linarith [Real.pi_pos])
       · apply Set.Icc_subset_Icc_left (by linarith [Real.pi_pos])
     _ = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by
-      rw [←MeasureTheory.integral_indicator annulus_measurableSet, ←MeasureTheory.integral_indicator annulus_measurableSet]
+      rw [←integral_indicator annulus_measurableSet, ←integral_indicator annulus_measurableSet]
       congr with y
       rw [Set.indicator_apply, Set.indicator_apply, Dirichlet_Hilbert_eq]
       split_ifs with h₀ h₁ h₂
@@ -223,9 +224,9 @@ lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g MeasureT
         exact le_trans' (h₀ h₂.1) (by linarith [Real.two_le_pi])
       · trivial
 
-lemma intervalIntegrable_mul_dirichletKernel'_specific {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
-    MeasureTheory.IntegrableOn (fun y ↦ f y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) {y | dist x y ∈ Set.Ioo 0 1} MeasureTheory.volume := by
-  have : IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) MeasureTheory.volume (x - Real.pi) (x + Real.pi) := intervalIntegrable_mul_dirichletKernel'_max hx hf
+lemma intervalIntegrable_mul_dirichletKernel'_specific {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
+    IntegrableOn (fun y ↦ f y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) {y | dist x y ∈ Set.Ioo 0 1} volume := by
+  have : IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) volume (x - Real.pi) (x + Real.pi) := intervalIntegrable_mul_dirichletKernel'_max hx hf
   rw [intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith [Real.pi_pos])] at this
   apply this.mono_set
   intro y hy
@@ -233,7 +234,7 @@ lemma intervalIntegrable_mul_dirichletKernel'_specific {x : ℝ} (hx : x ∈ Set
   rcases hy with h | h <;> constructor <;> linarith [h.1, h.2, hx.1, hx.2, Real.two_le_pi]
 
 
-lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) :
+lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) :
     ‖∫ (y : ℝ) in x - Real.pi..x + Real.pi, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖₊
     ≤ T g x + T (conj ∘ g) x := by
   rw [domain_reformulation hg hx]
@@ -261,7 +262,7 @@ lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g Measu
       linarith
   have : Tendsto (fun i => ∫ y in s i, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
           atTop (𝓝 (∫ y in ⋃ n, s n, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))) := by
-    apply MeasureTheory.tendsto_setIntegral_of_monotone
+    apply tendsto_setIntegral_of_monotone
     · intro n
       exact annulus_measurableSet
     · intro n m nlem
@@ -340,17 +341,17 @@ lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g Measu
                 rw [one_mul, mul_one, ← Real.dist_eq]
                 gcongr
           have integrable₁ := (integrable_annulus hx hg rpos.le rle1)
-          rw [MeasureTheory.integral_add]
+          rw [integral_add]
           · conv => pattern ((g _) * _); rw [mul_comm]
-            apply MeasureTheory.Integrable.bdd_mul' integrable₁ measurable₁.aestronglyMeasurable
-            · rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
+            apply Integrable.bdd_mul' integrable₁ measurable₁.aestronglyMeasurable
+            · rw [ae_restrict_iff' annulus_measurableSet]
               apply Eventually.of_forall
               exact fun _ hy ↦ boundedness₁ hy.1.le
           · conv => pattern ((g _) * _); rw [mul_comm]
-            apply MeasureTheory.Integrable.bdd_mul' integrable₁
+            apply Integrable.bdd_mul' integrable₁
             · apply Measurable.aestronglyMeasurable
               exact continuous_star.measurable.comp measurable₁
-            · rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
+            · rw [ae_restrict_iff' annulus_measurableSet]
               apply Eventually.of_forall
               intro y hy
               rw [RCLike.norm_conj]
@@ -373,7 +374,7 @@ lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g Measu
           push_cast
           norm_cast
           congr 1 <;>
-          · rw [MeasureTheory.integral_mul_left, norm_mul, norm_eq_abs, mul_comm I, abs_exp_ofReal_mul_I, one_mul]
+          · rw [integral_mul_left, norm_mul, norm_eq_abs, mul_comm I, abs_exp_ofReal_mul_I, one_mul]
     _ ≤ T g x + T (conj ∘ g) x := by
       simp_rw [carlesonOperatorReal]
       apply iSup₂_le
@@ -390,7 +391,7 @@ lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measu
     {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) :
     ‖S_ N g x‖₊
       ≤ (T g x + T (conj ∘ g) x) / (ENNReal.ofReal (2 * Real.pi)) + ENNReal.ofReal (Real.pi * δ) := by
-  have intervalIntegrable_g : IntervalIntegrable g MeasureTheory.volume (-Real.pi) (3 * Real.pi) := intervalIntegrable_of_bdd measurable_g bound_g
+  have intervalIntegrable_g : IntervalIntegrable g volume (-Real.pi) (3 * Real.pi) := intervalIntegrable_of_bdd measurable_g bound_g
   have decomposition : S_ N g x
       = (  (∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi),
               g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
@@ -459,33 +460,33 @@ end section
 lemma rcarleson_exceptional_set_estimate {δ : ℝ} (δpos : 0 < δ) {f : ℝ → ℂ} (hmf : Measurable f)
     {F : Set ℝ} (measurableSetF : MeasurableSet F) (hf : ∀ x, ‖f x‖ ≤ δ * F.indicator 1 x)
     {E : Set ℝ} (measurableSetE : MeasurableSet E) {ε : ENNReal} (hE : ∀ x ∈ E, ε ≤ T f x) :
-      ε * MeasureTheory.volume E ≤ ENNReal.ofReal (δ * C10_0_1 4 2) * MeasureTheory.volume F ^ (2 : ℝ)⁻¹ * MeasureTheory.volume E ^ (2 : ℝ)⁻¹ := by
-  calc ε * MeasureTheory.volume E
+      ε * volume E ≤ ENNReal.ofReal (δ * C10_0_1 4 2) * volume F ^ (2 : ℝ)⁻¹ * volume E ^ (2 : ℝ)⁻¹ := by
+  calc ε * volume E
     _ = ∫⁻ _ in E, ε := by
       symm
-      apply MeasureTheory.setLIntegral_const
+      apply setLIntegral_const
     _ ≤ ∫⁻ x in E, T f x := by
-      apply MeasureTheory.setLIntegral_mono' measurableSetE hE
+      apply setLIntegral_mono' measurableSetE hE
     _ = ENNReal.ofReal δ * ∫⁻ x in E, T (fun x ↦ (1 / δ) * f x) x := by
-      rw [← MeasureTheory.lintegral_const_mul']
+      rw [← lintegral_const_mul']
       congr with x
       rw [carlesonOperatorReal_mul δpos]
       congr
       exact ENNReal.ofReal_ne_top
-    _ ≤ ENNReal.ofReal δ * (ENNReal.ofReal (C10_0_1 4 2) * (MeasureTheory.volume E) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹) := by
+    _ ≤ ENNReal.ofReal δ * (ENNReal.ofReal (C10_0_1 4 2) * (volume E) ^ (2 : ℝ)⁻¹ * (volume F) ^ (2 : ℝ)⁻¹) := by
       gcongr
       apply rcarleson measurableSetF measurableSetE _ (by fun_prop)
       intro x
       simp
       rw [_root_.abs_of_nonneg δpos.le, inv_mul_le_iff δpos]
       exact hf x
-    _ = ENNReal.ofReal (δ * C10_0_1 4 2) * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume E) ^ (2 : ℝ)⁻¹ := by
+    _ = ENNReal.ofReal (δ * C10_0_1 4 2) * (volume F) ^ (2 : ℝ)⁻¹ * (volume E) ^ (2 : ℝ)⁻¹ := by
       rw [ENNReal.ofReal_mul δpos.le]
       ring
 
 lemma rcarleson_exceptional_set_estimate_specific {δ : ℝ} (δpos : 0 < δ) {f : ℝ → ℂ} (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ δ)
     {E : Set ℝ} (measurableSetE : MeasurableSet E) (E_subset : E ⊆ Set.Icc 0 (2 * Real.pi)) {ε : ENNReal} (hE : ∀ x ∈ E, ε ≤ T f x) :
-      ε * MeasureTheory.volume E ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (2 * Real.pi + 2) ^ (2 : ℝ)⁻¹) * MeasureTheory.volume E ^ (2 : ℝ)⁻¹ := by
+      ε * volume E ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (2 * Real.pi + 2) ^ (2 : ℝ)⁻¹) * volume E ^ (2 : ℝ)⁻¹ := by
   rw [ENNReal.ofReal_mul (by apply mul_nonneg δpos.le (C10_0_1_pos one_lt_two).le), ← ENNReal.ofReal_rpow_of_pos (by linarith [Real.pi_pos])]
   set F := (Set.Ioo (0 - 1) (2 * Real.pi + 1))
   set h := F.indicator f with hdef
@@ -535,7 +536,7 @@ lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤
 /- This is Lemma 11.6.4 (partial Fourier sums of small) in the blueprint.-/
 lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ : 0 < δ)
     {h : ℝ → ℂ} (h_measurable : Measurable h) (h_periodic : h.Periodic (2 * Real.pi)) (h_bound : ∀ x, ‖h x‖ ≤ δ ) :
-    ∃ E ⊆ Set.Icc 0 (2 * Real.pi), MeasurableSet E ∧ MeasureTheory.volume.real E ≤ ε ∧ ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
+    ∃ E ⊆ Set.Icc 0 (2 * Real.pi), MeasurableSet E ∧ volume.real E ≤ ε ∧ ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
       ∀ N, ‖S_ N h x‖ ≤ C_control_approximation_effect ε * δ := by
   set ε' := C_control_approximation_effect ε * δ with ε'def
   set E := {x ∈ Set.Icc 0 (2 * Real.pi) | ∃ N, ε' < abs (S_ N h x)} with Edef
@@ -596,28 +597,28 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
         · rw [← ENNReal.ofReal_mul Real.two_pi_pos.le]
           ring_nf
   --TODO: align this with paper version
-  have Evolume : MeasureTheory.volume E < ⊤ := by
-    calc MeasureTheory.volume E
-      _ ≤ MeasureTheory.volume (Set.Icc 0 (2 * Real.pi)) := by
-        apply MeasureTheory.measure_mono
+  have Evolume : volume E < ⊤ := by
+    calc volume E
+      _ ≤ volume (Set.Icc 0 (2 * Real.pi)) := by
+        apply measure_mono
         rw [E_eq]
         apply Set.inter_subset_left
       _ = ENNReal.ofReal (2 * Real.pi) := by
         rw [Real.volume_Icc, sub_zero]
       _ < ⊤ := ENNReal.ofReal_lt_top
-  obtain ⟨E', E'subset, measurableSetE', E'measure, h⟩ := ENNReal.le_on_subset MeasureTheory.volume measurableSetE (carlesonOperatorReal_measurable h_measurable h_bound) (carlesonOperatorReal_measurable (continuous_star.measurable.comp h_measurable) conj_h_bound) le_operator_add
-  have E'volume : MeasureTheory.volume E' < ⊤ := lt_of_le_of_lt (MeasureTheory.measure_mono E'subset) Evolume
-  have E'volume_bound: ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E' ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (MeasureTheory.volume E') ^ (2 : ℝ)⁻¹ := by
-    calc ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E'
-    _ = ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 * MeasureTheory.volume E' := by
+  obtain ⟨E', E'subset, measurableSetE', E'measure, h⟩ := ENNReal.le_on_subset volume measurableSetE (carlesonOperatorReal_measurable h_measurable h_bound) (carlesonOperatorReal_measurable (continuous_star.measurable.comp h_measurable) conj_h_bound) le_operator_add
+  have E'volume : volume E' < ⊤ := lt_of_le_of_lt (measure_mono E'subset) Evolume
+  have E'volume_bound: ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * volume E' ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
+    calc ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * volume E'
+    _ = ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 * volume E' := by
       rw [← ENNReal.ofReal_ofNat, ← ENNReal.ofReal_div_of_pos (by norm_num)]
       ring_nf
-    _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (2 * Real.pi + 2) ^ (2 : ℝ)⁻¹) * (MeasureTheory.volume E') ^ (2 : ℝ)⁻¹ := by
+    _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (2 * Real.pi + 2) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
       rcases h with hE' | hE'
       · exact rcarleson_exceptional_set_estimate_specific hδ h_measurable h_bound measurableSetE' (E'subset.trans Esubset) hE'
       · refine rcarleson_exceptional_set_estimate_specific hδ ?_ conj_h_bound measurableSetE' (E'subset.trans Esubset) hE'
         exact ContinuousStar.continuous_star.measurable.comp h_measurable
-    _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (MeasureTheory.volume E') ^ (2 : ℝ)⁻¹ := by
+    _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
       gcongr
       · exact mul_nonneg hδ.le (C10_0_1_pos one_lt_two).le
       · linarith [Real.two_le_pi]
@@ -625,27 +626,27 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
   have ε'_δ_expression_pos : 0 < Real.pi * (ε' - Real.pi * δ) := by
     rw [ε'def, C_control_approximation_effect_eq εpos.le, add_sub_cancel_right, mul_div_cancel₀ _ Real.pi_pos.ne.symm]
     exact mul_pos δ_mul_const_pos (Real.rpow_pos_of_pos (div_pos (by norm_num) εpos) _)
-  calc MeasureTheory.volume.real E
-    _ ≤ 2 * MeasureTheory.volume.real E' := by
+  calc volume.real E
+    _ ≤ 2 * volume.real E' := by
       --uses E'measure
-      rwa [MeasureTheory.measureReal_def, MeasureTheory.measureReal_def, ←@ENNReal.toReal_ofReal 2 (by norm_num),
+      rwa [measureReal_def, measureReal_def, ←@ENNReal.toReal_ofReal 2 (by norm_num),
         ←ENNReal.toReal_mul, ENNReal.toReal_le_toReal Evolume.ne, ENNReal.ofReal_ofNat]
       apply ENNReal.mul_ne_top ENNReal.ofReal_ne_top E'volume.ne
-    _ = 2 * MeasureTheory.volume.real E' ^ ((1 + -(2 : ℝ)⁻¹) * 2) := by
-      conv => lhs; rw [←Real.rpow_one (MeasureTheory.volume.real E')]
+    _ = 2 * volume.real E' ^ ((1 + -(2 : ℝ)⁻¹) * 2) := by
+      conv => lhs; rw [←Real.rpow_one (volume.real E')]
       norm_num
     _ ≤ 2 * (δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ / (Real.pi * (ε' - Real.pi * δ))) ^ (2 : ℝ) := by
-      rw [Real.rpow_mul MeasureTheory.measureReal_nonneg]
+      rw [Real.rpow_mul measureReal_nonneg]
       gcongr
-      rw [Real.rpow_add' MeasureTheory.measureReal_nonneg (by norm_num), Real.rpow_one, le_div_iff₀' ε'_δ_expression_pos, ← mul_assoc]
+      rw [Real.rpow_add' measureReal_nonneg (by norm_num), Real.rpow_one, le_div_iff₀' ε'_δ_expression_pos, ← mul_assoc]
       apply mul_le_of_nonneg_of_le_div δ_mul_const_pos.le
-      apply Real.rpow_nonneg MeasureTheory.measureReal_nonneg
-      rw[Real.rpow_neg MeasureTheory.measureReal_nonneg, div_inv_eq_mul]
-      rw [← ENNReal.ofReal_le_ofReal_iff, ENNReal.ofReal_mul ε'_δ_expression_pos.le, MeasureTheory.measureReal_def, ENNReal.ofReal_toReal E'volume.ne]
+      apply Real.rpow_nonneg measureReal_nonneg
+      rw[Real.rpow_neg measureReal_nonneg, div_inv_eq_mul]
+      rw [← ENNReal.ofReal_le_ofReal_iff, ENNReal.ofReal_mul ε'_δ_expression_pos.le, measureReal_def, ENNReal.ofReal_toReal E'volume.ne]
       apply le_trans E'volume_bound
       rw [ENNReal.ofReal_mul δ_mul_const_pos.le, ← ENNReal.ofReal_rpow_of_nonneg ENNReal.toReal_nonneg (by norm_num), ENNReal.ofReal_toReal E'volume.ne]
       apply mul_nonneg δ_mul_const_pos.le
-      apply Real.rpow_nonneg MeasureTheory.measureReal_nonneg
+      apply Real.rpow_nonneg measureReal_nonneg
     _ = ε := by
       --We have chosen ε' such that this works.
       rw [ε'def, C_control_approximation_effect_eq εpos.le, add_sub_cancel_right, mul_div_cancel₀ _ Real.pi_pos.ne.symm,
diff --git a/Carleson/Classical/DirichletKernel.lean b/Carleson/Classical/DirichletKernel.lean
index bb74b095..f5509df3 100644
--- a/Carleson/Classical/DirichletKernel.lean
+++ b/Carleson/Classical/DirichletKernel.lean
@@ -6,9 +6,7 @@ import Mathlib.Analysis.Fourier.AddCircle
 import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
 import Mathlib.Analysis.Convolution
 
-open BigOperators
-open Finset
-open Complex
+open BigOperators Finset Complex MeasureTheory
 
 noncomputable section
 
@@ -142,8 +140,8 @@ lemma dirichletKernel_eq_ae {N : ℕ} : ∀ᵐ (x : ℝ), dirichletKernel N x =
     simp only [I_ne_zero, or_false]
     norm_cast
     exact (h n).symm
-  rw [MeasureTheory.ae_iff]
-  apply MeasureTheory.measure_mono_null this
+  rw [ae_iff]
+  apply measure_mono_null this
   apply Set.Countable.measure_zero
   let f : ℤ → ℝ := fun n ↦ n * (2 * Real.pi)
   apply Set.countable_range f
@@ -170,7 +168,7 @@ lemma norm_dirichletKernel'_le {N : ℕ} {x : ℝ} : ‖dirichletKernel' N x‖
     linarith
 
 /-First part of lemma 11.1.8 (Dirichlet kernel) from the blueprint.-/
-lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) :
+lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f volume 0 (2 * Real.pi)) :
     partialFourierSum N f x = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel N (x - y)  := by
   calc partialFourierSum N f x
     _ = ∑ n in Icc (-(N : ℤ)) N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x := by
@@ -202,7 +200,7 @@ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x :
       field_simp
       rw [mul_sub, sub_eq_neg_add]
 
-lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) :
+lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f volume 0 (2 * Real.pi)) :
     partialFourierSum N f x = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel' N (x - y)  := by
   rw [partialFourierSum_eq_conv_dirichletKernel h]
   calc _
@@ -212,8 +210,8 @@ lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {N : ℕ} {x
       simp
     _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (x - 2 * Real.pi)..(x - 0), f (x - y) * dirichletKernel' N y := by
       congr 1
-      apply intervalIntegral.integral_congr_ae (MeasureTheory.ae_imp_of_ae_restrict
-        (MeasureTheory.ae_restrict_of_ae _))
+      apply intervalIntegral.integral_congr_ae (ae_imp_of_ae_restrict
+        (ae_restrict_of_ae _))
       have : {a | ¬f (x - a) * dirichletKernel N a = f (x - a) * dirichletKernel' N a} ⊆ {a | ¬dirichletKernel N a = dirichletKernel' N a} := by
         intro a ha
         contrapose! ha
@@ -221,7 +219,7 @@ lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {N : ℕ} {x
         intro h
         exfalso
         exact h ha
-      apply MeasureTheory.measure_mono_null this dirichletKernel_eq_ae
+      apply measure_mono_null this dirichletKernel_eq_ae
     _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel' N (x - y) := by
       congr 1
       rw [← intervalIntegral.integral_comp_sub_left]
diff --git a/Carleson/Classical/Helper.lean b/Carleson/Classical/Helper.lean
index ea00ce96..2b262db7 100644
--- a/Carleson/Classical/Helper.lean
+++ b/Carleson/Classical/Helper.lean
@@ -4,17 +4,18 @@
 import Carleson.ToMathlib.Misc
 import Mathlib.MeasureTheory.Integral.IntervalIntegral
 
+open MeasureTheory
 
-theorem Real.volume_uIoc {a b : ℝ} : MeasureTheory.volume (Set.uIoc a b) = ENNReal.ofReal |b - a| := by
+theorem Real.volume_uIoc {a b : ℝ} : volume (Set.uIoc a b) = ENNReal.ofReal |b - a| := by
   /- Cf. proof of Real.volume_interval-/
   rw [Set.uIoc, volume_Ioc, max_sub_min_eq_abs]
 
-lemma intervalIntegral.integral_conj' {μ : MeasureTheory.Measure ℝ} {𝕜 : Type} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ}:
+lemma intervalIntegral.integral_conj' {μ : Measure ℝ} {𝕜 : Type} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ}:
     ∫ x in a..b, (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ x in a..b, f x ∂μ) := by
   rw [intervalIntegral_eq_integral_uIoc, integral_conj, intervalIntegral_eq_integral_uIoc,
       RCLike.real_smul_eq_coe_mul, RCLike.real_smul_eq_coe_mul, map_mul, RCLike.conj_ofReal]
 
-lemma intervalIntegrable_of_bdd {a b : ℝ} {δ : ℝ} {g : ℝ → ℂ} (measurable_g : Measurable g) (bddg : ∀ x, ‖g x‖ ≤ δ) : IntervalIntegrable g MeasureTheory.volume a b := by
+lemma intervalIntegrable_of_bdd {a b : ℝ} {δ : ℝ} {g : ℝ → ℂ} (measurable_g : Measurable g) (bddg : ∀ x, ‖g x‖ ≤ δ) : IntervalIntegrable g volume a b := by
   apply @IntervalIntegrable.mono_fun' _ _ _ _ _ _ (fun _ ↦ δ)
   · exact intervalIntegrable_const
   · exact measurable_g.aestronglyMeasurable
@@ -23,20 +24,20 @@ lemma intervalIntegrable_of_bdd {a b : ℝ} {δ : ℝ} {g : ℝ → ℂ} (measur
     rw [Subtype.forall]
     exact fun x _ ↦ bddg x
 
-lemma IntervalIntegrable.bdd_mul {F : Type} [NormedDivisionRing F] {f g : ℝ → F} {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
-    (hg : IntervalIntegrable g μ a b) (hm : MeasureTheory.AEStronglyMeasurable f μ) (hfbdd : ∃ C, ∀ x, ‖f x‖ ≤ C) : IntervalIntegrable (fun x ↦ f x * g x) μ a b := by
-  rw [intervalIntegrable_iff, MeasureTheory.IntegrableOn]
-  apply MeasureTheory.Integrable.bdd_mul _ hm.restrict hfbdd
-  rwa [← MeasureTheory.IntegrableOn, ← intervalIntegrable_iff]
+lemma IntervalIntegrable.bdd_mul {F : Type} [NormedDivisionRing F] {f g : ℝ → F} {a b : ℝ} {μ : Measure ℝ}
+    (hg : IntervalIntegrable g μ a b) (hm : AEStronglyMeasurable f μ) (hfbdd : ∃ C, ∀ x, ‖f x‖ ≤ C) : IntervalIntegrable (fun x ↦ f x * g x) μ a b := by
+  rw [intervalIntegrable_iff, IntegrableOn]
+  apply Integrable.bdd_mul _ hm.restrict hfbdd
+  rwa [← IntegrableOn, ← intervalIntegrable_iff]
 
-lemma IntervalIntegrable.mul_bdd {F : Type} [NormedField F] {f g : ℝ → F} {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
-    (hf : IntervalIntegrable f μ a b) (hm : MeasureTheory.AEStronglyMeasurable g μ) (hgbdd : ∃ C, ∀ x, ‖g x‖ ≤ C) : IntervalIntegrable (fun x ↦ f x * g x) μ a b := by
+lemma IntervalIntegrable.mul_bdd {F : Type} [NormedField F] {f g : ℝ → F} {a b : ℝ} {μ : Measure ℝ}
+    (hf : IntervalIntegrable f μ a b) (hm : AEStronglyMeasurable g μ) (hgbdd : ∃ C, ∀ x, ‖g x‖ ≤ C) : IntervalIntegrable (fun x ↦ f x * g x) μ a b := by
   conv => pattern (fun x ↦ f x * g x); ext x; rw [mul_comm]
   exact hf.bdd_mul hm hgbdd
 
-lemma MeasureTheory.IntegrableOn.sub {α : Type} {β : Type} {m : MeasurableSpace α}
-    {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {s : Set α} {f g : α → β} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) : IntegrableOn (f - g) s μ := by
-  apply MeasureTheory.Integrable.sub <;> rwa [← IntegrableOn]
+lemma IntegrableOn.sub {α : Type} {β : Type} {m : MeasurableSpace α}
+    {μ : Measure α} [NormedAddCommGroup β] {s : Set α} {f g : α → β} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) : IntegrableOn (f - g) s μ := by
+  apply Integrable.sub <;> rwa [← IntegrableOn]
 
 
 lemma ConditionallyCompleteLattice.le_biSup {α : Type} [ConditionallyCompleteLinearOrder α] {ι : Type} [Nonempty ι]
diff --git a/Carleson/Classical/HilbertKernel.lean b/Carleson/Classical/HilbertKernel.lean
index 6be76458..80b83c08 100644
--- a/Carleson/Classical/HilbertKernel.lean
+++ b/Carleson/Classical/HilbertKernel.lean
@@ -8,7 +8,7 @@ import Mathlib.Tactic.FunProp
 
 noncomputable section
 
-open Complex ComplexConjugate
+open Complex ComplexConjugate MeasureTheory
 
 def k (x : ℝ) : ℂ := max (1 - |x|) 0 / (1 - exp (I * x))
 
@@ -145,11 +145,11 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧
         · exact f_deriv
         · exact f'_cont.intervalIntegrable
       _ = ‖∫ (t : ℝ) in Ι y' y, f' t‖ := intervalIntegral.norm_intervalIntegral_eq _ _ _ _
-      _ ≤ ∫ (t : ℝ) in Ι y' y, ‖f' t‖ := MeasureTheory.norm_integral_le_integral_norm _
+      _ ≤ ∫ (t : ℝ) in Ι y' y, ‖f' t‖ := norm_integral_le_integral_norm _
       _ ≤ ∫ (t : ℝ) in Ι y' y, 3 / ((y / 2) / 2) ^ 2 := by
-        apply MeasureTheory.setIntegral_mono_on
+        apply setIntegral_mono_on
         · exact f'_cont.norm.integrableOn_uIcc.mono_set Set.Ioc_subset_Icc_self
-        · apply MeasureTheory.integrableOn_const.mpr
+        · apply integrableOn_const.mpr
           rw [Real.volume_uIoc]
           right
           exact ENNReal.ofReal_lt_top
@@ -193,8 +193,8 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧
             · rw [abs_neg, le_abs]
               left
               rcases ht with ht | ht <;> linarith [ht.1]
-      _ = (MeasureTheory.volume (Ι y' y)).toReal * (3 / ((y / 2) / 2) ^ 2) :=
-        MeasureTheory.setIntegral_const _
+      _ = (volume (Ι y' y)).toReal * (3 / ((y / 2) / 2) ^ 2) :=
+        setIntegral_const _
       _ = |y - y'| * (3 / ((y / 2) / 2) ^ 2) := by
         rw [Real.volume_uIoc, ENNReal.toReal_ofReal (abs_nonneg (y - y'))]
       _ = (3 * (2 * 2) ^ 2) * (1 / y) * (|y - y'| / y) := by ring
diff --git a/Carleson/Classical/VanDerCorput.lean b/Carleson/Classical/VanDerCorput.lean
index 76cf0a5a..d53e9c6d 100644
--- a/Carleson/Classical/VanDerCorput.lean
+++ b/Carleson/Classical/VanDerCorput.lean
@@ -3,7 +3,7 @@ import Carleson.Classical.Basic
 
 noncomputable section
 
-open Complex
+open Complex MeasureTheory
 
 lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B K: NNReal}
     (h1 : LipschitzWith K ϕ) (h2 : ∀ x ∈ (Set.Ioo a b), ‖ϕ x‖ ≤ B) :
@@ -17,10 +17,10 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
       add_zero, inv_one, mul_one]
     calc ‖∫ (x : ℝ) in a..b, ϕ x‖
       _ = ‖∫ (x : ℝ) in Set.Ioo a b, ϕ x‖ := by
-        rw [intervalIntegral.integral_of_le, ← MeasureTheory.integral_Ioc_eq_integral_Ioo]
+        rw [intervalIntegral.integral_of_le, ← integral_Ioc_eq_integral_Ioo]
         linarith
-      _ ≤ B * (MeasureTheory.volume (Set.Ioo a b)).toReal := by
-        apply MeasureTheory.norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
+      _ ≤ B * (volume (Set.Ioo a b)).toReal := by
+        apply norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
         · exact fun x hx ↦ (h2 x hx)
         · exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
       _ = B * (b - a) := by rw [Real.volume_Ioo, ENNReal.toReal_ofReal (by linarith)]
@@ -64,10 +64,10 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
       apply mul_nonneg (by simp) (by linarith)
     calc _
       _ = ‖∫ (x : ℝ) in Set.Ioo a b, cexp (I * ↑n * ↑x) * ϕ x‖ := by
-        rw [intervalIntegral.integral_of_le, ← MeasureTheory.integral_Ioc_eq_integral_Ioo]
+        rw [intervalIntegral.integral_of_le, ← integral_Ioc_eq_integral_Ioo]
         linarith
-      _ ≤ B * (MeasureTheory.volume (Set.Ioo a b)).toReal := by
-        apply MeasureTheory.norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
+      _ ≤ B * (volume (Set.Ioo a b)).toReal := by
+        apply norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
         · intro x hx
           rw_mod_cast [norm_mul, mul_assoc, mul_comm I, Complex.norm_exp_ofReal_mul_I, one_mul]
           exact h2 x hx
@@ -168,20 +168,20 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
                  + ‖∫ (x : ℝ) in Set.Ioo (b - Real.pi / n) b, (I * n * (x + Real.pi / n)).exp * ϕ x‖) := by
       congr
       all_goals
-        rw [intervalIntegral.integral_of_le, ← MeasureTheory.integral_Ioc_eq_integral_Ioo]
+        rw [intervalIntegral.integral_of_le, ← integral_Ioc_eq_integral_Ioo]
         linarith
-    _ ≤ 1 / 2 * (  B * (MeasureTheory.volume (Set.Ioo a (a + Real.pi / n))).toReal
-                 + (K * Real.pi / n) * (MeasureTheory.volume (Set.Ioo (a + Real.pi / n) b)).toReal
-                 + B * (MeasureTheory.volume (Set.Ioo (b - Real.pi / n) b)).toReal) := by
+    _ ≤ 1 / 2 * (  B * (volume (Set.Ioo a (a + Real.pi / n))).toReal
+                 + (K * Real.pi / n) * (volume (Set.Ioo (a + Real.pi / n) b)).toReal
+                 + B * (volume (Set.Ioo (b - Real.pi / n) b)).toReal) := by
       gcongr
-      · apply MeasureTheory.norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
+      · apply norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
         · intro x hx
           rw [norm_mul, mul_assoc, mul_comm I]
           rw_mod_cast [Complex.norm_exp_ofReal_mul_I, one_mul]
           apply h2
           constructor <;> linarith [hx.1, hx.2]
         · exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
-      · apply MeasureTheory.norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
+      · apply norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
         · intro x _
           rw [norm_mul, mul_assoc, mul_comm I]
           rw_mod_cast [Complex.norm_exp_ofReal_mul_I, one_mul, ← dist_eq_norm]
@@ -191,7 +191,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
           apply le_of_eq
           ring
         · exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
-      · apply MeasureTheory.norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
+      · apply norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
         · intro x hx
           rw [norm_mul, mul_assoc, mul_comm I]
           rw_mod_cast [Complex.norm_exp_ofReal_mul_I, one_mul]
diff --git a/Carleson/ForestOperator.lean b/Carleson/ForestOperator.lean
index 5271c674..00123a41 100644
--- a/Carleson/ForestOperator.lean
+++ b/Carleson/ForestOperator.lean
@@ -101,7 +101,7 @@ def r𝓑 (z : ℕ × Grid X) : ℝ := 2 ^ z.1 * D ^ s z.2
 /-- The constant used in `first_tree_pointwise`.
 Has value `10 * 2 ^ (105 * a ^ 3)` in the blueprint. -/
 -- Todo: define this recursively in terms of previous constants
-def C7_1_4 (a : ℝ) : ℝ≥0 := 10 * 2 ^ (105 * a ^ 3)
+def C7_1_4 (a : ℕ) : ℝ≥0 := 10 * 2 ^ (105 * (a : ℝ) ^ 3)
 
 /-- Lemma 7.1.4 -/
 lemma first_tree_pointwise (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx : x ∈ L) (hx' : x' ∈ L)
@@ -120,7 +120,7 @@ lemma second_tree_pointwise (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx
 /-- The constant used in `third_tree_pointwise`.
 Has value `2 ^ (151 * a ^ 3)` in the blueprint. -/
 -- Todo: define this recursively in terms of previous constants
-def C7_1_6 (a : ℝ) : ℝ≥0 := 2 ^ (151 * a ^ 3)
+def C7_1_6 (a : ℕ) : ℝ≥0 := 2 ^ (151 * (a : ℝ) ^ 3)
 
 /-- Lemma 7.1.6 -/
 lemma third_tree_pointwise (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx : x ∈ L) (hx' : x' ∈ L)
@@ -132,7 +132,7 @@ lemma third_tree_pointwise (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx
 /-- The constant used in `pointwise_tree_estimate`.
 Has value `2 ^ (151 * a ^ 3)` in the blueprint. -/
 -- Todo: define this recursively in terms of previous constants
-def C7_1_3 (a : ℝ) : ℝ≥0 := 2 ^ (151 * a ^ 3)
+def C7_1_3 (a : ℕ) : ℝ≥0 := 2 ^ (151 * (a : ℝ) ^ 3)
 
 /-- Lemma 7.1.3. -/
 lemma pointwise_tree_estimate (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx : x ∈ L) (hx' : x' ∈ L)
diff --git a/Carleson/RealInterpolation.lean b/Carleson/RealInterpolation.lean
index 97028f30..bd4058eb 100644
--- a/Carleson/RealInterpolation.lean
+++ b/Carleson/RealInterpolation.lean
@@ -24,7 +24,7 @@ import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
 -/
 noncomputable section
 
-open ENNReal Real Set
+open ENNReal Real Set MeasureTheory
 
 variable {p₀ q₀ p₁ q₁ p q : ℝ≥0∞} {t : ℝ}
 
@@ -1646,7 +1646,7 @@ lemma aestronglyMeasurable_trunc [MeasurableSpace E₁] [NormedAddCommGroup E₁
   rcases hf with ⟨g, ⟨wg1, wg2⟩⟩
   exists (trunc g t)
   constructor
-  · apply MeasureTheory.StronglyMeasurable.indicator (s := {x | ‖g x‖ ≤ t})
+  · apply StronglyMeasurable.indicator (s := {x | ‖g x‖ ≤ t})
     · exact wg1
     · apply StronglyMeasurable.measurableSet_le
       apply StronglyMeasurable.norm
@@ -1669,7 +1669,7 @@ lemma aestronglyMeasurable_trunc_compl [MeasurableSpace E₁] [NormedAddCommGrou
   exists (g - trunc g t)
   constructor
   · rw [trunc_compl_eq]
-    apply MeasureTheory.StronglyMeasurable.indicator (s := {x | t < ‖g x‖})
+    apply StronglyMeasurable.indicator (s := {x | t < ‖g x‖})
     · exact wg1
     · apply StronglyMeasurable.measurableSet_lt
       · exact stronglyMeasurable_const
@@ -1788,7 +1788,7 @@ lemma trnc_le_func {j : Bool} {f : α → E₁} {a : ℝ} {x : α}
 
 -- /-- The `t`-truncation of `f : α →ₘ[μ] E`. -/
 -- def AEEqFun.trunc (f : α →ₘ[μ] E) (t : ℝ) : α →ₘ[μ] E :=
---   AEEqFun.mk (MeasureTheory.trunc f t) (aestronglyMeasurable_trunc f.aestronglyMeasurable)
+--   AEEqFun.mk (trunc f t) (aestronglyMeasurable_trunc f.aestronglyMeasurable)
 
 -- /-- A set of measurable functions is closed under truncation. -/
 -- class IsClosedUnderTruncation (U : Set (α →ₘ[μ] E)) : Prop where
@@ -2572,8 +2572,8 @@ lemma representationLp {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞
 
 lemma aemeasurability_prod₁ {α : Type u_1} {β : Type u_3}
     [MeasurableSpace α] [MeasurableSpace β]
-    {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν]
-    [MeasureTheory.SFinite μ] ⦃f : α × β → ENNReal⦄
+    {μ : Measure α} {ν : Measure β} [SFinite ν]
+    [SFinite μ] ⦃f : α × β → ENNReal⦄
     (hf : AEMeasurable f (μ.prod ν)) :
     ∀ᵐ x : α ∂μ, AEMeasurable (f ∘ (Prod.mk x)) ν := by
   rcases hf with ⟨g, hg⟩
@@ -2582,8 +2582,8 @@ lemma aemeasurability_prod₁ {α : Type u_1} {β : Type u_3}
 
 lemma aemeasurability_prod₂ {α : Type u_1} {β : Type u_3}
     [MeasurableSpace α] [MeasurableSpace β]
-    {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν]
-    [MeasureTheory.SFinite μ] ⦃f : α × β → ENNReal⦄
+    {μ : Measure α} {ν : Measure β} [SFinite ν]
+    [SFinite μ] ⦃f : α × β → ENNReal⦄
     (hf : AEMeasurable f (μ.prod ν)) :
     ∀ᵐ y : β ∂ν, AEMeasurable (f ∘ (fun x ↦ Prod.mk x y)) μ := by
   have : AEMeasurable (f ∘ Prod.swap) (ν.prod μ) := by
@@ -2594,8 +2594,8 @@ lemma aemeasurability_prod₂ {α : Type u_1} {β : Type u_3}
 
 lemma aemeasurability_integral_component {α : Type u_1} {β : Type u_3}
     [MeasurableSpace α] [MeasurableSpace β]
-    {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν]
-    [MeasureTheory.SFinite μ] ⦃f : α × β → ENNReal⦄
+    {μ : Measure α} {ν : Measure β} [SFinite ν]
+    [SFinite μ] ⦃f : α × β → ENNReal⦄
     (hf : AEMeasurable f (μ.prod ν)) :
     AEMeasurable (fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ := by
   rcases hf with ⟨g, hg⟩
@@ -2608,8 +2608,8 @@ lemma aemeasurability_integral_component {α : Type u_1} {β : Type u_3}
 -- argument
 lemma lintegral_lintegral_pow_swap {α : Type u_1} {β : Type u_3} {p : ℝ} (hp : 1 ≤ p)
     [MeasurableSpace α] [MeasurableSpace β]
-    {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν]
-    [MeasureTheory.SigmaFinite μ] ⦃f : α → β → ENNReal⦄
+    {μ : Measure α} {ν : Measure β} [SFinite ν]
+    [SigmaFinite μ] ⦃f : α → β → ENNReal⦄
     (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) :
     (∫⁻ (x : α), (∫⁻ (y : β), f x y ∂ν) ^ p ∂μ) ^ p⁻¹ ≤
     ∫⁻ (y : β), (∫⁻ (x : α), (f x y) ^ p ∂μ) ^ p⁻¹ ∂ν := by
@@ -2658,8 +2658,8 @@ lemma lintegral_lintegral_pow_swap {α : Type u_1} {β : Type u_3} {p : ℝ} (hp
 
 lemma lintegral_lintegral_pow_swap_rpow {α : Type u_1} {β : Type u_3} {p : ℝ} (hp : p ≥ 1)
     [MeasurableSpace α] [MeasurableSpace β]
-    {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν]
-    [MeasureTheory.SigmaFinite μ] ⦃f : α → β → ENNReal⦄
+    {μ : Measure α} {ν : Measure β} [SFinite ν]
+    [SigmaFinite μ] ⦃f : α → β → ENNReal⦄
     (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) :
     (∫⁻ (x : α), (∫⁻ (y : β), f x y ∂ν) ^ p ∂μ) ≤
     (∫⁻ (y : β), (∫⁻ (x : α), (f x y) ^ p ∂μ) ^ p⁻¹ ∂ν) ^ p := by
@@ -3427,7 +3427,7 @@ lemma weaktype_estimate_trunc_top {C₁ : ℝ≥0} (hC₁ : C₁ > 0) {p p₁ q
         exact fun x ↦ trunc_le_func
       _ ≤ _ := by
         have : eLpNorm f p₁ μ = 0 := Trans.trans (eLpNorm_congr_ae
-            (eLpNormEssSup_eq_zero_iff.mp snorm_zero)) MeasureTheory.eLpNorm_zero
+            (eLpNormEssSup_eq_zero_iff.mp snorm_zero)) eLpNorm_zero
         simp only [this, mul_zero, zero_le]
     · have snorm_p_pos : eLpNorm f p μ ≠ 0 := by
         intro snorm_0
diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean
index f8471ae9..3d14826c 100644
--- a/Carleson/ToMathlib/Misc.lean
+++ b/Carleson/ToMathlib/Misc.lean
@@ -172,19 +172,19 @@ lemma lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ℝ≥0∞} (hc
 
 -- Named for consistency with `lintegral_add_left'`
 -- Maybe add laverage/laverage theorems for all the other lintegral_add statements?
-lemma laverage_add_left {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
+lemma laverage_add_left {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
     {f g : α → ENNReal} (hf : AEMeasurable f μ) :
     ⨍⁻ x, (f x + g x) ∂μ = ⨍⁻ x, f x ∂μ + ⨍⁻ x, g x ∂μ := by
   simp_rw [laverage_eq, ENNReal.div_add_div_same, lintegral_add_left' hf]
 
 -- Named for consistency with `lintegral_mono'`
-lemma laverage_mono {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
+lemma laverage_mono {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
     {f g : α → ENNReal} (h : ∀ x, f x ≤ g x) :
     ⨍⁻ x, f x ∂μ ≤ ⨍⁻ x, g x ∂μ := by
   simp_rw [laverage_eq]
   exact ENNReal.div_le_div_right (lintegral_mono h) (μ univ)
 
-lemma laverage_const_mul {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
+lemma laverage_const_mul {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
     {f : α → ENNReal} {c : ENNReal} (hc : c ≠ ⊤) :
     c * ⨍⁻ x, f x ∂μ = ⨍⁻ x, c * f x ∂μ := by
   simp_rw [laverage_eq, ← mul_div_assoc c, lintegral_const_mul' c f hc]
@@ -193,13 +193,13 @@ lemma laverage_const_mul {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureThe
 
 -- Named for consistency with `lintegral_add_left'`
 -- Maybe add laverage/setLaverage theorems for all the other lintegral_add statements?
-lemma setLaverage_add_left' {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
+lemma setLaverage_add_left' {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
     {s : Set α} {f g : α → ENNReal} (hf : AEMeasurable f μ) :
     ⨍⁻ x in s, (f x + g x) ∂μ = ⨍⁻ x in s, f x ∂μ + ⨍⁻ x in s, g x ∂μ := by
   simp_rw [setLaverage_eq, ENNReal.div_add_div_same, lintegral_add_left' hf.restrict]
 
 -- Named for consistency with `setLintegral_mono'`
-lemma setLaverage_mono' {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
+lemma setLaverage_mono' {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
     {s : Set α} (hs : MeasurableSet s) {f g : α → ENNReal} (h : ∀ x ∈ s, f x ≤ g x) :
     ⨍⁻ x in s, f x ∂μ ≤ ⨍⁻ x in s, g x ∂μ := by
   simp_rw [setLaverage_eq]
diff --git a/Carleson/WeakType.lean b/Carleson/WeakType.lean
index 851b5a5f..b1ab11e4 100644
--- a/Carleson/WeakType.lean
+++ b/Carleson/WeakType.lean
@@ -154,7 +154,7 @@ lemma tendsto_measure_iUnion_distribution (t₀ : ℝ≥0∞) :
     Filter.Tendsto (⇑μ ∘ (fun n : ℕ ↦ {x | t₀ + (↑n)⁻¹ < ‖f x‖₊}))
       Filter.atTop (nhds (μ ({x | t₀ < ‖f x‖₊}))) := by
   rw [← approx_above_superset]
-  apply MeasureTheory.tendsto_measure_iUnion
+  apply tendsto_measure_iUnion
   intro a b h x h₁
   calc
     _ ≤ t₀ + (↑a)⁻¹ := by gcongr
@@ -267,7 +267,7 @@ lemma lintegral_norm_pow_eq_distribution {p : ℝ} (hp : 0 < p) :
     ∫⁻ x, ‖f x‖₊ ^ p ∂μ =
     ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (p * t ^ (p - 1)) * distribution f (.ofReal t) μ := by
   have h2p : 0 ≤ p := hp.le
-  have := MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul μ (f := fun x ↦ ‖f x‖)
+  have := lintegral_rpow_eq_lintegral_meas_lt_mul μ (f := fun x ↦ ‖f x‖)
     (Eventually.of_forall fun x ↦ norm_nonneg _) hf.norm hp
   simp [*, ENNReal.coe_rpow_of_nonneg, ← ENNReal.ofReal_rpow_of_nonneg, ← ofReal_norm_eq_coe_nnnorm,
     ofReal_mul, ← lintegral_const_mul', ← mul_assoc, mul_comm (μ _), distribution]
@@ -283,7 +283,7 @@ lemma eLpNorm_pow_eq_distribution {p : ℝ≥0} (hp : 0 < p) :
   have h2p : 0 < (p : ℝ) := hp
   have h3p : (p : ℝ) ≠ 0 := h2p.ne'
   have h4p : 0 ≤ (p : ℝ) := zero_le_coe
-  simp_rw [MeasureTheory.eLpNorm_nnreal_eq_eLpNorm' hp.ne', eLpNorm', one_div, ← ENNReal.rpow_mul,
+  simp_rw [eLpNorm_nnreal_eq_eLpNorm' hp.ne', eLpNorm', one_div, ← ENNReal.rpow_mul,
     inv_mul_cancel₀ h3p, ENNReal.rpow_one, lintegral_norm_pow_eq_distribution hf h2p,
     ENNReal.ofReal_mul h4p, ofReal_coe_nnreal]
 
diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex
index c8ea9503..11c2328d 100644
--- a/blueprint/src/chapter/main.tex
+++ b/blueprint/src/chapter/main.tex
@@ -4194,6 +4194,8 @@ \section{The pointwise tree estimate}
 $$
 \begin{lemma}[convex scales]
 \label{convex-scales}
+\leanok
+\lean{TileStructure.Forest.convex_scales}
     For each $\fu \in \fU$, we have
     $$
         \sigma(\fu, x) = \mathbb{Z} \cap [\underline{\sigma} (\fu, x), \overline{\sigma} (\fu, x)]\,.
@@ -4222,6 +4224,9 @@ \section{The pointwise tree estimate}
 
 \begin{lemma}[dyadic partitions]
     \label{dyadic-partitions}
+    \leanok
+    \lean{TileStructure.Forest.biUnion_𝓙, TileStructure.Forest.pairwiseDisjoint_𝓙,
+    TileStructure.Forest.biUnion_𝓛, TileStructure.Forest.pairwiseDisjoint_𝓛}
     For each $\mathfrak{S} \subset \fP$, we have
     \begin{equation}
         \label{eq-J-partition}
@@ -4271,6 +4276,8 @@ \section{The pointwise tree estimate}
 
 \begin{lemma}[pointwise tree estimate]
     \label{pointwise-tree-estimate}
+    \leanok
+    \lean{TileStructure.Forest.pointwise_tree_estimate}
     \uses{first-tree-pointwise,second-tree-pointwise,third-tree-pointwise}
     Let $\fu \in \fU$ and $L \in \mathcal{L}(\fT(\fu))$. Let $x, x' \in L$.
     Then for all bounded functions $f$ with bounded support
@@ -4312,6 +4319,8 @@ \section{The pointwise tree estimate}
 
 \begin{lemma}[first tree pointwise]
     \label{first-tree-pointwise}
+    \leanok
+    \lean{TileStructure.Forest.first_tree_pointwise}
     \uses{convex-scales}
     For all $\fu \in \fU$, all $L \in \mathcal{L}(\fT(\fu))$, all $x, x' \in L$ and all bounded $f$ with bounded support, we have
     $$
@@ -4371,6 +4380,8 @@ \section{The pointwise tree estimate}
 
 \begin{lemma}[second tree pointwise]
     \label{second-tree-pointwise}
+    \leanok
+    \lean{TileStructure.Forest.second_tree_pointwise}
     For all $\fu \in \fU$, all $L \in \mathcal{L}(\fT(\fu))$, all $x, x' \in L$ and all bounded $f$ with bounded support, we have
     $$
          \Bigg| \sum_{s \in \sigma(\fu, x)} \int K_s(x,y) P_{\mathcal{J}(\fT(\fu))} f(y) \, \mathrm{d}\mu(y) \Bigg| \le T_{\mathcal{N}}^{\fcc(\fu)} P_{\mathcal{J}(\fT(\fu))} f(x')\,.
@@ -4401,6 +4412,8 @@ \section{The pointwise tree estimate}
 
 \begin{lemma}[third tree pointwise]
     \label{third-tree-pointwise}
+    \leanok
+    \lean{TileStructure.Forest.third_tree_pointwise}
     For all $\fu \in \fU$, all $L \in \mathcal{L}(\fT(\fu))$, all $x, x' \in L$ and all bounded $f$ with bounded support, we have
     \begin{equation*}
         \Bigg| \sum_{s \in \sigma(\fu, x)} \int K_s(x,y) (f(y) - P_{\mathcal{J}(\fT(\fu))} f(y)) \, \mathrm{d}\mu(y) \Bigg|