chore/perf: miscellaneous small tweaks (#232)

Some tweaks salvaged from #229, and some small performance improvements
I found.

Carleson/Antichain/AntichainTileCount.lean

@@ -98,7 +98,7 @@ lemma tile_reach (ha : 4 ≤ a) {ϑ : Θ X} {N : ℕ} {p p' : 𝔓 X} (hp : dist
           gcongr --uses h12
           have : (2 : ℝ)^a = 2^(a : ℤ) := by rw [@zpow_natCast]
           ring_nf
-          nlinarith
+          nlinarith only
       _ = (4 * 2 ^ (2 - 5 * (a : ℤ)  ^ 2 - 2 * ↑a)) * (D * D ^ 𝔰 p) := by ring
       _ ≤ 4 * 2 ^ (2 - 5 * (a : ℤ)  ^ 2 - 2 * ↑a) * D ^ 𝔰 p' := by
         have h1D : 1 ≤ (D : ℝ) := one_le_D

Carleson/Classical/Approximation.lean

@@ -154,7 +154,7 @@ lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [Continuo
   · simp
   · have : Icc (- Int.ofNat (N.succ)) (N.succ) = insert (↑(N.succ)) (insert (-Int.ofNat (N.succ)) (Icc (-Int.ofNat N) N)) := by
       rw [←Ico_insert_right, ←Ioo_insert_left]
-      · congr with n
+      · congr 2 with n
         simp only [Int.ofNat_eq_coe, mem_Ioo, mem_Icc]
         push_cast
         rw [Int.lt_add_one_iff, neg_add, ←sub_eq_add_neg, Int.sub_one_lt_iff]
@@ -171,7 +171,6 @@ lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [Continuo
     · norm_num
       linarith
 
-
 lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : f.Periodic (2 * π))
     (fdiff : ContDiff ℝ 2 f) {ε : ℝ} (εpos : ε > 0) :
     ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * π), ‖f x - S_ N f x‖ ≤ ε := by

Carleson/Classical/Basic.lean

@@ -23,17 +23,20 @@ def AddCircle.partialFourierSum' {T : ℝ} [hT : Fact (0 < T)] (N : ℕ) (f : Ad
 
 local notation "S_" => partialFourierSum
 
-
 @[simp]
 lemma fourierCoeffOn_mul {a b : ℝ} {hab : a < b} {f: ℝ → ℂ} {c : ℂ} {n : ℤ} :
   fourierCoeffOn hab (fun x ↦ c * f x) n = c * (fourierCoeffOn hab f n):= by
-  simp [fourierCoeffOn_eq_integral, mul_assoc, mul_comm]
+  simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
+    fourier_coe_apply', mul_comm, Complex.ofReal_sub, smul_eq_mul, mul_assoc,
+    intervalIntegral.integral_const_mul, Complex.real_smul, Complex.ofReal_inv]
   ring
 
 @[simp]
 lemma fourierCoeffOn_neg {a b : ℝ} {hab : a < b} {f: ℝ → ℂ} {n : ℤ} :
   fourierCoeffOn hab (-f) n = - (fourierCoeffOn hab f n):= by
-  simp [fourierCoeffOn_eq_integral]
+  simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
+    fourier_coe_apply', Complex.ofReal_sub, Pi.neg_apply, smul_eq_mul, mul_neg,
+    intervalIntegral.integral_neg, smul_neg, Complex.real_smul, Complex.ofReal_inv]
 
 @[simp]
 lemma fourierCoeffOn_add {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}
@@ -45,8 +48,10 @@ lemma fourierCoeffOn_add {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}
     Complex.ofReal_inv]
   rw [← mul_add, ← intervalIntegral.integral_add]
   · ring_nf
-    apply hf.continuousOn_mul (Continuous.continuousOn _); continuity
-  · apply hg.continuousOn_mul (Continuous.continuousOn _); continuity
+    apply hf.continuousOn_mul (Continuous.continuousOn _)
+    exact Complex.continuous_conj.comp' (by fun_prop)
+  · apply hg.continuousOn_mul (Continuous.continuousOn _)
+    exact Complex.continuous_conj.comp' (by fun_prop)
 
 @[simp]
 lemma fourierCoeffOn_sub {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}
