chore: replace omega by cutsat

omega is going to vanish in the medium term; cutsat's implementation
(based on grind) is much more maintainable. Switch to it, when possible.

Almost all cases can be converted, except for one in GridStructure,
one in LargeSeparation and three in Truncation.

Author: grunweg

Carleson/Antichain/AntichainOperator.lean

@@ -248,7 +248,7 @@ lemma le_C6_1_4 (a4 : 4 ≤ a) :
   simp_rw [Tile.C6_1_5, Antichain.C6_1_6, C6_1_4, ← pow_add, ← pow_mul]
   gcongr
   · exact one_le_two
-  · have : 𝕔 / 4 ≤ 2 * (𝕔 / 8) + 1 := by omega
+  · have : 𝕔 / 4 ≤ 2 * (𝕔 / 8) + 1 := by cutsat
     have : (𝕔 / 4) * a ^ 3 ≤ 2 * (𝕔 / 8) * a ^ 3 + a ^ 3 :=
       (mul_le_mul_of_nonneg_right this (Nat.zero_le _)).trans_eq (by ring)
     ring_nf

Carleson/Antichain/AntichainTileCount.lean

@@ -133,11 +133,11 @@ lemma pairwiseDisjoint_𝔄_aux {𝔄 : Set (𝔓 X)} {ϑ : Θ X} :
     univ.PairwiseDisjoint (fun N ↦ (𝔄_aux 𝔄 ϑ N).toFinset) := fun i mi j mj hn ↦ by
   change Disjoint (𝔄_aux _ _ _).toFinset ((𝔄_aux _ _ _).toFinset)
   wlog hl : i < j generalizing i j
-  · exact (this _ mj _ mi hn.symm (by omega)).symm
+  · exact (this _ mj _ mi hn.symm (by cutsat)).symm
   simp_rw [Finset.disjoint_left, 𝔄_aux, mem_toFinset, mem_setOf_eq, not_and, and_imp]
   refine fun p mp md _ ↦ ?_
   rw [mem_Ico, not_and_or, not_le]
-  exact Or.inl <| md.2.trans_le (pow_le_pow_right₀ one_le_two (by omega))
+  exact Or.inl <| md.2.trans_le (pow_le_pow_right₀ one_le_two (by cutsat))
 
 open Classical in
 lemma biUnion_𝔄_aux {𝔄 : Set (𝔓 X)} {ϑ : Θ X} :
@@ -894,7 +894,7 @@ private lemma le_C6_3_4 (ha : 4 ≤ a) :
     (((2 : ℝ≥0∞) ^ (a * (N + 5)) + 2 ^ (a * N + a * 3)) * 2 ^ (𝕔 * a ^ 3 + 5 * a)) +
       2 ^ (a * (N + 5)) ≤ C6_3_4 a N := by
   simp only [add_mul, ← pow_add, C6_3_4, one_mul, ENNReal.coe_pow, ENNReal.coe_ofNat]
-  apply add_le_pow_two₃ le_rfl (by linarith) (by omega) ?_
+  apply add_le_pow_two₃ le_rfl (by linarith) (by cutsat) ?_
   ring_nf
   linarith [sixteen_times_le_cube ha]
 
