chore: replace omega with lia where possible (#32666)

As previously discussed, we'd like to move users off `omega` and on to `lia` (which is the linear integer arithmetic module from `grind`, plus a controlled set of instantiated lemmas).

This does not yet remove all uses of `omega` in Mathlib.

Author: kim-em

Archive/Imo/Imo1960Q1.lean

@@ -45,14 +45,14 @@ theorem ge_100 {n : ℕ} (h1 : ProblemPredicate n) : 100 ≤ n := by
     rw [← h1.left]
     refine Nat.base_pow_length_digits_le 10 n ?_ (not_zero h1)
     simp
-  omega
+  lia
 
 theorem lt_1000 {n : ℕ} (h1 : ProblemPredicate n) : n < 1000 := by
   have h2 : n < 10 ^ 3 := by
     rw [← h1.left]
     refine Nat.lt_base_pow_length_digits ?_
     simp
-  omega
+  lia
 
 /-
 We do an exhaustive search to show that all results are covered by `SolutionPredicate`.
@@ -70,7 +70,7 @@ theorem searchUpTo_step {c n} (H : SearchUpTo c n) {c' n'} (ec : c + 1 = c') (en
   refine ⟨by ring, fun m l p => ?_⟩
   obtain ⟨h₁, ⟨m, rfl⟩, h₂⟩ := id p
   by_cases h : 11 * m < c * 11; · exact H _ h p
-  obtain rfl : m = c := by omega
+  obtain rfl : m = c := by lia
   rw [Nat.mul_div_cancel_left _ (by simp : 11 > 0), mul_comm] at h₂
   refine (H' h₂).imp ?_ ?_ <;> · rintro rfl; norm_num
 

Archive/Imo/Imo1962Q1.lean

@@ -53,31 +53,31 @@ Now we can eliminate possibilities for `(digits 10 c).length` until we get to th
 lemma case_0_digits {c n : ℕ} (hc : (digits 10 c).length = 0) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 0 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_1_digits {c n : ℕ} (hc : (digits 10 c).length = 1) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 1 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_2_digits {c n : ℕ} (hc : (digits 10 c).length = 2) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 2 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_3_digits {c n : ℕ} (hc : (digits 10 c).length = 3) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 3 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_4_digits {c n : ℕ} (hc : (digits 10 c).length = 4) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 4 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 /-- Putting this inline causes a deep recursion error, so we separate it out. -/
 private lemma helper_5_digits {c : ℤ} (hc : 6 * 10 ^ 5 + c = 4 * (10 * c + 6)) : c = 15384 := by
-  omega
+  lia
 
 lemma case_5_digits {c n : ℕ} (hc : (digits 10 c).length = 5) (hpp : ProblemPredicate' c n) :
     c = 15384 := by

Archive/Imo/Imo1985Q2.lean

@@ -51,22 +51,22 @@ lemma C_mul_mod {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n) (cpj : Nat.C
     have nej : (k + 1) * j % n ≠ j := by
       by_contra! h; nth_rw 2 [← Nat.mod_eq_of_lt hj.2, ← one_mul j] at h
       replace h : (k + 1) % n = 1 % n := Nat.ModEq.cancel_right_of_coprime cpj h
-      rw [Nat.mod_eq_of_lt hk.2, Nat.mod_eq_of_lt (by omega)] at h
-      omega
+      rw [Nat.mod_eq_of_lt hk.2, Nat.mod_eq_of_lt (by lia)] at h
+      lia
     have b₁ : (k + 1) * j % n ∈ Set.Ico 1 n := by
-      refine ⟨?_, Nat.mod_lt _ (by omega)⟩
+      refine ⟨?_, Nat.mod_lt _ (by lia)⟩
       by_contra! h; rw [Nat.lt_one_iff, ← Nat.dvd_iff_mod_eq_zero] at h
       have ek := Nat.eq_zero_of_dvd_of_lt (cpj.dvd_of_dvd_mul_right h) hk.2
-      omega
+      lia
     rw [← ih ⟨hk₁, Nat.lt_of_succ_lt hk.2⟩, hC.2 _ b₁ nej]
     rcases nej.lt_or_gt with h | h
     · rw [Int.natAbs_natCast_sub_natCast_of_ge h.le]
       have b₂ : j - (k + 1) * j % n ∈ Set.Ico 1 n :=
         ⟨Nat.sub_pos_iff_lt.mpr h, (Nat.sub_le ..).trans_lt hj.2⟩
       have q : n - (j - (k + 1) * j % n) = (k + 1) * j % n + (n - j) % n := by
         rw [tsub_tsub_eq_add_tsub_of_le h.le, add_comm, Nat.add_sub_assoc hj.2.le,
-          Nat.mod_eq_of_lt (show n - j < n by omega)]
-      rw [hC.1 _ b₂, q, ← Nat.add_mod_of_add_mod_lt (by omega), ← Nat.add_sub_assoc hj.2.le,
+          Nat.mod_eq_of_lt (show n - j < n by lia)]
+      rw [hC.1 _ b₂, q, ← Nat.add_mod_of_add_mod_lt (by lia), ← Nat.add_sub_assoc hj.2.le,
         add_comm, Nat.add_sub_assoc (Nat.le_mul_of_pos_left _ hk.1), ← tsub_one_mul,
         Nat.add_mod_left, add_tsub_cancel_right]
     · rw [Int.natAbs_natCast_sub_natCast_of_le h.le, Nat.mod_sub_of_le h.le]
@@ -75,13 +75,13 @@ lemma C_mul_mod {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n) (cpj : Nat.C
 theorem result {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n) (cpj : Coprime n j)
     {C : ℕ → Fin 2} (hC : Condition n j C) {i : ℕ} (hi : i ∈ Set.Ico 1 n) :
     C i = C j := by
-  obtain ⟨v, -, hv⟩ := exists_mul_mod_eq_one_of_coprime cpj.symm (by omega)
+  obtain ⟨v, -, hv⟩ := exists_mul_mod_eq_one_of_coprime cpj.symm (by lia)
   have hvi : i = (v * i % n) * j % n := by
     rw [mod_mul_mod, ← mul_rotate, ← mod_mul_mod, hv, one_mul, mod_eq_of_lt hi.2]
   have vib : v * i % n ∈ Set.Ico 1 n := by
-    refine ⟨(?_ : 0 < _), mod_lt _ (by omega)⟩
+    refine ⟨(?_ : 0 < _), mod_lt _ (by lia)⟩
     by_contra! h; rw [le_zero, ← dvd_iff_mod_eq_zero] at h
-    rw [mul_comm, ← mod_eq_of_lt (show 1 < n by omega)] at hv
+    rw [mul_comm, ← mod_eq_of_lt (show 1 < n by lia)] at hv
     have i0 := eq_zero_of_dvd_of_lt
       ((coprime_of_mul_modEq_one _ hv).symm.dvd_of_dvd_mul_left h) hi.2
     subst i; simp at hi

Archive/Imo/Imo1988Q6.lean

@@ -239,7 +239,7 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
     · contrapose! hV₀ with x_lt_z
       apply ne_of_gt
       calc
-        z * y > x * x := by apply mul_lt_mul' <;> omega
+        z * y > x * x := by apply mul_lt_mul' <;> lia
         _ ≥ x * x - k := sub_le_self _ (Int.natCast_nonneg k)
   · -- There is no base case in this application of Vieta jumping.
     simp
@@ -276,16 +276,16 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
     constructor
     · have zy_pos : z * y ≥ 0 := by rw [hV₀]; exact mod_cast Nat.zero_le _
       apply nonneg_of_mul_nonneg_left zy_pos
-      omega
+      lia
     · contrapose! hV₀ with x_lt_z
       apply ne_of_gt
       push_neg at h_base
       calc
-        z * y > x * y := by apply mul_lt_mul_of_pos_right <;> omega
-        _ ≥ x * (x + 1) := by apply mul_le_mul <;> omega
+        z * y > x * y := by apply mul_lt_mul_of_pos_right <;> lia
+        _ ≥ x * (x + 1) := by apply mul_le_mul <;> lia
         _ > x * x + 1 := by
           rw [mul_add]
-          omega
+          lia
   · -- Show the base case.
     intro x y h h_base
     obtain rfl | rfl : x = 0 ∨ x = 1 := by rwa [Nat.le_add_one_iff, Nat.le_zero] at h_base

Archive/Imo/Imo1994Q1.lean

@@ -37,7 +37,7 @@ theorem tedious (m : ℕ) (k : Fin (m + 1)) : m - ((m + 1 - ↑k) + m) % (m + 1)
   rcases hk with ⟨c, rfl⟩
   have : (k + c + 1 - k) + (k + c) = c + (k + c + 1) := by lia
   rw [Fin.val_mk, this, Nat.add_mod_right, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
-  omega
+  lia
 
 end Imo1994Q1
 

Archive/Imo/Imo1997Q3.lean

@@ -74,7 +74,7 @@ lemma sign_eq_of_contra
   | one => rfl
   | mul_right p s sform ih =>
     suffices |S x p - S x (p * s)| ≤ (n + 1 : ℕ) + 1 by
-      rw [ih]; exact sign_eq_of_abs_sub_le (h _) (h _) (by norm_cast; omega) this
+      rw [ih]; exact sign_eq_of_abs_sub_le (h _) (h _) (by norm_cast; lia) this
     rw [Set.mem_range] at sform; obtain ⟨i, hi⟩ := sform
     iterate 2 rw [S, ← sum_add_sum_compl {i.castSucc, i.succ}]
     have cg : ∑ j ∈ {i.castSucc, i.succ}ᶜ, (j + 1) * x ((p * s) j) =
@@ -99,16 +99,16 @@ lemma S_one_add_S_revPerm
   nth_rw 2 [S]; rw [← revPerm.sum_comp _ _ (by simp)]
   simp_rw [revPerm_apply, val_rev, rev_rev, S, Perm.one_apply, ← sum_add_distrib, ← add_mul]
   have cg : ∑ i : Fin n, (i + 1 + ((n - (i + 1) : ℕ) + 1)) * x i = ∑ i, (n + 1) * x i := by
-    congr! 2 with i; norm_cast; omega
-  rw [cg, ← mul_sum, abs_mul, hx₁, mul_one]; exact abs_of_nonneg (by norm_cast; omega)
+    congr! 2 with i; norm_cast; lia
+  rw [cg, ← mul_sum, abs_mul, hx₁, mul_one]; exact abs_of_nonneg (by norm_cast; lia)
 
 theorem result {x : Fin n → ℝ} (hx₁ : |∑ i, x i| = 1) (hx₂ : ∀ i, |x i| ≤ (n + 1) / 2) :
     ∃ p, |S x p| ≤ (n + 1) / 2 := by
   match n with
   | 0 => simp [S]
   | n + 1 =>
     by_contra! h
-    exact (lt_abs_add_of_sign_eq (h _) (h _) (by norm_cast; omega)
+    exact (lt_abs_add_of_sign_eq (h _) (h _) (by norm_cast; lia)
       (sign_eq_of_contra hx₂ h _)).ne' (S_one_add_S_revPerm hx₁)
 
 end Imo1997Q3

Archive/Imo/Imo2001Q3.lean

@@ -66,7 +66,7 @@ lemma card_not_easy_le_five {i : Fin 21} (hG : #(G i) ≤ 6) (hB : ∀ j, ¬Disj
     _ = #((G i).biUnion fun p ↦ {j | p ∈ B j}) := by congr 1; ext j; simp [not_disjoint_iff]
     _ ≤ ∑ p ∈ G i, #{j | p ∈ B j} := card_biUnion_le
     _ ≤ ∑ p ∈ G i, 2 := sum_le_sum fun p mp ↦ Nat.le_of_lt_succ (h p mp)
-    _ ≤ _ := by rw [sum_const, smul_eq_mul]; omega
+    _ ≤ _ := by rw [sum_const, smul_eq_mul]; lia
 
 open Classical in
 /-- There are at most 210 girl-boy pairs who solved some problem in common that was not easy for

Archive/Imo/Imo2001Q6.lean

@@ -22,9 +22,9 @@ variable {a b c d : ℤ}
 theorem imo2001_q6 (hd : 0 < d) (hdc : d < c) (hcb : c < b) (hba : b < a)
     (h : a * c + b * d = (a + b - c + d) * (-a + b + c + d)) : ¬Prime (a * b + c * d) := by
   intro (h0 : Prime (a * b + c * d))
-  have ha : 0 < a := by omega
-  have hb : 0 < b := by omega
-  have hc : 0 < c := by omega
+  have ha : 0 < a := by lia
+  have hb : 0 < b := by lia
+  have hc : 0 < c := by lia
   -- the key step is to show that `a*c + b*d` divides the product `(a*b + c*d) * (a*d + b*c)`
   have dvd_mul : a * c + b * d ∣ (a * b + c * d) * (a * d + b * c) := by
     use b ^ 2 + b * d + d ^ 2

Archive/Imo/Imo2008Q3.lean

@@ -45,7 +45,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
     simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
     rw [pow_two, ← hy]; exact neg_add_cancel 1
   have hnat₂ : n ≤ p / 2 := ZMod.natAbs_valMinAbs_le y
-  have hnat₃ : p ≥ 2 * n := by omega
+  have hnat₃ : p ≥ 2 * n := by lia
   set k : ℕ := p - 2 * n with hnat₄
   have hnat₅ : p ∣ k ^ 2 + 4 := by
     obtain ⟨x, hx⟩ := hnat₁

Archive/Imo/Imo2015Q6.lean

@@ -73,9 +73,9 @@ lemma exists_add_eq_of_mem_pool {z : ℤ} (hz : z ∈ pool a t) : ∃ u < t, u +
     simp_rw [pool, mem_map, Equiv.coe_toEmbedding, Equiv.subRight_apply] at hz
     obtain ⟨y, my, ey⟩ := hz
     rw [mem_insert, mem_erase] at my; rcases my with h | h
-    · use t; omega
+    · use t; lia
     · obtain ⟨u, lu, hu⟩ := ih h.2
-      use u; omega
+      use u; lia
 
 include ha
 
@@ -86,10 +86,10 @@ lemma pool_subset_Icc : ∀ {t}, pool a t ⊆ Icc 0 2014
     intro x hx
     simp_rw [pool, mem_map, Equiv.coe_toEmbedding, Equiv.subRight_apply] at hx
     obtain ⟨y, my, ey⟩ := hx
-    suffices y ∈ Icc 1 2015 by rw [mem_Icc] at this ⊢; omega
+    suffices y ∈ Icc 1 2015 by rw [mem_Icc] at this ⊢; lia
     rw [mem_insert, mem_erase] at my; rcases my with h | ⟨h₁, h₂⟩
     · exact h ▸ ha.1 t
-    · have := pool_subset_Icc h₂; rw [mem_Icc] at this ⊢; omega
+    · have := pool_subset_Icc h₂; rw [mem_Icc] at this ⊢; lia
 
 lemma notMem_pool_self : a t ∉ pool a t := by
   by_contra h
@@ -105,12 +105,12 @@ lemma card_pool_succ : #(pool a (t + 1)) = #(pool a t) + if 0 ∈ pool a t then
     rw [mem_erase, not_and_or]; exact .inr (notMem_pool_self ha)
   rw [pool, card_map, card_insert_of_notMem nms, card_erase_eq_ite]
   split_ifs with h
-  · have := card_pos.mpr ⟨0, h⟩; omega
+  · have := card_pos.mpr ⟨0, h⟩; lia
   · rfl
 
 lemma monotone_card_pool : Monotone fun t ↦ #(pool a t) := by
   refine monotone_nat_of_le_succ fun t ↦ ?_
-  have := card_pool_succ (t := t) ha; omega
+  have := card_pool_succ (t := t) ha; lia
 
 /-- There exists a point where the number of balls reaches a maximum (which follows from its
 monotonicity and boundedness). We take its coordinates for the problem's `b` and `N`. -/
@@ -135,12 +135,12 @@ lemma b_pos : 0 < b := by
     · exact hbN _ h.le
   have cp1 : #(pool a 1) = 1 := by
     simp_rw [card_pool_succ ha, pool, card_empty, notMem_empty, ite_false]
-  apply absurd (hbN 1); omega
+  apply absurd (hbN 1); lia
 
 include ht in
 lemma zero_mem_pool : 0 ∈ pool a t := by
   have := card_pool_succ (t := t) ha
-  have := hbN (t + 1) (by omega)
+  have := hbN (t + 1) (by lia)
   simp_all
 
 include ht in
@@ -151,14 +151,14 @@ lemma sum_sub_sum_eq_sub : ∑ x ∈ pool a (t + 1), x - ∑ x ∈ pool a t, x =
     rw [mem_erase, not_and_or]; exact .inr (notMem_pool_self ha)
   rw [sum_insert nms, sum_erase_eq_sub (h := zero_mem_pool ha hbN ht), sum_sub_distrib, sum_const,
     nsmul_one, hbN _ ht]
-  omega
+  lia
 
 /-- The telescoping sum giving the part of the problem's expression within the modulus signs. -/
 lemma sum_telescope {m n : ℕ} (hm : N ≤ m) (hn : m < n) :
     ∑ j ∈ Ico m n, (a j - b) = ∑ x ∈ pool a n, x - ∑ x ∈ pool a m, x :=
   calc
     _ = ∑ j ∈ Ico m n, (∑ x ∈ pool a (j + 1), x - ∑ x ∈ pool a j, x) := by
-      congr! 1 with j hj; rw [sum_sub_sum_eq_sub ha hbN]; simp at hj; omega
+      congr! 1 with j hj; rw [sum_sub_sum_eq_sub ha hbN]; simp at hj; lia
     _ = _ := sum_Ico_sub (∑ x ∈ pool a ·, x) hn.le
 
 include ht in
@@ -190,7 +190,7 @@ theorem result (ha : Condition a) :
       nth_rw 2 [← Nat.sub_one_add_one_eq_of_pos bp]
       rw [← sum_flip, sum_range_succ, tsub_self, Nat.cast_zero, add_zero, ← sum_sub_distrib]
       have sc : ∀ x ∈ range (b - 1), (2014 - x - (b - 1 - x : ℕ)) = (2015 - b : ℤ) := fun x mx ↦ by
-        rw [mem_range] at mx; omega
+        rw [mem_range] at mx; lia
       rw [sum_congr rfl sc, sum_const, card_range, nsmul_eq_mul, Nat.cast_pred bp]
     _ ≤ _ := by
       rw [← mul_le_mul_iff_right₀ zero_lt_four, ← mul_assoc,