@@ -61,21 +66,24 @@ lemma partialFourierSum_add {f g : ℝ → ℂ} {N : ℕ}
     (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * π)) :
   S_ N (f + g) = S_ N f + S_ N g := by
   ext x
-  simp [partialFourierSum, sum_add_distrib, fourierCoeffOn_add hf hg, add_mul]
+  simp only [partialFourierSum, fourierCoeffOn_add hf hg, fourier_apply, fourier_coe_apply',
+    Complex.ofReal_mul, Complex.ofReal_ofNat, add_mul, sum_add_distrib, Pi.add_apply]
 
 @[simp]
 lemma partialFourierSum_sub {f g : ℝ → ℂ} {N : ℕ}
     (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * π))
     (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * π)) :
     S_ N (f - g) = S_ N f - S_ N g := by
   ext x
-  simp [partialFourierSum, fourierCoeffOn_sub hf hg, sub_mul]
+  simp only [partialFourierSum, fourierCoeffOn_sub hf hg, fourier_apply, fourier_coe_apply',
+    Complex.ofReal_mul, Complex.ofReal_ofNat, sub_mul, sum_sub_distrib, Pi.sub_apply]
 
 @[simp]
 lemma partialFourierSum_mul {f: ℝ → ℂ} {a : ℂ} {N : ℕ}:
   S_ N (fun x ↦ a * f x) = fun x ↦ a * S_ N f x := by
   ext x
-  simp [partialFourierSum, mul_sum, mul_assoc]
+  simp only [partialFourierSum, fourierCoeffOn_mul, fourier_apply, fourier_coe_apply', mul_assoc,
+    Complex.ofReal_mul, Complex.ofReal_ofNat, mul_sum]
 
 lemma fourier_periodic {n : ℤ} :
     (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * π))).Periodic (2 * π) := by
@@ -122,6 +130,37 @@ theorem strictConvexOn_cos_Icc : StrictConvexOn ℝ (Set.Icc (π / 2) (π + π /
   rw [interior_Icc] at hx
   simp [Real.cos_neg_of_pi_div_two_lt_of_lt hx.1 hx.2]
 
+lemma lower_secant_bound_aux {η : ℝ} (ηpos : 0 < η) {x : ℝ} (le_abs_x : η ≤ x)
+    (abs_x_le : x ≤ 2 * π - η) (x_le_pi : x ≤ π) (h : π / 2 < x) :
+    2 / π * η ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖ := by
+  calc (2 / π) * η
+    _ ≤ (2 / π) * x := by gcongr
+    _ = 1 - ((1 - (2 / π) * (x - π / 2)) * Real.cos (π / 2) + ((2 / π) * (x - π / 2)) * Real.cos (π)) := by
+      field_simp -- a bit slow
+      ring
+    _ ≤ 1 - (Real.cos ((1 - (2 / π) * (x - π / 2)) * (π / 2) + (((2 / π) * (x - π / 2)) * (π)))) := by
+      gcongr
+      apply (strictConvexOn_cos_Icc.convexOn).2 (by simp [pi_nonneg])
+      · simp
+        constructor <;> linarith [pi_nonneg]
+      · rw [sub_nonneg, mul_comm]
+        exact mul_le_of_le_div₀ (by norm_num) (div_nonneg (by norm_num) pi_nonneg) (by simpa)
+      · exact mul_nonneg (div_nonneg (by norm_num) pi_nonneg) (by linarith [h])
+      · simp
+    _ = 1 - Real.cos x := by congr; field_simp; ring -- slow
+    _ ≤ Real.sqrt ((1 - Real.cos x) ^ 2) := by
+      exact Real.sqrt_sq_eq_abs _ ▸ le_abs_self _
+    _ ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖ := by
+        rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_abs, Complex.abs_eq_sqrt_sq_add_sq]
+        simp only [Complex.sub_re, Complex.one_re, Complex.add_re, Complex.mul_re, Complex.I_re,
+          Complex.sin_ofReal_im, Complex.I_im, Complex.sub_im, Complex.one_im, Complex.add_im,
+          Complex.cos_ofReal_im, Complex.mul_im]
+        rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re]
+        apply (Real.sqrt_le_sqrt_iff _).mpr
+        · simp only [mul_zero, mul_one, sub_self, add_zero, zero_add, zero_sub, even_two,
+          Even.neg_pow, le_add_iff_nonneg_right, pow_two_nonneg]
+        · linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
+
 lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_le : |x| ≤ 2 * π - η) :
     (2 / π) * η ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
   by_cases ηpos : η ≤ 0