@@ -1038,7 +1038,7 @@ lemma tile_count_aux {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄
       · refine fun p mp ↦ pow_nonneg (mul_nonneg ?_ (indicator_nonneg (by simp) _)) _
         exact mul_nonneg (Real.rpow_nonneg zero_le_two _) (indicator_nonneg (by simp) _)
       simp_rw [enorm_pow, enorm_mul, mul_pow]
-      have an0 : a ≠ 0 := by omega
+      have an0 : a ≠ 0 := by cutsat
       congr! 3 with p mp
       · rw [Real.rpow_mul zero_le_two, ENNReal.rpow_mul,
           Real.enorm_rpow_of_nonneg (by positivity) (by positivity), Real.rpow_neg zero_le_two,
@@ -1063,13 +1063,13 @@ lemma tile_count_aux {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄
       · rw [neg_sub_left, ← mul_one_add, neg_mul, neg_mul, neg_le_neg_iff, mul_assoc]
         gcongr; push_cast
         calc
-          _ ≤ 3⁻¹ * (4 * a : ℝ) := by rw [le_inv_mul_iff₀ zero_lt_three]; norm_cast; omega
+          _ ≤ 3⁻¹ * (4 * a : ℝ) := by rw [le_inv_mul_iff₀ zero_lt_three]; norm_cast; cutsat
           _ = (3 * a ^ 3 : ℝ)⁻¹ * (4 * a ^ 4) := by
             rw [pow_succ' _ 3, ← mul_assoc 4, ← div_eq_inv_mul, ← div_eq_inv_mul,
               mul_div_mul_right _ _ (by positivity)]
           _ ≤ _ := by
             rw [show (3 * a ^ 3 : ℝ) = 2 * a ^ 3 + a ^ 3 by ring]; gcongr
-            · norm_cast; omega
+            · norm_cast; cutsat
             · norm_num
       · exact global_antichain_density h𝔄 ϑ n
     _ = _ := by
@@ -1104,7 +1104,7 @@ lemma le_C6_1_6 (a4 : 4 ≤ a) :
     _ ≤ _ := by
       rw [C6_1_6]; norm_cast; rw [← pow_add]; gcongr
       · exact one_le_two
-      · omega
+      · cutsat
 
 open Classical in
 /-- Lemma 6.1.6. -/

Carleson/Antichain/Basic.lean

@@ -131,7 +131,7 @@ lemma norm_Ks_le' {x y : X} {𝔄 : Set (𝔓 X)} (p : 𝔄) (hxE : x ∈ E ↑p
   apply h.trans
   rw [zpow_sub₀ (by simp), zpow_one, div_div]
   apply (ineq_6_1_7 x p).trans
-  have ha : 6 * a + (𝕔 + 1) * a ^ 3 = (5 * a + (𝕔 + 1) * a ^ 3) + a := by omega
+  have ha : 6 * a + (𝕔 + 1) * a ^ 3 = (5 * a + (𝕔 + 1) * a ^ 3) + a := by cutsat
   simp only [div_eq_mul_inv, ge_iff_le]
   rw [ha, pow_add _ (5 * a + (𝕔 + 1) * a ^ 3) a, mul_assoc]
   apply mul_le_mul_of_nonneg_left _ (zero_le _)
@@ -212,7 +212,7 @@ lemma maximal_bound_antichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤
         rw [C6_1_2, add_comm (5 * a), add_assoc]; norm_cast
         apply pow_le_pow_right₀ one_le_two
         ring_nf
-        suffices 6 * a ≤ a ^ 3 by omega
+        suffices 6 * a ≤ a ^ 3 by cutsat
         linarith [sixteen_times_le_cube (four_le_a X)]
       · exact lt_of_le_of_lt hdist_cp
           (mul_lt_mul_of_nonneg_of_pos (by linarith) (le_refl _) (by linarith) hDpow_pos)

Carleson/Antichain/TileCorrelation.lean

@@ -154,9 +154,9 @@ lemma correlation_kernel_bound {s₁ s₂ : ℤ} {x₁ x₂ : X} (hs : s₁ ≤
       rw [← pow_mul]
       apply add_le_pow_two ?_ le_rfl ?_
       · ring_nf
-        omega
+        cutsat
       · ring_nf
-        suffices 1 ≤ a ^ 3 by omega
+        suffices 1 ≤ a ^ 3 by cutsat
         exact one_le_pow₀ (by linarith [four_le_a X])
 
 variable [TileStructure Q D κ S o]
@@ -272,13 +272,13 @@ lemma uncertainty' (ha : 1 ≤ a) {p₁ p₂ : 𝔓 X} (hle : 𝔰 p₁ ≤ 𝔰
             apply add_le_add_right
             norm_cast
             nth_rw 1 [← pow_one 2]
-            exact Nat.pow_le_pow_right zero_lt_two (by omega)
+            exact Nat.pow_le_pow_right zero_lt_two (by cutsat)
           _ = 2 * (2 : ℝ) ^ (6 * a) := by ring
           _ ≤ _ := by
             nth_rw 1 [← pow_one 2, ← pow_add]
             norm_cast
-            exact Nat.pow_le_pow_right zero_lt_two (by omega)
-      have h38 : 3 ≤ 8 := by omega
+            exact Nat.pow_le_pow_right zero_lt_two (by cutsat)
+      have h38 : 3 ≤ 8 := by cutsat
       have h12 : (1 : ℝ) ≤ 2 := by norm_num
       rw [C6_2_3]
       conv_rhs => ring_nf
@@ -367,7 +367,7 @@ lemma I12_le' {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ} (x1 : E
     norm_cast
     gcongr
     · exact one_le_two
-    · omega
+    · cutsat
 
 private lemma exp_ineq (ha : 4 ≤ a) : 0 < (8 * a : ℕ) * -(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹ + 1 := by
   have hpos : 0 < (a : ℝ) ^ 2 * 2 + a ^ 3 := by positivity
@@ -389,7 +389,7 @@ lemma I12_le (ha : 4 ≤ a) {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X 
   rw [pow_add 2 _ 1, pow_one, mul_comm _ 2, mul_assoc, mul_comm 2 (_ * _), mul_assoc]
   gcongr
   -- Now we need to use Lemma 6.2.3 to conclude this inequality.
-  have h623 := uncertainty (by omega) hle hinter x1.2 x2.2
+  have h623 := uncertainty (by cutsat) hle hinter x1.2 x2.2
   rw [C6_2_3, ENNReal.coe_pow, ENNReal.coe_ofNat] at h623
   have hneg : -(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹ < 0 :=
     neg_neg_iff_pos.mpr (inv_pos.mpr (by norm_cast; nlinarith))

Carleson/Calculations.lean

@@ -86,7 +86,7 @@ lemma calculation_3 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x y
   rw [← distrib_three_right ..]
   calc (100 + 4 * (D : ℝ) ^ (-2 : ℝ) + 8⁻¹ * D ^ (-3 : ℝ)) * D ^ (x + 3)
   _ ≤ (100 + 4 * (D : ℝ) ^ (-2 : ℝ) + 8⁻¹ * D ^ (-3 : ℝ)) * D ^ (y - 1) := by
-    have h1 : x + 3 ≤ y - 1 := by omega
+    have h1 : x + 3 ≤ y - 1 := by cutsat
     gcongr
     linarith [four_le_realD X]
   _ = (100 + 4 * (D : ℝ) ^ (-2 : ℝ) + 8⁻¹ * D ^ (-3 : ℝ)) * (D ^ (y) * D ^ (- 1 : ℝ)) := by
@@ -272,7 +272,7 @@ lemma calculation_7_7_4 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G]
     · norm_num
     gcongr
     · norm_num
-    omega
+    cutsat
   exact Nat.mul_le_mul this (Nat.le_add_left 1 n)
 
 /-- A bound on the sum of a geometric series whose ratio is close to 1. -/
@@ -340,12 +340,12 @@ lemma calculation_150 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :
 
 lemma sq_le_two_pow_of_four_le (a4 : 4 ≤ a) : a ^ 2 ≤ 2 ^ a := by
   induction a, a4 using Nat.le_induction with
-  | base => omega
+  | base => cutsat
   | succ a a4 ih =>
     rw [pow_succ 2, mul_two, add_sq, one_pow, mul_one, add_assoc]; gcongr
     calc
-      _ ≤ 3 * a := by omega
-      _ ≤ a * a := by gcongr; omega
+      _ ≤ 3 * a := by cutsat
+      _ ≤ a * a := by gcongr; cutsat
       _ ≤ _ := by rwa [← sq]
 
 lemma calculation_6_1_6 (a4 : 4 ≤ a) : 8 * a ^ 4 ≤ 2 ^ (2 * a + 3) := by

Carleson/Classical/HilbertStrongType.lean

@@ -389,10 +389,10 @@ lemma norm_dirichletApprox_le {n : ℕ} {x : ℝ} :
     have : (i : ℕ) < 2 * n := by
       simp only [Finset.mem_Ico] at hi
       exact hi.2
-    have : 2 * i + 1 ≤ 4 * n := by omega
+    have : 2 * i + 1 ≤ 4 * n := by cutsat
     exact_mod_cast this
   _ ≤ _ := by
-    simp only [Finset.sum_const, Nat.card_Ico, show 2 * n - n = n by omega, nsmul_eq_mul,
+    simp only [Finset.sum_const, Nat.card_Ico, show 2 * n - n = n by cutsat, nsmul_eq_mul,
       ← mul_assoc]
     rcases eq_zero_or_pos n with rfl | hn
     · simp

Carleson/Discrete/Defs.lean

@@ -21,11 +21,11 @@ def 𝓒 (k : ℕ) : Set (Grid X) :=
 def TilesAt (k : ℕ) : Set (𝔓 X) := 𝓘 ⁻¹' 𝓒 k
 
 lemma disjoint_TilesAt_of_ne {m n : ℕ} (h : m ≠ n) : Disjoint (TilesAt (X := X) m) (TilesAt n) := by
-  wlog hl : m < n generalizing m n; · exact (this h.symm (by omega)).symm
+  wlog hl : m < n generalizing m n; · exact (this h.symm (by cutsat)).symm
   by_contra! h; rw [not_disjoint_iff] at h; obtain ⟨p, mp₁, mp₂⟩ := h
   simp_rw [TilesAt, mem_preimage, 𝓒, mem_diff, aux𝓒, mem_setOf] at mp₁ mp₂
   apply absurd _ mp₂.2; obtain ⟨j, lj, vj⟩ := mp₁.1; use j, lj; apply lt_of_le_of_lt _ vj
-  exact mul_le_mul_right' (ENNReal.zpow_le_of_le one_le_two (by omega)) _
+  exact mul_le_mul_right' (ENNReal.zpow_le_of_le one_le_two (by cutsat)) _
 
 lemma pairwiseDisjoint_TilesAt : univ.PairwiseDisjoint (TilesAt (X := X)) := fun _ _ _ _ ↦
   disjoint_TilesAt_of_ne
@@ -56,11 +56,11 @@ lemma ℭ_subset_TilesAt {k n : ℕ} : ℭ k n ⊆ TilesAt (X := X) k := fun t m
   rw [ℭ, mem_setOf] at mt; exact mt.1
 
 lemma disjoint_ℭ_of_ne {k m n : ℕ} (h : m ≠ n) : Disjoint (ℭ (X := X) k m) (ℭ k n) := by
-  wlog hl : m < n generalizing m n; · exact (this h.symm (by omega)).symm
+  wlog hl : m < n generalizing m n; · exact (this h.symm (by cutsat)).symm
   by_contra! h; rw [not_disjoint_iff] at h; obtain ⟨p, mp₁, mp₂⟩ := h
   apply absurd _ (not_disjoint_iff.mpr ⟨_, mp₁.2, mp₂.2⟩)
   rw [Ioc_disjoint_Ioc, le_max_iff]; left; rw [min_le_iff]; right
-  exact ENNReal.zpow_le_of_le one_le_two (by omega)
+  exact ENNReal.zpow_le_of_le one_le_two (by cutsat)
 
 lemma pairwiseDisjoint_ℭ :
     (univ : Set (ℕ × ℕ)).PairwiseDisjoint (fun kn ↦ ℭ (X := X) kn.1 kn.2) :=
@@ -130,11 +130,11 @@ lemma ℭ₁_subset_ℭ {k n j : ℕ} : ℭ₁ k n j ⊆ ℭ (X := X) k n := fun
   rw [ℭ₁, preℭ₁, mem_diff, mem_setOf] at mt; exact mt.1.1
 
 lemma disjoint_ℭ₁_of_ne {k n j l : ℕ} (h : j ≠ l) : Disjoint (ℭ₁ (X := X) k n j) (ℭ₁ k n l) := by
-  wlog hl : j < l generalizing j l; · exact (this h.symm (by omega)).symm
+  wlog hl : j < l generalizing j l; · exact (this h.symm (by cutsat)).symm
   by_contra! h; rw [not_disjoint_iff] at h; obtain ⟨p, mp₁, mp₂⟩ := h
   simp_rw [ℭ₁, mem_diff, preℭ₁, mem_setOf, mp₁.1.1, true_and, not_le] at mp₁ mp₂
   have := mp₂.1.trans_lt mp₁.2
-  rw [pow_lt_pow_iff_right₀ one_lt_two] at this; omega
+  rw [pow_lt_pow_iff_right₀ one_lt_two] at this; cutsat
 
 lemma pairwiseDisjoint_ℭ₁ {k n : ℕ} : univ.PairwiseDisjoint (ℭ₁ (X := X) k n) := fun _ _ _ _ ↦
   disjoint_ℭ₁_of_ne
@@ -317,7 +317,7 @@ lemma setA_subset_iUnion_𝓒 {l k n : ℕ} :
 lemma setA_subset_setA {l k n : ℕ} : setA (X := X) (l + 1) k n ⊆ setA l k n := by
   refine setOf_subset_setOf.mpr fun x hx ↦ ?_
   calc
-    _ ≤ _ := by gcongr; omega
+    _ ≤ _ := by gcongr; cutsat
     _ < _ := hx
 
 lemma measurable_setA {l k n : ℕ} : MeasurableSet (setA (X := X) l k n) :=

Carleson/Discrete/ExceptionalSet.lean

@@ -247,7 +247,7 @@ lemma john_nirenberg_aux1 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n))
         refine stackSize_mono <| sep_subset ..
       _ ≤ l * 2 ^ (n + 1) := by rwa [setA, mem_setOf_eq, not_lt] at nx'
   -- so the (unchanged) first sum of RHS is at least `2 ^ (n + 1)`
-  rw [add_one_mul] at mx; omega
+  rw [add_one_mul] at mx; cutsat
 
 /-- Equation (5.2.11) in the proof of Lemma 5.2.5. -/
 lemma john_nirenberg_aux2 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) :
@@ -314,7 +314,7 @@ lemma john_nirenberg : volume (setA (X := X) l k n) ≤ 2 ^ (k + 1 - l : ℤ) *
     suffices 2 * volume (setA (X := X) (l + 1) k n) ≤ volume (setA (X := X) l k n) by
       rw [← ENNReal.mul_le_mul_left (a := 2) (by simp) (by simp), ← mul_assoc]; apply this.trans
       convert ih using 2; nth_rw 1 [← zpow_one 2, ← ENNReal.zpow_add (by simp) (by simp)]
-      congr 1; omega
+      congr 1; cutsat
     calc
       _ = 2 * ∑ L ∈ Grid.maxCubes (MsetA (X := X) l k n),
           volume (setA (X := X) (l + 1) k n ∩ L) := by
@@ -358,11 +358,11 @@ lemma second_exception : volume (G₂ (X := X)) ≤ 2 ^ (-2 : ℤ) * volume G :=
       rw [ENNReal.tsum_comm]; congr!; split_ifs <;> simp
     _ ≤ ∑' (k : ℕ) (n : ℕ), if k ≤ n then 2 ^ (k - 5 - 2 * n : ℤ) * volume G else 0 := by
       gcongr; split_ifs
-      · convert john_nirenberg using 3; omega
+      · convert john_nirenberg using 3; cutsat
       · rfl
     _ = ∑' (k : ℕ), 2 ^ (-k - 5 : ℤ) * volume G * ∑' (n' : ℕ), 2 ^ (- 2 * n' : ℤ) := by
       congr with k -- n' = n - k - 1; n = n' + k + 1
-      have rearr : ∀ n : ℕ, (k - 5 - 2 * n : ℤ) = (-k - 5 + (-2 * (n - k)) : ℤ) := by omega
+      have rearr : ∀ n : ℕ, (k - 5 - 2 * n : ℤ) = (-k - 5 + (-2 * (n - k)) : ℤ) := by cutsat
       conv_lhs =>
         enter [1, n]
         rw [rearr, ENNReal.zpow_add (by simp) (by simp), ← mul_rotate,
@@ -413,7 +413,7 @@ lemma lintegral_Ioc_layervol_one {l : ℕ} :
       unfold layervol; congr with x; constructor <;> intro h
       · rw [indicator_sum_eq_natCast, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le]
         rw [indicator_sum_eq_natCast, ← Nat.ceil_le] at h; convert h; symm
-        rwa [Nat.ceil_eq_iff (by omega), add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]
+        rwa [Nat.ceil_eq_iff (by cutsat), add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]
       · exact ht.2.trans h
     _ = layervol k n (l + 1) * volume (Ioc (l : ℝ) (l + 1)) := setLIntegral_const ..
     _ = _ := by rw [Real.volume_Ioc, add_sub_cancel_left, ENNReal.ofReal_one, mul_one]
@@ -503,7 +503,7 @@ lemma top_tiles : ∑ m with m ∈ 𝔐 (X := X) k n, volume (𝓘 m : Set X) 
     _ = _ := by
       nth_rw 3 [← pow_one 2]
       rw [mul_rotate, ← pow_add, ← mul_assoc, ← pow_add,
-        show n + 1 + (k + 1 + 1) = n + k + 3 by omega]
+        show n + 1 + (k + 1 + 1) = n + k + 3 by cutsat]
 
 end TopTiles
 
@@ -957,7 +957,7 @@ lemma third_exception : volume (G₃ (X := X)) ≤ 2 ^ (-4 : ℤ) * volume G :=
       calc
       4 + (9 * a + 6)
       _ = 9 * a + 10 := by ring
-      _ ≤ 3 * 4 * a + 4 * 4 := by omega
+      _ ≤ 3 * 4 * a + 4 * 4 := by cutsat
       _ ≤ 3 * a * a + a * a := by gcongr <;> linarith [four_le_a X]
       _ = 4 * a ^ 2 := by ring
       _ ≤ 𝕔 * a ^ 2 := by

Carleson/Discrete/ForestComplement.lean

@@ -117,8 +117,8 @@ lemma exists_k_n_of_mem_𝔓pos (h : p ∈ 𝔓pos (X := X)) : ∃ k n, p ∈ 
       ENNReal.toReal_le_toReal dens'_lt_top.ne (by simp)]
     exact_mod_cast dens'_le
   have klq : k ≤ ⌊v⌋₊ := Nat.le_floor klv
-  let n : ℕ := 4 * a + ⌊v⌋₊ + 1; use n; refine ⟨⟨mp, ?_⟩, by omega⟩
-  rw [show 4 * (a : ℤ) - (4 * a + ⌊v⌋₊ + 1 : ℕ) = (-⌊v⌋₊ - 1 : ℤ) by omega, sub_add_cancel, mem_Ioc,
+  let n : ℕ := 4 * a + ⌊v⌋₊ + 1; use n; refine ⟨⟨mp, ?_⟩, by cutsat⟩
+  rw [show 4 * (a : ℤ) - (4 * a + ⌊v⌋₊ + 1 : ℕ) = (-⌊v⌋₊ - 1 : ℤ) by cutsat, sub_add_cancel, mem_Ioc,
     ← ENNReal.ofReal_toReal dens'_lt_top.ne, ← ENNReal.rpow_intCast, ← ENNReal.rpow_intCast,
     show (2 : ℝ≥0∞) = ENNReal.ofReal (2 : ℝ) by norm_cast,
     ENNReal.ofReal_rpow_of_pos zero_lt_two, ENNReal.ofReal_rpow_of_pos zero_lt_two,
@@ -137,7 +137,7 @@ private lemma two_mul_n_add_six_lt : 2 * n + 6 < 2 ^ (n + 3) := by
     calc
       _ = 2 * n + 6 + 2 := by ring
       _ < 2 ^ (n + 3) + 2 := by gcongr
-      _ < 2 ^ (n + 3) + 2 ^ (n + 3) := by omega
+      _ < 2 ^ (n + 3) + 2 ^ (n + 3) := by cutsat
       _ = _ := by ring
 
 lemma exists_j_of_mem_𝔓pos_ℭ (h : p ∈ 𝔓pos (X := X)) (mp : p ∈ ℭ k n) (hkn : k ≤ n) :
@@ -163,13 +163,13 @@ lemma exists_j_of_mem_𝔓pos_ℭ (h : p ∈ 𝔓pos (X := X)) (mp : p ∈ ℭ k
           Finset.filter_filter]; rfl
       _ ≤ (2 * n + 6) * 2 ^ (n + 1) := by rwa [setA, mem_setOf, not_lt] at nx
       _ < _ := by
-        rw [show 2 * n + 4 = (n + 3) + (n + 1) by omega, pow_add _ (n + 3)]
+        rw [show 2 * n + 4 = (n + 3) + (n + 1) by cutsat, pow_add _ (n + 3)]
         exact mul_lt_mul_of_pos_right two_mul_n_add_six_lt (by positivity)
   rcases B.eq_zero_or_pos with Bz | Bpos
   · simp_rw [B, filter_mem_univ_eq_toFinset, Finset.card_eq_zero, toFinset_eq_empty] at Bz
     exact Or.inl ⟨mp, Bz⟩
   · right; use Nat.log 2 B; rw [← Nat.log_lt_iff_lt_pow one_lt_two Bpos.ne'] at Blt
-    refine ⟨by omega, (?_ : _ ∧ _ ≤ B), (?_ : ¬(_ ∧ _ ≤ B))⟩
+    refine ⟨by cutsat, (?_ : _ ∧ _ ≤ B), (?_ : ¬(_ ∧ _ ≤ B))⟩
     · exact ⟨mp, Nat.pow_log_le_self 2 Bpos.ne'⟩
     · rw [not_and, not_le]; exact fun _ ↦ Nat.lt_pow_succ_log_self one_lt_two _
 
@@ -379,7 +379,7 @@ lemma lt_quotient_rearrange :
   congr 1
   rw [ENNReal.coe_pow, ENNReal.coe_ofNat, ← zpow_natCast,
     ← ENNReal.zpow_add two_ne_zero ENNReal.ofNat_ne_top]
-  congr 1; omega
+  congr 1; cutsat
 
 lemma l_upper_bound : l < 2 ^ n := by
   have ql1 : volume (E₂ l p') / volume (𝓘 p' : Set X) ≤ 1 := by
@@ -441,7 +441,7 @@ lemma iUnion_L0' : ⋃ (l < n), 𝔏₀' (X := X) k n l = 𝔏₀ k n := by
   suffices ¬∃ s : LTSeries (𝔏₀ (X := X) k n), s.length = n by
     rcases lt_or_ge p.length n with c | c
     · exact c
-    · exact absurd ⟨p.take ⟨n, by omega⟩, by rw [RelSeries.take_length]⟩ this
+    · exact absurd ⟨p.take ⟨n, by cutsat⟩, by rw [RelSeries.take_length]⟩ this
   by_contra h; obtain ⟨s, hs⟩ := h; let sl := s.last; have dsl := sl.2.1.2.1
   simp_rw [dens', lt_iSup_iff, mem_singleton_iff, exists_prop, exists_eq_left] at dsl
   obtain ⟨l, hl, p', mp', sp', qp'⟩ := dsl
@@ -507,7 +507,7 @@ lemma iUnion_L0' : ⋃ (l < n), 𝔏₀' (X := X) k n l = 𝔏₀ k n := by
       simp [div_pow]; ring
     _ ≤ 1 + 2 * (2 / 256) ^ 0 + (1 / 256) ^ 0 * 3 := by
       gcongr 1 + 2 * ?_ + ?_ * 3 <;>
-        exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by omega)
+        exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by cutsat)
     _ < _ := by norm_num
 
 /-- Part of Lemma 5.5.2 -/
@@ -1019,7 +1019,7 @@ lemma lintegral_carlesonSum_𝔓₁_compl_le_sum_aux1 [ProofData a q K σ₁ σ
   _ = 2 ^ (28 * a + 20) / (q - 1) ^ 4 := by
     simp only [← pow_add]
     congr
-    omega
+    cutsat
 
 omit [TileStructure Q D κ S o] in
 lemma lintegral_carlesonSum_𝔓₁_compl_le_sum_aux2 {N : ℕ} :
@@ -1079,7 +1079,7 @@ lemma C5_1_3_optimized_le_C5_1_3 : C5_1_3_optimized a nnq ≤ C5_1_3 a nnq := by
       have := four_le_a X
       gcongr; · exact one_le_two
       calc
-        _ ≤ 3 * 4 * 4 * a := by omega
+        _ ≤ 3 * 4 * 4 * a := by cutsat
         _ ≤ 3 * a * a * a := by gcongr
         _ = _ := by ring
     _ = 2 ^ ((𝕔 + 5 + 𝕔 / 8) * a ^ 3 + 3 * a ^ 3) / (nnq - 1) ^ (4 + 1) := by