diff --git a/Carleson/Classical/CarlesonOnTheRealLine.lean b/Carleson/Classical/CarlesonOnTheRealLine.lean
index 928c7ee0..ab7dd25b 100644
--- a/Carleson/Classical/CarlesonOnTheRealLine.lean
+++ b/Carleson/Classical/CarlesonOnTheRealLine.lean
@@ -178,7 +178,7 @@ lemma coeΘ_R_C (n : Θ ℝ) (x : ℝ) : (n x : ℂ) = n * x := by norm_cast
 lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} :
     localOscillation (ball x r) (coeΘ f) (coeΘ g) ≤ dist_{x, r} f g := by
   by_cases r_pos : r ≤ 0
-  . rw [ball_eq_empty.mpr r_pos]
+  · rw [ball_eq_empty.mpr r_pos]
     unfold localOscillation
     simp [dist_nonneg]
   push_neg at r_pos
@@ -199,7 +199,7 @@ lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} :
       --TODO: investigate strange (delaborator) behavior - why is there still a sup?
       intro z
       apply Real.iSup_le
-      . intro hz
+      · intro hz
         simp at hz
         rw [Real.dist_eq, Real.dist_eq] at hz
         rw [Real.norm_eq_abs]
@@ -222,7 +222,7 @@ lemma frequency_monotone {x₁ x₂ r R : ℝ} {f g : Θ ℝ} (h : ball x₁ r 
   unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal
   dsimp
   by_cases r_pos : r ≤ 0
-  . rw [ball_eq_empty.mpr r_pos] at h
+  · rw [ball_eq_empty.mpr r_pos] at h
     rw [max_eq_right r_pos]
     gcongr
     apply le_max_right
@@ -235,10 +235,10 @@ lemma frequency_ball_doubling {x₁ x₂ r : ℝ} {f g : Θ ℝ} : dist_{x₂, 2
   unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal Real.pseudoMetricSpace
   dsimp
   by_cases r_nonneg : r ≥ 0
-  . rw [max_eq_left, max_eq_left]
+  · rw [max_eq_left, max_eq_left]
     ring_nf;rfl
     all_goals linarith [r_nonneg]
-  . rw [max_eq_right, max_eq_right]
+  · rw [max_eq_right, max_eq_right]
     simp
     all_goals linarith [r_nonneg]
 
@@ -246,10 +246,10 @@ lemma frequency_ball_doubling {x₁ x₂ r : ℝ} {f g : Θ ℝ} : dist_{x₂, 2
     unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal
     dsimp
     by_cases r_nonneg : r ≥ 0
-    . rw [max_eq_left, max_eq_left]
+    · rw [max_eq_left, max_eq_left]
       ring_nf;rfl
       all_goals linarith [r_nonneg]
-    . rw [max_eq_right, max_eq_right]
+    · rw [max_eq_right, max_eq_right]
       simp
       all_goals linarith [r_nonneg]
 
@@ -261,7 +261,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
   · --trivial case
     use {f}
     constructor
-    . norm_num
+    · norm_num
     simp only [Finset.mem_singleton, Set.iUnion_iUnion_eq_left]
     rw [Metric.ball_eq_empty.mpr R'pos, Set.subset_empty_iff, Metric.ball_eq_empty]
     linarith
@@ -270,12 +270,12 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
   · --trivial case
     use {f}
     constructor
-    . norm_num
+    · norm_num
     simp only [Finset.mem_singleton, Set.iUnion_iUnion_eq_left]
     convert Set.subset_univ _
     ext g
     constructor
-    . simp
+    · simp
     simp only [Set.mem_univ, mem_ball, true_implies]
     unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal
     dsimp
@@ -302,7 +302,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
   /- m₁, m₂, m₃ each correspond to one case. -/
   simp only [Set.mem_iUnion, mem_ball, exists_prop]
   by_cases h : φ ≤ f - R' / (2 * R)
-  . use m₁
+  · use m₁
     constructor
     · rw [balls_def]
       simp
@@ -322,7 +322,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
       _ = 2 * R * (m₁ - f) + 2 * R * (f - φ) := by ring
       _ < - R' + 2 * R' := by
         apply add_lt_add_of_le_of_lt
-        . rw [m₁def]
+        · rw [m₁def]
           calc 2 * R * (⌊f - R' / (2 * R)⌋ - f)
             _ ≤ 2 * R * (f - R' / (2 * R) - f) := by
               gcongr
@@ -330,7 +330,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
             _ = -R' := by
               ring_nf
               rw [mul_comm, ←mul_assoc, inv_mul_cancel Rpos.ne.symm, one_mul]
-        . calc 2 * R * (↑f - ↑φ)
+        · calc 2 * R * (↑f - ↑φ)
             _ ≤ 2 * R * |↑f - ↑φ| := by
               gcongr
               apply le_abs_self
@@ -346,7 +346,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
       _ = R' := by ring
   push_neg at h
   by_cases h' : φ < f + R' / (2 * R)
-  . use m₂
+  · use m₂
     constructor
     · rw [balls_def]
       simp
@@ -367,7 +367,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
   push_neg at h'
   use m₃
   constructor
-  . simp [balls_def]
+  · simp [balls_def]
   unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal
   dsimp
   push_cast
@@ -382,7 +382,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
     _ = 2 * R * (φ - f) + 2 * R * (f - m₃) := by ring
     _ < 2 * R' - R' := by
       apply add_lt_add_of_lt_of_le
-      . calc 2 * R * (↑φ - ↑f)
+      · calc 2 * R * (↑φ - ↑f)
           _ ≤ 2 * R * |↑φ - ↑f| := by
             gcongr
             exact le_abs_self _
@@ -398,7 +398,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
             symm
             rw [max_eq_left_iff]
             exact Rpos.le
-      . rw [m₃def]
+      · rw [m₃def]
         calc 2 * R * (f - ⌈f + R' / (2 * R)⌉)
           _ ≤ 2 * R * (f - (f + R' / (2 * R))) := by
             gcongr
@@ -427,8 +427,8 @@ instance compatibleFunctions_R : CompatibleFunctions ℝ ℝ (2 ^ 4) where
     unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal
     dsimp
     by_cases r_nonneg : 0 ≤ r
-    . gcongr; norm_num
-    . push_neg at r_nonneg
+    · gcongr; norm_num
+    · push_neg at r_nonneg
       rw [max_eq_right (by linarith), max_eq_right (by linarith)]
   ballsCoverBalls := by
     intro x R R' f
@@ -441,7 +441,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
   norm_integral_exp_le := by
     intro x r ϕ K hK _ f g
     by_cases r_pos : 0 ≥ r
-    . rw [ball_eq_empty.mpr r_pos]
+    · rw [ball_eq_empty.mpr r_pos]
       simp
     push_neg at r_pos
     rw [defaultτ, ← one_div, measureReal_def, Real.volume_ball, ENNReal.toReal_ofReal (by linarith [r_pos]), Real.ball_eq_Ioo, ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by linarith [r_pos])]
@@ -468,11 +468,11 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
         norm_cast
       _ ≤ 2 * Real.pi * ((x + r) - (x - r)) * (B + L * ((x + r) - (x - r)) / 2) * (1 + |((↑f - ↑g) : ℤ)| * ((x + r) - (x - r)))⁻¹ := by
         apply van_der_Corput (by linarith)
-        . rw [lipschitzWith_iff_dist_le_mul]
+        · rw [lipschitzWith_iff_dist_le_mul]
           intro x y
           --TODO: The following could be externalised as a lemma.
           by_cases hxy : x = y
-          . rw [hxy]
+          · rw [hxy]
             simp
           rw [dist_eq_norm, ← div_le_iff (dist_pos.mpr hxy), Ldef, NNReal.coe_mk]
           --apply ConditionallyCompleteLattice.le_csSup
@@ -480,14 +480,14 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
           apply le_ciSup_of_le _ y
           apply le_ciSup_of_le _ hxy
           rfl
-          . use K
+          · use K
             rw [upperBounds]
             simp only [ne_eq, Set.mem_range, exists_prop, and_imp,
               forall_apply_eq_imp_iff, Set.mem_setOf_eq]
             intro h
             rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
             exact LipschitzWith.norm_sub_le hK _ _
-          . use K
+          · use K
             rw [upperBounds]
             simp only [ne_eq, Set.mem_range, forall_exists_index,
               forall_apply_eq_imp_iff, Set.mem_setOf_eq]
@@ -496,7 +496,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
             intro h
             rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
             exact LipschitzWith.norm_sub_le hK _ _
-          . use K
+          · use K
             rw [upperBounds]
             simp only [ne_eq, Set.mem_range, forall_exists_index,
               forall_apply_eq_imp_iff, Set.mem_setOf_eq]
@@ -507,10 +507,10 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
             intro h
             rw [div_le_iff (dist_pos.mpr h), dist_eq_norm]
             apply LipschitzWith.norm_sub_le hK
-        . --prove main property of B
+        · --prove main property of B
           intro y hy
           apply ConditionallyCompleteLattice.le_biSup
-          . --TODO: externalize as lemma LipschitzWithOn.BddAbove or something like that?
+          · --TODO: externalize as lemma LipschitzWithOn.BddAbove or something like that?
             rw [Real.ball_eq_Ioo]
             exact BddAbove.mono (Set.image_mono Set.Ioo_subset_Icc_self)
               (isCompact_Icc.bddAbove_image (continuous_norm.comp hK.continuous).continuousOn)
@@ -521,14 +521,14 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
         ring
       _ ≤ (2 ^ 4 : ℕ) * (2 * r) * iLipNorm ϕ x r * (1 + 2 * r * ↑|(↑f - ↑g : ℤ)|) ^ (- (1 / (4 : ℝ))) := by
         gcongr
-        . exact mul_nonneg (mul_nonneg (by norm_num) (by linarith)) (iLipNorm_nonneg r_pos.le)
-        . norm_num
+        · exact mul_nonneg (mul_nonneg (by norm_num) (by linarith)) (iLipNorm_nonneg r_pos.le)
+        · norm_num
           linarith [Real.pi_le_four]
-        . unfold iLipNorm
+        · unfold iLipNorm
           gcongr
           apply le_of_eq Bdef
           apply le_of_eq Ldef
-        . rw [← Real.rpow_neg_one]
+        · rw [← Real.rpow_neg_one]
           apply Real.rpow_le_rpow_of_exponent_le _ (by norm_num)
           simp only [Int.cast_abs, Int.cast_sub, le_add_iff_nonneg_right]
           exact mul_nonneg (by linarith) (abs_nonneg _)
diff --git a/Carleson/Classical/CarlesonOperatorReal.lean b/Carleson/Classical/CarlesonOperatorReal.lean
index 0162849f..4eac245f 100644
--- a/Carleson/Classical/CarlesonOperatorReal.lean
+++ b/Carleson/Classical/CarlesonOperatorReal.lean
@@ -74,9 +74,9 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
   set Q : Set ℝ := Rat.cast '' Set.univ with Qdef
   have hQ : Dense Q ∧ Countable Q := by
     constructor
-    . rw [Rat.denseEmbedding_coe_real.dense_image]
+    · rw [Rat.denseEmbedding_coe_real.dense_image]
       exact dense_univ
-    . rw [Set.countable_coe_iff, Qdef, Set.image_univ]
+    · rw [Set.countable_coe_iff, Qdef, Set.image_univ]
       exact Set.countable_range _
   have : (fun x ↦ ⨆ (r ∈ Set.Ioo 0 1), G x r) = (fun x ↦ ⨆ (r ∈ (Set.Ioo 0 1) ∩ Q), G x r) := by
     ext x
@@ -90,54 +90,54 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
       rw [eventually_nhds_iff]
       use S
       constructor
-      . intro s hs
+      · intro s hs
         apply Filter.eventually_of_forall
         intro y
         rw [bound_def, Fdef, norm_indicator_eq_indicator_norm]
         simp only
         rw [norm_indicator_eq_indicator_norm]
         apply Set.indicator_le_indicator_of_subset
-        . intro y hy
+        · intro y hy
           constructor <;> linarith [hy.1, hy.2, hs.1]
-        . intro y
+        · intro y
           apply norm_nonneg
       constructor
-      . apply isOpen_Ioo
-      . rw [Sdef]
+      · apply isOpen_Ioo
+      · rw [Sdef]
         constructor <;> linarith [hr.1]
     apply MeasureTheory.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
+    · 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
         rw [norm_mul, norm_mul, mul_assoc Complex.I, mul_comm Complex.I]
         norm_cast
         rw [Complex.norm_exp_ofReal_mul_I, mul_one]
         gcongr
-        . linarith [f_bounded 0, norm_nonneg (f 0)]
-        . exact f_bounded a
-        . rw [Set.mem_setOf_eq] at ha
+        · linarith [f_bounded 0, norm_nonneg (f 0)]
+        · exact f_bounded a
+        · rw [Set.mem_setOf_eq] at ha
           rw [Real.norm_eq_abs, abs_of_nonneg (by apply div_nonneg (by norm_num); linarith [hr.1])]
           calc _
             _ ≤ 2 ^ (2 : ℝ) / (2 * |x - a|) := Hilbert_kernel_bound
             _ ≤ 4 / (2 * (r / 2)) := by
               gcongr
-              . linarith [hr.1]
-              . norm_num
-              . rw [← Real.dist_eq]
+              · linarith [hr.1]
+              · norm_num
+              · rw [← Real.dist_eq]
                 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 [annulus_real_volume (by constructor <;> linarith [hr.1, hr.2])]
+      · rw [annulus_real_volume (by constructor <;> linarith [hr.1, hr.2])]
         exact ENNReal.ofReal_ne_top
-      . --measurability
+      · --measurability
         apply ((Measurable.of_uncurry_left (helper f_measurable)).norm).aestronglyMeasurable
-      . --interesting part
+      · --interesting part
         rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
         simp_rw [norm_norm]
         apply Filter.eventually_of_forall
         apply F_bound_on_set
-    . have contOn1 : ∀ (y : ℝ), ContinuousOn (fun s ↦ F x s y) (Set.Iio (dist x y)) := by
+    · have contOn1 : ∀ (y : ℝ), ContinuousOn (fun s ↦ F x s y) (Set.Iio (dist x y)) := by
         intro y
         rw [continuousOn_iff_continuous_restrict]
         apply continuous_of_const
@@ -146,12 +146,12 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
         rw [Fdef]
         simp only [Set.mem_Ioo]
         by_cases h : dist x y < 1
-        . rw [Set.indicator_apply, ite_cond_eq_true, Set.indicator_apply, ite_cond_eq_true]
-          . simp
+        · rw [Set.indicator_apply, ite_cond_eq_true, Set.indicator_apply, ite_cond_eq_true]
+          · simp
             use ht
-          . simp
+          · simp
             use hs
-        . push_neg at h
+        · push_neg at h
           rw [Set.indicator_apply, ite_cond_eq_false, Set.indicator_apply, ite_cond_eq_false]
           all_goals
             simp only [Set.mem_setOf_eq, eq_iff_iff, iff_false, not_and, not_lt]
@@ -165,25 +165,25 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
         rw [Fdef]
         simp
         rw [Set.indicator_apply, ite_cond_eq_false, Set.indicator_apply, ite_cond_eq_false]
-        . rw [Set.mem_Ioi, min_lt_iff] at ht
+        · rw [Set.mem_Ioi, min_lt_iff] at ht
           simp
           intro h
           rcases ht with h' | h'
-          . exfalso
+          · exfalso
             exact (lt_self_iff_false _).mp (h'.trans h)
-          . exact (h'.trans h).le
-        . rw [Set.mem_Ioi, min_lt_iff] at hs
+          · exact (h'.trans h).le
+        · rw [Set.mem_Ioi, min_lt_iff] at hs
           simp
           intro h
           rcases hs with h' | h'
-          . exfalso
+          · exfalso
             exact (lt_self_iff_false _).mp (h'.trans h)
-          . exact (h'.trans h).le
+          · exact (h'.trans h).le
       have contOn : ∀ y, ∀ t ≠ dist x y, ContinuousAt (fun s ↦ F x s y) t := by
         intro y t ht
         by_cases h : t < dist x y
-        . exact_mod_cast (contOn1 y).continuousAt (Iio_mem_nhds h)
-        . push_neg at h
+        · exact_mod_cast (contOn1 y).continuousAt (Iio_mem_nhds h)
+        · push_neg at h
           exact ContinuousOn.continuousAt (contOn2 y) (Ioi_mem_nhds
             ((min_le_left _ _).trans_lt (lt_of_le_of_ne h ht.symm)))
       have subset_finite : {y | ¬ContinuousAt (fun s ↦ F x s y) r} ⊆ ({x - r, x + r} : Finset ℝ) := by
@@ -195,15 +195,15 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
         rw [Real.dist_eq, abs_eq hr.1.le] at this
         simp
         rcases this with h | h
-        . left; linarith
-        . right; linarith
+        · left; linarith
+        · right; linarith
       rw [MeasureTheory.ae_iff]
       exact MeasureTheory.measure_mono_null subset_finite (Finset.measure_zero _ _)
-    . exact Filter.eventually_of_forall fun r ↦ ((Measurable.of_uncurry_left
+    · exact Filter.eventually_of_forall fun r ↦ ((Measurable.of_uncurry_left
         (helper f_measurable)).indicator annulus_measurableSet).aestronglyMeasurable
   rw [this]
   apply measurable_biSup _
-  . apply Set.Countable.mono Set.inter_subset_right hQ.2
+  · apply Set.Countable.mono Set.inter_subset_right hQ.2
   intro r _
   apply measurable_coe_nnreal_ennreal.comp (measurable_nnnorm.comp _)
   rw [← stronglyMeasurable_iff_measurable]
@@ -244,14 +244,14 @@ lemma CarlesonOperatorReal_eq_of_restrict_interval {f : ℝ → ℂ} {a b : ℝ}
   left
   rw [Set.indicator]
   split_ifs with hy
-  . left; rfl
-  . right
+  · left; rfl
+  · right
     apply k_of_one_le_abs
     simp only [Set.mem_Ioo, not_and_or, not_lt] at hy
     rw [le_abs]
     rcases hy with hy | hy
-    . left; linarith [hx.1]
-    . right; linarith [hx.2]
+    · left; linarith [hx.1]
+    · right; linarith [hx.2]
 
 /-
 import Mathlib.MeasureTheory.Measure.MeasureSpace
diff --git a/Carleson/Classical/ControlApproximationEffect.lean b/Carleson/Classical/ControlApproximationEffect.lean
index e80468f8..4e43cb34 100644
--- a/Carleson/Classical/ControlApproximationEffect.lean
+++ b/Carleson/Classical/ControlApproximationEffect.lean
@@ -115,9 +115,9 @@ lemma Dirichlet_Hilbert_diff {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (-Real.pi)
       · rw [mul_assoc I, mul_comm I]
         norm_cast
         rw [abs_exp_ofReal_mul_I]
-      . rw [←abs_conj, map_sub, map_one, ←exp_conj, ← neg_mul, map_mul, conj_I, conj_ofReal]
-      . apply min_le_left
-      . /-Duplicate from above:
+      · rw [←abs_conj, map_sub, map_one, ←exp_conj, ← neg_mul, map_mul, conj_I, conj_ofReal]
+      · apply min_le_left
+      · /-Duplicate from above:
         TODO: how to remove duplicate goals? -/
         rw [mul_assoc I, mul_comm I, ← neg_mul]
         norm_cast
@@ -214,12 +214,12 @@ lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g MeasureT
         rw [k_of_one_le_abs (h₁ h₀.1)]
         simp
       · rw [k_of_one_le_abs]
-        . simp
+        · simp
         dsimp at h₀ h₂
         rw [Real.dist_eq, Set.mem_Ioo] at h₀ h₂
         push_neg at h₀
         exact le_trans' (h₀ h₂.1) (by linarith [Real.two_le_pi])
-      . trivial
+      · 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
@@ -371,7 +371,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 [MeasureTheory.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
       rw [CarlesonOperatorReal, CarlesonOperatorReal]
       apply iSup₂_le
@@ -418,12 +418,12 @@ lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measu
       rw [decomposition, nnnorm_div, ENNReal.coe_div (by simp [Real.pi_pos.ne.symm])]
       norm_cast
       gcongr
-      . apply nnnorm_add_le
-      . rw [← ofReal_norm_eq_coe_nnnorm, Real.norm_of_nonneg Real.two_pi_pos.le]
+      · apply nnnorm_add_le
+      · rw [← ofReal_norm_eq_coe_nnnorm, Real.norm_of_nonneg Real.two_pi_pos.le]
     _ ≤ (T g x + T (⇑conj ∘ g) x + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi))) / ENNReal.ofReal (2 * Real.pi) := by
       gcongr
-      . apply le_CarlesonOperatorReal intervalIntegrable_g hx
-      . rw [ENNReal.ofReal]
+      · apply le_CarlesonOperatorReal intervalIntegrable_g hx
+      · rw [ENNReal.ofReal]
         norm_cast
         apply NNReal.le_toNNReal_of_coe_le
         rw [coe_nnnorm]
@@ -436,7 +436,7 @@ lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measu
             rw [norm_mul]
             gcongr
             · apply bound_g
-            . rw [Dirichlet_Hilbert_eq]
+            · rw [Dirichlet_Hilbert_eq]
               apply Dirichlet_Hilbert_diff
               constructor <;> linarith [hy.1, hy.2]
           _ = Real.pi * δ * (2 * Real.pi) := by
@@ -489,12 +489,12 @@ lemma rcarleson_exceptional_set_estimate_specific {δ : ℝ} (δpos : 0 < δ) {f
     intro x
     rw [hdef, norm_indicator_eq_indicator_norm, Set.indicator, Set.indicator]
     split_ifs with hx
-    . simp only [norm_eq_abs, Pi.one_apply, mul_one]; exact hf x
-    . simp
+    · simp only [norm_eq_abs, Pi.one_apply, mul_one]; exact hf x
+    · simp
   convert rcarleson_exceptional_set_estimate δpos (hmf.indicator measurableSet_Ioo) measurableSet_Ioo hh measurableSetE ?_
-  . rw [Real.volume_Ioo]
+  · rw [Real.volume_Ioo]
     ring_nf
-  . intro x hx
+  · intro x hx
     rw [← CarlesonOperatorReal_eq_of_restrict_interval (E_subset hx)]
     exact hE x hx
 
@@ -591,8 +591,8 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
       _ = (T h x + T (conj ∘ h) x) + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) := by
         rw [mul_add]
         congr
-        . rw [ENNReal.mul_div_cancel' (by simp [Real.pi_pos]) ENNReal.ofReal_ne_top]
-        . rw [← ENNReal.ofReal_mul Real.two_pi_pos.le]
+        · rw [ENNReal.mul_div_cancel' (by simp [Real.pi_pos]) ENNReal.ofReal_ne_top]
+        · rw [← ENNReal.ofReal_mul Real.two_pi_pos.le]
           ring_nf
   --TODO: align this with paper version
   have Evolume : MeasureTheory.volume E < ⊤ := by
@@ -614,12 +614,12 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
     _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (2 * Real.pi + 2) ^ (2 : ℝ)⁻¹) * (MeasureTheory.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'
+      · 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
       gcongr
-      . exact mul_nonneg hδ.le (C10_0_1_pos one_lt_two).le
-      . linarith [Real.two_le_pi]
+      · exact mul_nonneg hδ.le (C10_0_1_pos one_lt_two).le
+      · linarith [Real.two_le_pi]
   have δ_mul_const_pos : 0 < δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ := mul_pos (mul_pos hδ (C10_0_1_pos one_lt_two)) (Real.rpow_pos_of_pos (by linarith [Real.two_pi_pos]) _)
   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]
diff --git a/Carleson/Classical/DirichletKernel.lean b/Carleson/Classical/DirichletKernel.lean
index 0d95e6d1..8564ca35 100644
--- a/Carleson/Classical/DirichletKernel.lean
+++ b/Carleson/Classical/DirichletKernel.lean
@@ -28,25 +28,25 @@ lemma dirichletKernel'_periodic {N : ℕ} : Function.Periodic (dirichletKernel'
   simp_rw [dirichletKernel']
   push_cast
   congr 2
-  . rw [mul_add, exp_add]
+  · rw [mul_add, exp_add]
     conv => rhs; rw [← mul_one (cexp _)]
     congr
     convert exp_int_mul_two_pi_mul_I N using 2
     norm_cast
     ring
-  . congr 1
+  · congr 1
     rw [mul_add, exp_add]
     conv => rhs; rw [← mul_one (cexp _)]
     congr
     convert exp_int_mul_two_pi_mul_I (-1) using 2
     ring
-  . rw [mul_add, exp_add]
+  · rw [mul_add, exp_add]
     conv => rhs; rw [← mul_one (cexp _)]
     congr
     convert exp_int_mul_two_pi_mul_I (-Int.ofNat N) using 2
     simp
     ring
-  . congr 1
+  · congr 1
     rw [mul_add, exp_add]
     conv => rhs; rw [← mul_one (cexp _)]
     congr
diff --git a/Carleson/Classical/VanDerCorput.lean b/Carleson/Classical/VanDerCorput.lean
index 6bfe2e7b..dee287c4 100644
--- a/Carleson/Classical/VanDerCorput.lean
+++ b/Carleson/Classical/VanDerCorput.lean
@@ -12,7 +12,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
   have hK : 0 ≤ K * (b - a) / 2 := by
     apply mul_nonneg (mul_nonneg (by simp) (by linarith)) (by norm_num)
   by_cases n_nonzero : n = 0
-  . rw [n_nonzero]
+  · rw [n_nonzero]
     simp only [Int.cast_zero, mul_zero, zero_mul, exp_zero, one_mul, abs_zero,
       add_zero, inv_one, mul_one]
     calc ‖∫ (x : ℝ) in a..b, ϕ x‖
@@ -21,18 +21,18 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         linarith
       _ ≤ B * (MeasureTheory.volume (Set.Ioo a b)).toReal := by
         apply MeasureTheory.norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
-        . exact fun x hx ↦ (h2 x hx)
-        . exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
+        · 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)]
       _ = 1 * (b - a) * B := by ring
       _ ≤ 2 * Real.pi * (b - a) * (↑B + ↑K * (b - a) / 2) := by
         gcongr
-        . exact mul_nonneg Real.two_pi_pos.le (by linarith)
-        . exact sub_nonneg_of_le hab
-        . linarith [Real.two_le_pi]
-        . exact (le_add_iff_nonneg_right ↑B).mpr hK
+        · exact mul_nonneg Real.two_pi_pos.le (by linarith)
+        · exact sub_nonneg_of_le hab
+        · linarith [Real.two_le_pi]
+        · exact (le_add_iff_nonneg_right ↑B).mpr hK
   wlog n_pos : 0 < n generalizing n ϕ
-  . /-We could do calculations analogous to those below. Instead, we apply the positive
+  · /-We could do calculations analogous to those below. Instead, we apply the positive
     case to the complex conjugate.-/
     push_neg at n_pos
     calc ‖∫ (x : ℝ) in a..b, cexp (I * ↑n * ↑x) * ϕ x‖
@@ -44,22 +44,22 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         rw [map_mul, ← exp_conj]
         congr
         simp
-        exact Or.inl (conj_ofReal _)
+        -- exact Or.inl (conj_ofReal _)
       _ ≤ 2 * Real.pi * (b - a) * (↑B + ↑K * (b - a) / 2) * (1 + ↑|-n| * (b - a))⁻¹ := by
         apply this
-        . intro x y
+        · intro x y
           simp only [Function.comp_apply]
           rw [edist_eq_coe_nnnorm_sub, ← map_sub, starRingEnd_apply, nnnorm_star, ← edist_eq_coe_nnnorm_sub]
           exact h1 _ _
-        . intro x hx
+        · 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
+        · 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.
   by_cases h : b - a < Real.pi / n
-  . have : 0 < 1 + ↑|n| * (b - a) := by
+  · have : 0 < 1 + ↑|n| * (b - a) := by
       apply add_pos_of_pos_of_nonneg zero_lt_one
       apply mul_nonneg (by simp) (by linarith)
     calc _
@@ -68,10 +68,10 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         linarith
       _ ≤ B * (MeasureTheory.volume (Set.Ioo a b)).toReal := by
         apply MeasureTheory.norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
-        . intro x hx
+        · 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
-        . exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
+        · exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
       _ = B * (b - a) := by rw [Real.volume_Ioo, ENNReal.toReal_ofReal (by linarith)]
       _ = (1 + |n| * (b - a)) * (1 + |n| * (b - a))⁻¹ * (b - a) * B := by
         rw [mul_inv_cancel]
@@ -79,16 +79,16 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         exact ne_of_gt this
       _ ≤ (Real.pi + Real.pi) * (1 + |n| * (b - a))⁻¹ * (b - a) * (B + K * (b - a) / 2) := by
         gcongr
-        . apply mul_nonneg
+        · apply mul_nonneg
           apply mul_nonneg
           linarith [Real.two_pi_pos]
           · exact inv_nonneg_of_nonneg this.le
           · linarith
-        . linarith
-        . linarith [Real.two_le_pi]
-        . rw [mul_comm, _root_.abs_of_nonneg n_pos.le]
+        · linarith
+        · linarith [Real.two_le_pi]
+        · rw [mul_comm, _root_.abs_of_nonneg n_pos.le]
           exact mul_le_of_nonneg_of_le_div Real.pi_pos.le (by exact_mod_cast n_pos.le) h.le
-        . simpa
+        · simpa
       _ = 2 * Real.pi * (b - a) * (B + K * (b - a) / 2) * (1 + |n| * (b - a))⁻¹ := by ring
   push_neg at h
   have pi_div_n_pos : 0 < Real.pi / n := div_pos Real.pi_pos (Int.cast_pos.mpr n_pos)
@@ -174,15 +174,15 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
                  + (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
       gcongr
-      . apply MeasureTheory.norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
-        . intro x hx
+      · apply MeasureTheory.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
-        . intro x _
+        · exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
+      · apply MeasureTheory.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]
           apply le_trans (h1.dist_le_mul _ _)
@@ -190,14 +190,14 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
           rw [_root_.abs_of_nonneg Real.pi_pos.le, _root_.abs_of_nonneg (by simp; linarith [n_pos])]
           apply le_of_eq
           ring
-        . exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
-      . apply MeasureTheory.norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
-        . intro x hx
+        · exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
+      · apply MeasureTheory.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
+        · exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
     _ = Real.pi / n * (B + K * (b - (a + Real.pi / n)) / 2) := by
       rw [Real.volume_Ioo, Real.volume_Ioo, Real.volume_Ioo, ENNReal.toReal_ofReal, ENNReal.toReal_ofReal, ENNReal.toReal_ofReal]
       ring
diff --git a/Carleson/DiscreteCarleson.lean b/Carleson/DiscreteCarleson.lean
index 607157ae..7fc0929c 100644
--- a/Carleson/DiscreteCarleson.lean
+++ b/Carleson/DiscreteCarleson.lean
@@ -26,7 +26,7 @@ def aux𝔐 (k n : ℕ) : Set (𝔓 X) :=
   {p ∈ TilesAt k | 2 ^ (-n : ℤ) * volume (𝓘 p : Set X) < volume (E₁ p) }
 
 /-- The definition `𝔐(k, n)` given in (5.1.4) and (5.1.5). -/
-def 𝔐 (k n : ℕ) : Set (𝔓 X) := maximals (·≤·) (aux𝔐 k n)
+def 𝔐 (k n : ℕ) : Set (𝔓 X) := {m | Maximal (aux𝔐 k n) m}
 
 /-- The definition `dens'_k(𝔓')` given in (5.1.6). -/
 def dens' (k : ℕ) (P' : Set (𝔓 X)) : ℝ≥0∞ :=
@@ -179,7 +179,7 @@ lemma setA_subset_iUnion_𝓒 {l k n : ℕ} :
   obtain ⟨p, hp⟩ := mx
   simp_rw [Finset.mem_filter, Finset.mem_univ, true_and, 𝔐] at hp
   rw [mem_iUnion₂]; use 𝓘 p, ?_, hp.2
-  have hp' : p ∈ aux𝔐 k n := mem_of_mem_of_subset hp.1 (maximals_subset ..)
+  have hp' : p ∈ aux𝔐 k n := mem_of_mem_of_subset hp.1 (fun _ h ↦ h.prop)
   rw [aux𝔐, mem_setOf, TilesAt, mem_preimage] at hp'
   exact hp'.1
 
@@ -330,7 +330,7 @@ lemma pairwiseDisjoint_E1 : (𝔐 (X := X) k n).PairwiseDisjoint E₁ := fun p m
   rw [mem_preimage] at mxp mxp'
   have l𝓘 := Grid.le_def.mpr ⟨(fundamental_dyadic hs).resolve_right (disjoint_comm.not.mpr h𝓘), hs⟩
   have sΩ := (relative_fundamental_dyadic l𝓘).resolve_left <| not_disjoint_iff.mpr ⟨_, mxp', mxp⟩
-  exact (eq_of_mem_maximals mp' (mem_of_mem_of_subset mp (maximals_subset ..)) ⟨l𝓘, sΩ⟩).symm
+  exact mp'.eq_of_ge mp.prop ⟨l𝓘, sΩ⟩
 
 /-- Lemma 5.2.4 -/
 lemma dyadic_union (hx : x ∈ setA l k n) : ∃ i : Grid X, x ∈ i ∧ (i : Set X) ⊆ setA l k n := by
@@ -431,7 +431,9 @@ lemma john_nirenberg_aux2 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n))
     calc
       _ ≤ ∑ q ∈ Q₁, 2 ^ n * volume (E₁ q) := by
         refine Finset.sum_le_sum fun q mq ↦ ?_
-        simp_rw [Q₁, Finset.mem_filter, 𝔐, maximals, aux𝔐, mem_setOf] at mq
+        simp_rw [Q₁, Finset.mem_filter, 𝔐, mem_setOf] at mq
+        change _ ∧ Maximal (· ∈ aux𝔐 k n) q ∧ _ at mq
+        simp_rw [aux𝔐, mem_setOf] at mq
         replace mq := mq.2.1.1.2
         rw [← ENNReal.rpow_intCast, show (-(n : ℕ) : ℤ) = (-n : ℝ) by simp, mul_comm,
           ← ENNReal.lt_div_iff_mul_lt (by simp) (by simp), ENNReal.div_eq_inv_mul,
@@ -442,7 +444,7 @@ lemma john_nirenberg_aux2 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n))
   calc
     _ = ∫⁻ x in setA (X := X) (l + 1) k n ∩ L, 2 ^ (n + 1) := (setLIntegral_const _ _).symm
     _ ≤ ∫⁻ x in setA (X := X) (l + 1) k n ∩ L, ∑ q ∈ Q₁, (𝓘 q : Set X).indicator 1 x := by
-      refine setLIntegral_mono (by simp) (Finset.measurable_sum Q₁ Q₁m) fun x ⟨mx, mx₂⟩ ↦ ?_
+      refine setLIntegral_mono (Finset.measurable_sum Q₁ Q₁m) fun x ⟨mx, mx₂⟩ ↦ ?_
       have : 2 ^ (n + 1) ≤ ∑ q ∈ Q₁, (𝓘 q : Set X).indicator 1 x := by
         convert john_nirenberg_aux1 mL mx mx₂
         simp_rw [stackSize, Q₁, mem_setOf_eq]
@@ -1036,7 +1038,9 @@ lemma ordConnected_C2 : OrdConnected (ℭ₂ k n j : Set (𝔓 X)) := by
   by_cases e : p = p'; · rwa [e] at mp
   simp_rw [ℭ₂, layersAbove, mem_diff, mp'₁, true_and]
   by_contra h; rw [mem_iUnion₂] at h; obtain ⟨l', bl', p'm⟩ := h
-  rw [minLayer, mem_minimals_iff] at p'm
+  rw [minLayer, mem_setOf] at p'm
+  change Minimal (· ∈ ℭ₁ k n j \ ⋃ (k' < l'), (ℭ₁ k n j).minLayer k') p' at p'm
+  rw [minimal_iff] at p'm
   have pnm : p ∉ ⋃ l'', ⋃ (_ : l'' < l'), 𝔏₁ k n j l'' := by
     replace mp := mp.2; contrapose! mp
     exact mem_of_mem_of_subset mp
@@ -1063,7 +1067,9 @@ lemma ordConnected_C4 : OrdConnected (ℭ₄ k n j : Set (𝔓 X)) := by
   by_cases e : p' = p''; · rwa [← e] at mp''
   simp_rw [ℭ₄, layersBelow, mem_diff, mp'₁, true_and]
   by_contra h; simp_rw [mem_iUnion] at h; obtain ⟨l', hl', p'm⟩ := h
-  rw [maxLayer_def, mem_maximals_iff] at p'm; simp_rw [mem_diff] at p'm
+  rw [maxLayer_def, mem_setOf] at p'm
+  change Maximal (· ∈ ℭ₃ k n j \ ⋃ (k' < l'), (ℭ₃ k n j).maxLayer k') p' at p'm
+  rw [maximal_iff] at p'm; simp_rw [mem_diff] at p'm
   have p''nm : p'' ∉ ⋃ l'', ⋃ (_ : l'' < l'), 𝔏₃ k n j l'' := by
     replace mp'' := mp''.2; contrapose! mp''
     refine mem_of_mem_of_subset mp'' <| iUnion₂_mono' fun i hi ↦ ⟨i, hi.le.trans hl', subset_rfl⟩
diff --git a/Carleson/ForestOperator.lean b/Carleson/ForestOperator.lean
index 377991fa..906c7484 100644
--- a/Carleson/ForestOperator.lean
+++ b/Carleson/ForestOperator.lean
@@ -33,7 +33,7 @@ def 𝓙₀ (G : Set (𝔓 X)) : Set (Grid X) :=
 
 /-- The definition of `𝓙(G), defined below Lemma 7.1.1 -/
 def 𝓙 (G : Set (𝔓 X)) : Set (Grid X) :=
-  maximals (·≤·) (𝓙₀ G)
+  {x | Maximal (𝓙₀ G) x}
 
 /-- The definition of `𝓛₀(G), defined below Lemma 7.1.1 -/
 def 𝓛₀ (G : Set (𝔓 X)) : Set (Grid X) :=
@@ -41,7 +41,7 @@ def 𝓛₀ (G : Set (𝔓 X)) : Set (Grid X) :=
 
 /-- The definition of `𝓛(G), defined below Lemma 7.1.1 -/
 def 𝓛 (G : Set (𝔓 X)) : Set (Grid X) :=
-  maximals (·≤·) (𝓛₀ G)
+  {x | Maximal (𝓛₀ G) x}
 
 @[simp]
 lemma biUnion_𝓙 : ⋃ J ∈ 𝓙 G, J = ⋃ I : Grid X, (I : Set X) := by
@@ -100,5 +100,5 @@ theorem forest_operator {n : ℕ} (𝔉 : Forest X n) {f g : X → ℂ}
     ‖∫ x, conj (g x) * ∑ u ∈ Finset.univ.filter (· ∈ 𝔉.𝔘),
       ∑ p ∈ Finset.univ.filter (· ∈ 𝔉.𝔗 u), T p f x‖₊ ≤
     C2_0_4 a q n * (dens₂ (X := X) (⋃ u ∈ 𝔉.𝔘, 𝔉.𝔗 u)) ^ (q⁻¹ - 2⁻¹) *
-    snorm f 2 volume * snorm g 2 volume := by
+    eLpNorm f 2 volume * eLpNorm g 2 volume := by
   sorry
diff --git a/Carleson/Psi.lean b/Carleson/Psi.lean
index 0be2e5af..2911585e 100644
--- a/Carleson/Psi.lean
+++ b/Carleson/Psi.lean
@@ -582,7 +582,7 @@ private lemma norm_Ks_sub_Ks_le₁ {s : ℤ} {x y y' : X} (hK : Ks s x y ≠ 0)
   apply le_trans <| add_le_add norm_Ks_le norm_Ks_le
   rw [div_mul_eq_mul_div, div_add_div_same, ← two_mul,
     div_le_div_right (measure_ball_pos_real x (D ^ s) (D_pow0' (D1 X) s)), ← pow_one 2]
-  rw [not_le, ← div_lt_iff' two_pos] at h
+  rw [not_le, ← _root_.div_lt_iff' two_pos] at h
   have dist_pos : dist y y' > 0 := lt_of_le_of_lt (div_nonneg dist_nonneg two_pos.le) h
   have := lt_of_le_of_lt
     ((div_le_div_right two_pos).2 ((mem_Icc.1 <| dist_mem_Icc_of_Ks_ne_zero hK).1)) h
diff --git a/Carleson/TileExistence.lean b/Carleson/TileExistence.lean
index ede9683a..00cceb52 100644
--- a/Carleson/TileExistence.lean
+++ b/Carleson/TileExistence.lean
@@ -129,7 +129,7 @@ lemma property_set_nonempty (k:ℤ): (if k = S then ({o}:Set X) else ∅) ∈ pr
 
 variable (X) in
 lemma chain_property_set_has_bound (k : ℤ):
-    ∀ c ⊆ property_set X k, IsChain (. ⊆ .) c → ∃ ub ∈ property_set X k,
+    ∀ c ⊆ property_set X k, IsChain (· ⊆ ·) c → ∃ ub ∈ property_set X k,
     ∀ s ∈ c, s ⊆ ub := by
   intro c hc hchain
   use (⋃ s ∈ c,s) ∪ (if k = S then {o} else ∅)
@@ -1788,7 +1788,7 @@ lemma forget_map_inj : Function.Injective (forget_map X) := by
   intro x1 x2 h
   dsimp only [forget_map] at h
   simp only [Sigma.mk.inj_iff, Subtype.mk.injEq] at h
-  exact (𝓓.ext_iff x1 x2).mpr h
+  exact 𝓓.ext_iff.mpr h
 
 variable (X) in
 def 𝓓_finite : Finite (𝓓 X) := by
diff --git a/Carleson/ToMathlib/Height.lean b/Carleson/ToMathlib/Height.lean
index 639be315..c14f95b7 100644
--- a/Carleson/ToMathlib/Height.lean
+++ b/Carleson/ToMathlib/Height.lean
@@ -380,9 +380,8 @@ lemma subtype_mk_minimal_iff (α : Type*) [Preorder α]
   change Minimal (· ∈ t) _ ↔ _
   rw [← OrderEmbedding.minimal_mem_image_iff
     (f := ⟨Function.Embedding.subtype (· ∈ s), by simp⟩) hxt]
-  simp only [RelEmbedding.coe_mk, Function.Embedding.coe_subtype, Set.mem_image, Subtype.exists,
+  simp_rw [RelEmbedding.coe_mk, Function.Embedding.coe_subtype, Set.mem_image, Subtype.exists,
     exists_and_right, exists_eq_right, exists_and_left]
-  congr! 2 with x'
-  change _ ↔ x' ∈ s ∧ _
-  rw [iff_and_self, forall_exists_index]
-  exact fun hy _ ↦ hy
+  congr! 2
+  rw [setOf, iff_and_self, forall_exists_index]
+  exact fun h _ ↦ h
diff --git a/Carleson/ToMathlib/MinLayer.lean b/Carleson/ToMathlib/MinLayer.lean
index 80837b71..236d0634 100644
--- a/Carleson/ToMathlib/MinLayer.lean
+++ b/Carleson/ToMathlib/MinLayer.lean
@@ -27,7 +27,7 @@ variable {α : Type*} [PartialOrder α]
 
 /-- The `n`th minimal layer of `A`. -/
 def minLayer (A : Set α) (n : ℕ) : Set α :=
-  minimals (· ≤ ·) (A \ ⋃ (k < n), A.minLayer k)
+  {a | Minimal (A \ ⋃ (k < n), A.minLayer k) a}
 
 /-- The `n`th maximal layer of `A`. -/
 def maxLayer (A : Set α) (n : ℕ) : Set α :=
@@ -43,12 +43,12 @@ def layersBelow (A : Set α) (n : ℕ) : Set α :=
 
 variable {A : Set α} {m n : ℕ} {a : α}
 
-lemma maxLayer_def : A.maxLayer n = maximals (· ≤ ·) (A \ ⋃ (k < n), A.maxLayer k) := by
+lemma maxLayer_def : A.maxLayer n = {a | Maximal (A \ ⋃ (k < n), A.maxLayer k) a} := by
   rw [maxLayer, minLayer]; rfl
 
 lemma minLayer_subset : A.minLayer n ⊆ A :=
   calc
-    _ ⊆ A \ ⋃ (k < n), A.minLayer k := by rw [minLayer]; exact minimals_subset ..
+    _ ⊆ A \ ⋃ (k < n), A.minLayer k := by rw [minLayer]; exact fun _ h ↦ h.prop
     _ ⊆ A := diff_subset
 
 lemma maxLayer_subset : A.maxLayer n ⊆ A := minLayer_subset
@@ -57,14 +57,16 @@ lemma layersAbove_subset : A.layersAbove n ⊆ A := diff_subset
 
 lemma layersBelow_subset : A.layersBelow n ⊆ A := diff_subset
 
-lemma minLayer_zero : A.minLayer 0 = minimals (· ≤ ·) A := by rw [minLayer]; simp
+lemma minLayer_zero : A.minLayer 0 = {a | Minimal A a} := by
+  rw [minLayer]; congr!; simpa using fun _ _ ↦ id
 
-lemma maxLayer_zero : A.maxLayer 0 = maximals (· ≤ ·) A := by rw [maxLayer_def]; simp
+lemma maxLayer_zero : A.maxLayer 0 = {a | Maximal A a} := by
+  rw [maxLayer_def]; congr!; simpa using fun _ _ ↦ id
 
 lemma disjoint_minLayer_of_ne (h : m ≠ n) : Disjoint (A.minLayer m) (A.minLayer n) := by
   wlog hl : m < n generalizing m n; · exact (this h.symm (by omega)).symm
   rw [disjoint_right]; intro p hp
-  rw [minLayer, mem_minimals_iff, mem_diff] at hp; replace hp := hp.1.2; contrapose! hp
+  rw [minLayer] at hp; replace hp := hp.1.2; contrapose! hp
   exact mem_iUnion₂_of_mem hl hp
 
 lemma disjoint_maxLayer_of_ne (h : m ≠ n) : Disjoint (A.maxLayer m) (A.maxLayer n) :=
@@ -77,10 +79,10 @@ lemma pairwiseDisjoint_maxLayer : univ.PairwiseDisjoint A.maxLayer := fun _ _ _
   disjoint_minLayer_of_ne
 
 lemma isAntichain_minLayer : IsAntichain (· ≤ ·) (A.minLayer n) := by
-  rw [minLayer]; apply minimals_antichain
+  rw [minLayer]; apply setOf_minimal_antichain
 
 lemma isAntichain_maxLayer : IsAntichain (· ≤ ·) (A.maxLayer n) := by
-  rw [maxLayer_def]; apply maximals_antichain
+  rw [maxLayer_def]; apply setOf_maximal_antichain
 
 lemma exists_le_in_minLayer_of_le (ha : a ∈ A.minLayer n) (hm : m ≤ n) :
     ∃ c ∈ A.minLayer m, c ≤ a := by
@@ -89,10 +91,10 @@ lemma exists_le_in_minLayer_of_le (ha : a ∈ A.minLayer n) (hm : m ≤ n) :
   | succ n _ ih =>
     have nma : a ∉ A.minLayer n :=
       disjoint_right.mp (disjoint_minLayer_of_ne (by omega)) ha
-    rw [minLayer, mem_minimals_iff] at ha nma
-    have al : a ∈ A \ ⋃ (l < n), A.minLayer l := by
-      refine mem_of_mem_of_subset ha.1 (diff_subset_diff_right ?_)
-      refine biUnion_subset_biUnion_left fun k hk ↦ ?_
+    rw [minLayer, mem_setOf, minimal_iff] at ha nma
+    have al : (A \ ⋃ (l < n), A.minLayer l) a := by
+      have ha1 : a ∈ A \ ⋃ (k < n + 1), A.minLayer k := ha.1
+      refine (diff_subset_diff_right (biUnion_subset_biUnion_left fun k hk ↦ ?_)) ha1
       rw [mem_def, Nat.le_eq] at hk ⊢; omega
     simp_rw [al, true_and] at nma; push_neg at nma; obtain ⟨a', ha', la⟩ := nma
     have ma' : a' ∈ A.minLayer n := by
@@ -102,7 +104,8 @@ lemma exists_le_in_minLayer_of_le (ha : a ∈ A.minLayer n) (hm : m ≤ n) :
         simp_rw [this, iUnion_or, iUnion_union_distrib]
         simp only [iUnion_iUnion_eq_left, mem_diff, mem_union, mem_iUnion, exists_prop, not_or,
           not_exists, not_and] at ha' ⊢
-        tauto
+        change a' ∈ A ∧ a' ∉ ⋃ (k < n), A.minLayer k at ha'
+        rw [mem_iUnion₂] at ha'; push_neg at ha'; tauto
       exact absurd (ha.2 a'l la.1) (ne_eq _ _ ▸ la.2)
     obtain ⟨c, mc, lc⟩ := ih ma'; use c, mc, lc.trans la.1
 
@@ -122,19 +125,16 @@ lemma minLayer_eq_setOf_height : A.minLayer n = {x | ∃ hx : x ∈ A, height (
     rw [minLayer]
     simp_rw [← mem_minimal_le_height_iff_height]
     simp (config := {contextual := true}) only [ih]; clear ih
-    rw [subtype_mk_mem_minimals_iff]
-    congr! 2
-    ext y
-    wlog hys : y ∈ A
-    · simp [hys]
+    simp_rw [subtype_mk_minimal_iff, mem_setOf_eq, exists_and_left]
+    congr! 1; ext y; rw [Pi.sdiff_apply]
+    change y ∈ A ∧ y ∉ ⋃ (k < n), _ ↔ y ∈ A ∧ _
+    rw [and_congr_right_iff]; intro hys
     simp only [mem_diff, hys, mem_iUnion, exists_prop, not_exists, not_and, true_and, mem_setOf_eq,
       exists_and_left, exists_true_left]
     cases height (⟨y, hys⟩ : A)
     · simp
     · simp only [Nat.cast_inj, Nat.cast_le]
-      constructor
-      · intro h; contrapose! h; simp [h]
-      · intro h m hm; omega
+      exact ⟨fun h ↦ by contrapose! h; simp [h], fun h m hm ↦ by omega⟩
 
 /-- `A` equals the union of its `minLayer`s up to `n` iff
 all `LTSeries` in `A` have length at most `n`. -/
@@ -180,8 +180,9 @@ lemma exists_le_in_layersAbove_of_le (ha : a ∈ A.layersAbove n) (hm : m ≤ n)
     not_and, mem_toFinset] at ma' mina'
   conv at mina' => enter [x]; rw [and_imp]
   have ma'₁ : a' ∈ A.minLayer n := by
-    rw [minLayer, mem_minimals_iff]
-    simp_rw [mem_diff, mem_iUnion, exists_prop, not_exists, not_and]
+    rw [minLayer, mem_setOf]
+    change Minimal (· ∈ A \ ⋃ k, ⋃ (_ : k < n), A.minLayer k) _
+    simp_rw [minimal_iff, mem_diff, mem_iUnion, exists_prop, not_exists, not_and]
     exact ⟨ma'.1, fun y hy ly ↦ (eq_of_le_of_not_lt ly (mina' y hy (ly.trans ma'.2))).symm⟩
   obtain ⟨c, mc, lc⟩ := exists_le_in_minLayer_of_le ma'₁ hm
   use c, mc, lc.trans ma'.2