@@ -167,34 +206,9 @@ lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_l
         · simp [pow_two_nonneg]
         · linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
   · push_neg at h
-    calc (2 / π) * η
-    _ ≤ (2 / π) * x := by gcongr
-    _ = 1 - ((1 - (2 / π) * (x - π / 2)) * Real.cos (π / 2) + ((2 / π) * (x - π / 2)) * Real.cos (π)) := by
-      field_simp
-      ring
-    _ ≤ 1 - (Real.cos ((1 - (2 / π) * (x - π / 2)) * (π / 2) + (((2 / π) * (x - π / 2)) * (π)))) := by
-      gcongr
-      apply (strictConvexOn_cos_Icc.convexOn).2 (by simp [pi_nonneg])
-      · simp
-        constructor <;> linarith [pi_nonneg]
-      · rw [sub_nonneg, mul_comm]
-        exact mul_le_of_le_div₀ (by norm_num) (div_nonneg (by norm_num) pi_nonneg) (by simpa)
-      · exact mul_nonneg (div_nonneg (by norm_num) pi_nonneg) (by linarith [h])
-      · simp
-    _ = 1 - Real.cos x := by congr; field_simp; ring
-    _ ≤ Real.sqrt ((1 - Real.cos x) ^ 2) := by
-      exact Real.sqrt_sq_eq_abs _ ▸ le_abs_self _
-    _ ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖ := by
-        rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_abs, Complex.abs_eq_sqrt_sq_add_sq]
-        simp only [Complex.sub_re, Complex.one_re, Complex.add_re, Complex.mul_re, Complex.I_re,
-          Complex.sin_ofReal_im, Complex.I_im, Complex.sub_im, Complex.one_im, Complex.add_im,
-          Complex.cos_ofReal_im, Complex.mul_im]
-        rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re]
-        apply (Real.sqrt_le_sqrt_iff _).mpr
-        · simp [pow_two_nonneg]
-        · linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
+    exact lower_secant_bound_aux ηpos le_abs_x abs_x_le x_le_pi h
 
-/-Slightly weaker version of Lemma 11..1.9 (lower secant bound) with simplified constant. -/
+/- Slightly weaker version of Lemma 11..1.9 (lower secant bound) with simplified constant. -/
 lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * π + η) (2 * π - η)) (xAbs : η ≤ |x|) :
     η / 2 ≤ Complex.abs (1 - Complex.exp (Complex.I * x)) := by
   by_cases ηpos : η < 0

Carleson/Classical/CarlesonOperatorReal.lean

@@ -37,17 +37,15 @@ lemma annulus_measurableSet {x r R : ℝ} : MeasurableSet {y | dist x y ∈ Set.
 
 lemma sup_eq_sup_dense_of_continuous {f : ℝ → ENNReal} {S : Set ℝ} (D : Set ℝ) (hS : IsOpen S) (hD: Dense D) (hf : ContinuousOn f S) :
     ⨆ r ∈ S, f r = ⨆ r ∈ (S ∩ D), f r := by
-  --Show two inequalities, one is trivial
+  -- Show two inequalities, one is trivial
   refine le_antisymm (le_of_forall_lt_imp_le_of_dense fun c hc ↦ ?_) (biSup_mono Set.inter_subset_left)
   rw [lt_iSup_iff] at hc
   rcases hc with ⟨x, hx⟩
   rw [lt_iSup_iff] at hx
   rcases hx with ⟨xS, hx⟩
   have : IsOpen (S ∩ f ⁻¹' (Set.Ioi c)) := hf.isOpen_inter_preimage hS isOpen_Ioi
-  have : Set.Nonempty ((S ∩ f ⁻¹' (Set.Ioi c)) ∩ D) := by
-    apply hD.inter_open_nonempty _ this _
-    use x, xS
-    simpa
+  have : Set.Nonempty ((S ∩ f ⁻¹' (Set.Ioi c)) ∩ D) :=
+    hD.inter_open_nonempty _ this ⟨x, xS, by simpa⟩
   rcases this with ⟨y, hy⟩
   rw [Set.mem_inter_iff, Set.mem_inter_iff, Set.mem_preimage, Set.mem_Ioi] at hy
   exact hy.1.2.le.trans (le_biSup _ ⟨hy.1.1, hy.2⟩)

Carleson/Classical/DirichletKernel.lean

@@ -21,7 +21,8 @@ variable {N : ℕ}
 
 lemma dirichletKernel_periodic : Function.Periodic (dirichletKernel N) (2 * π) := by
   intro x
-  simp [dirichletKernel]
+  simp only [dirichletKernel, Int.ofNat_eq_coe, AddSubgroup.mem_zmultiples,
+    QuotientAddGroup.mk_add_of_mem, fourier_apply, fourier_coe_apply', ofReal_mul, ofReal_ofNat]
 
 lemma dirichletKernel'_periodic : Function.Periodic (dirichletKernel' N) (2 * π) := by
   intro x
@@ -30,7 +31,7 @@ lemma dirichletKernel'_periodic : Function.Periodic (dirichletKernel' N) (2 * π
   congr 2
   · rw [mul_add, exp_add]
     conv => rhs; rw [← mul_one (cexp _)]
-    congr
+    congr 1
     convert exp_int_mul_two_pi_mul_I N using 2
     norm_cast
     simp
@@ -66,9 +67,9 @@ lemma dirichletKernel_eq {x : ℝ} (h : cexp (I * x) ≠ 1) :
     calc (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x
       _ = ∑ n ∈ Icc (-(N : ℤ)) N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by
         rw [dirichletKernel, mul_sum]
-        congr with n
+        congr 1 with n
         simp [sub_mul, ← exp_add, ← exp_add]
-        congr <;>
+        congr 2 <;>
         · ring_nf
           congr 1
           rw [mul_assoc, mul_assoc]
@@ -81,11 +82,11 @@ lemma dirichletKernel_eq {x : ℝ} (h : cexp (I * x) ≠ 1) :
       _ = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by
         rw [← sum_Ico_add_eq_sum_Icc, ← sum_Ioc_add_eq_sum_Icc, add_sub_add_comm,
           ← zero_add (cexp ((N + 1 / 2) * I * ↑x) - cexp (-(N + 1 / 2) * I * ↑x))]
-        congr
+        congr 2
         rw [sub_eq_zero]
         conv => lhs; rw [← Int.add_sub_cancel (-(N : ℤ)) 1, sub_eq_add_neg,
           ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add']
-        congr with n
+        congr 2 with n
         · rw [mem_Ico, mem_Ioc, Int.lt_iff_add_one_le, add_le_add_iff_right,
             ← mem_Icc, Int.lt_iff_add_one_le, ← mem_Icc]
           simp
@@ -102,7 +103,7 @@ lemma dirichletKernel_eq {x : ℝ} (h : cexp (I * x) ≠ 1) :
       _ = cexp (1 / 2 * I * ↑x) * cexp (1 / 2 * I * ↑x) := by
         rw [← exp_add, mul_assoc, ← mul_add]
         ring_nf
-      _ = cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) := by congr
+      _ = cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) := by congr 2
       _ = 1 := by
         rw [← exp_add]
         ring_nf

Carleson/Classical/VanDerCorput.lean

@@ -50,16 +50,16 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         apply this
         · intro x y
           simp only [Function.comp_apply]
-          rw [edist_eq_enorm_sub, ← map_sub, starRingEnd_apply, enorm_eq_nnnorm, nnnorm_star,
-            ← enorm_eq_nnnorm, ← edist_eq_enorm_sub]
+          rw [edist_eq_enorm_sub, ← map_sub, starRingEnd_apply,
+            enorm_eq_nnnorm, nnnorm_star]
           exact h1 _ _
         · intro x hx
           rw [Function.comp_apply, RCLike.norm_conj]
           exact h2 x hx
         · exact Int.neg_ne_zero.mpr n_nonzero
         · rw [Left.neg_pos_iff]; exact lt_of_le_of_ne n_pos n_nonzero
     rw [abs_neg]
-  --Case distinction such that splitting integrals in the second case works.
+  -- Case distinction such that splitting integrals in the second case works.
   by_cases h : b - a < π / n
   · have : 0 < 1 + ↑|n| * (b - a) := by
       apply add_pos_of_pos_of_nonneg zero_lt_one
@@ -99,7 +99,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
   have integrand_continuous2 : Continuous (fun x ↦ cexp (I * ↑n * (↑x + ↑π / ↑n)) * ϕ x) :=
     Continuous.mul (by fun_prop) h1.continuous
   have integrand_continuous3 : Continuous (fun (x : ℝ) ↦ cexp (I * n * x) * ϕ (x - π / n)) :=
-    Continuous.mul (by fun_prop) (h1.continuous.comp (by continuity))
+    Continuous.mul (by fun_prop) (h1.continuous.comp (by fun_prop))
   calc _
     _ = ‖∫ (x : ℝ) in a..b, (1 / 2 * (I * n * x).exp - 1 / 2 * (I * ↑n * (↑x + ↑π / ↑n)).exp) * ϕ x‖ := by
       congr

Carleson/ForestOperator/L2Estimate.lean

@@ -183,7 +183,7 @@ private lemma nontangential_integral_bound₂ (hf : BoundedCompactSupport f) {x
     intro y hy
     rw [Annulus.cc] at hy
     rw [enorm_mul]
-    refine mul_le_mul_right' ((ennnorm_K_le 5 hy.1).trans ?_) ‖f y‖ₑ
+    refine mul_le_mul_right' ((enorm_K_le 5 hy.1).trans ?_) ‖f y‖ₑ
     gcongr
     · norm_num
     · norm_num
@@ -486,14 +486,14 @@ private lemma le_C7_2_1 {a : ℕ} (ha : 4 ≤ a) :
   _ ≤ (2 : ℝ≥0∞) ^ ((a : ℝ) ^ 3) * (2 : ℝ≥0∞) ^ (151 * (a : ℝ) ^ 3) := by
     apply mul_right_mono
     norm_cast
-    calc
-      3 * 2 ^ (12 * a) ≤ 2 ^ 2 * 2 ^ (12 * a) := by gcongr; norm_num
-      _                = 2 ^ (2 + 12 * a)     := by rw [pow_add]
-      _                ≤ 2 ^ (a ^ 3)          := pow_le_pow_right₀ one_le_two <| calc
-                          2 + 12 * a ≤ a + 12 * a  := by apply add_le_add_right; linarith
-                          _          = 13 * a      := by ring
-                          _          ≤ a ^ 2 * a   := by rw [mul_le_mul_right] <;> nlinarith
-                          _          = a ^ 3       := rfl
+    calc 3 * 2 ^ (12 * a)
+      _ ≤ 2 ^ 2 * 2 ^ (12 * a) := by gcongr; norm_num
+      _ = 2 ^ (2 + 12 * a)     := by rw [pow_add]
+      _ ≤ 2 ^ (a ^ 3)          := pow_le_pow_right₀ one_le_two <| calc 2 + 12 * a
+        _ ≤ a + 12 * a := by apply add_le_add_right; linarith
+        _ = 13 * a     := by ring
+        _ ≤ a ^ 2 * a  := by rw [mul_le_mul_right] <;> nlinarith
+        _ = a ^ 3      := rfl
   _ = _ := by
     rw [C7_2_1_def, ← ENNReal.rpow_add _ _ two_ne_zero ENNReal.ofNat_ne_top]
     norm_cast

Carleson/Psi.lean

@@ -460,15 +460,15 @@ lemma norm_K_le {s : ℤ} {x y : X} (n : ℕ) (hxy : dist x y ≥ D ^ (s - 1) /
   apply div_le_div_of_nonneg_right _ measureReal_nonneg
   exact_mod_cast le_of_eq (by ring)
 
-lemma ennnorm_K_le {s : ℤ} {x y : X} (n : ℕ) (hxy : dist x y ≥ D ^ (s - 1) / 4) :
+lemma enorm_K_le {s : ℤ} {x y : X} (n : ℕ) (hxy : dist x y ≥ D ^ (s - 1) / 4) :
     ‖K x y‖ₑ ≤ 2 ^ ((2 + n) * (a : ℝ) + 101 * a ^ 3) / volume (ball x (2 ^ n * D ^ s)) := by
-  rw [← ENNReal.ofReal_ofNat 2, ENNReal.ofReal_rpow_of_pos two_pos]
-  rw [← ENNReal.ofReal_toReal (measure_ball_ne_top _ _)]
-  rw [← ENNReal.ofReal_div_of_pos, ← Measure.real, ← ofReal_norm]; swap
+  rw [← ENNReal.ofReal_ofNat 2, ENNReal.ofReal_rpow_of_pos two_pos,
+    ← ENNReal.ofReal_toReal (measure_ball_ne_top _ _),
+    ← ENNReal.ofReal_div_of_pos, ← Measure.real, ← ofReal_norm]; swap
   · apply ENNReal.toReal_pos
     · refine (measure_ball_pos volume x ?_).ne.symm
       exact mul_pos (pow_pos two_pos n) (defaultD_pow_pos a s)
-    · apply measure_ball_ne_top x (2 ^ n * D ^ s)
+    · exact measure_ball_ne_top x (2 ^ n * D ^ s)
   rw [ENNReal.ofReal_le_ofReal_iff (by positivity)]
   exact norm_K_le n hxy
 

Carleson/ToMathlib/ENorm.lean

@@ -49,8 +49,10 @@ export ENormedAddCommSubMonoid
   (sub_add_cancel_of_enorm_le add_right_cancel_of_enorm_lt_top esub_self)
 export ENormedSpace (enorm_smul)
 
+-- mathlib has these (in the _root_ namespace), in a less general setting
 attribute [simp] ENormedAddMonoid.enorm_eq_zero ENormedSpace.enorm_smul
 
+-- mathlib has this (unprimed), for a SeminormedAddGroup E
 @[simp] lemma enorm_zero' {ε} [ENormedAddMonoid ε] : ‖(0 : ε)‖ₑ = 0 := by simp
 
 instance : ENormedSpace ℝ≥0∞ where
@@ -88,16 +90,19 @@ protected theorem Continuous.enorm {X : Type*} [TopologicalSpace X] {f : X → E
     (hf : Continuous f) : Continuous (fun x => (‖f x‖ₑ)) :=
   continuous_enorm.comp hf
 
+-- mathlib has this, but only for a NormedAddCommGroup
 @[fun_prop]
 theorem measurable_enorm [MeasurableSpace E] [OpensMeasurableSpace E] :
     Measurable (fun a : E => (‖a‖ₑ)) :=
   continuous_enorm.measurable
 
+-- mathlib has this, but only for a NormedAddCommGroup
 @[fun_prop]
 protected theorem AEMeasurable.enorm [MeasurableSpace E] [OpensMeasurableSpace E] {f : α → E}
     (hf : AEMeasurable f μ) : AEMeasurable (fun a => (‖f a‖ₑ)) μ :=
   measurable_enorm.comp_aemeasurable hf
 
+-- TODO: generalise the mathlib version (unprimed), then replace by that one
 @[fun_prop]
 protected theorem AEStronglyMeasurable.enorm' {f : α → E}
     (hf : AEStronglyMeasurable f μ) : AEMeasurable (fun a => (‖f a‖ₑ)) μ :=

Carleson/ToMathlib/HardyLittlewood.lean

@@ -358,12 +358,10 @@ protected theorem MeasureTheory.AESublinearOn.maximalFunction
   refine AESublinearOn.biSup2 (P := (Memℒp · ⊤ μ)) (Q := (Memℒp · 1 μ)) h𝓑 ?_ ?_
     Memℒp.zero Memℒp.zero Memℒp.add Memℒp.add ?_ ?_ ?_
   · intro u hu
-    have := MB_ae_ne_top' (c := c) h𝓑 hR (.inl hu)
-    filter_upwards [this] with x hx
+    filter_upwards [MB_ae_ne_top' h𝓑 hR (.inl hu)] with x hx
     simpa [MB, maximalFunction] using hx
   · intro u hu
-    have := MB_ae_ne_top (c := c) h𝓑 hR hu
-    filter_upwards [this] with x hx
+    filter_upwards [MB_ae_ne_top h𝓑 hR hu] with x hx
     simpa [MB, maximalFunction] using hx
   · intro f c hf; rw [NNReal.smul_def]; exact hf.const_smul _
   · intro f c hf; rw [NNReal.smul_def]; exact hf.const_smul _