chore: replace some uses of lia with omega

Author: euprunin

Mathlib/Analysis/Analytic/Order.lean

@@ -320,7 +320,7 @@ theorem AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero {x : 𝕜} (hf :
     · contrapose! hf'
       simp_rw [sub_eq_iff_eq_add] at hfF
       rw [EventuallyEq.deriv_eq hfF, deriv_add_const, deriv_fun_smul (by fun_prop) (by fun_prop),
-        deriv_fun_pow (by fun_prop), sub_self, zero_pow (by omega), zero_pow (by omega),
+        deriv_fun_pow (by fun_prop), sub_self, zero_pow (by lia), zero_pow (by lia),
         mul_zero, zero_mul, zero_smul, zero_smul, add_zero]
 
 lemma natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero [CharZero 𝕜] [CompleteSpace E]

Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean

@@ -315,7 +315,7 @@ lemma shiftFunctorCompIsoId_op_inv_app (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m =
         (shiftFunctorOpIso C m n (by omega)).inv.app (Opposite.op (X.unop⟦m⟧)) ≫
           ((shiftFunctorOpIso C n m hnm).inv.app X)⟦m⟧' := by
   simp [shiftFunctorCompIsoId, shiftFunctorZero_op_inv_app X,
-    shiftFunctorAdd'_op_hom_app X n m 0 hnm m n 0 hnm (by omega) (add_zero 0)]
+    shiftFunctorAdd'_op_hom_app X n m 0 hnm m n 0 hnm (by lia) (add_zero 0)]
 
 set_option backward.isDefEq.respectTransparency false in
 @[reassoc]

Mathlib/LinearAlgebra/Lagrange.lean

@@ -507,7 +507,7 @@ theorem leadingCoeff_eq_sum
   replace hP : #s = deg + 1 := WithBot.coe_eq_coe.mp hP
   have hdegree : P.degree = ↑(#s - 1) := hdeg.symm.trans (WithBot.coe_eq_coe.mpr (by grind))
   rw [leadingCoeff, natDegree_eq_of_degree_eq_some hdegree]
-  exact coeff_eq_sum hvs (by rw [hdegree]; norm_cast; omega)
+  exact coeff_eq_sum hvs (by rw [hdegree]; norm_cast; lia)
 
 end Interpolate
 

Mathlib/Order/Interval/Finset/Gaps.lean

@@ -92,7 +92,7 @@ theorem intervalGapsWithin_snd_of_lt (hj : j < k) :
   congr
   ext
   simp only [coe_castPred, val_natCast, Nat.mod_succ_eq_iff_lt]
-  omega
+  lia
 
 theorem intervalGapsWithin_mapsTo : (Set.Iio k).MapsTo
     (fun (j : ℕ) ↦ ((F.intervalGapsWithin h a b j).2, (F.intervalGapsWithin h a b j.succ).1))
@@ -128,7 +128,7 @@ theorem intervalGapsWithin_le_fst {a b : α} (hFab : ∀ ⦃z⦄, z ∈ F → a
   by_cases hj : j = 0
   · simp [hj]
   · have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j - 1) (by grind))
-    have hj₀ : j - 1 + 1 = j := by omega
+    have hj₀ : j - 1 + 1 = j := by lia
     simp only [Nat.succ_eq_add_one, hj₀] at this
     grind
 

Mathlib/RingTheory/Finiteness/Ideal.lean

@@ -63,7 +63,7 @@ theorem exists_radical_pow_le_of_fg {R : Type*} [CommSemiring R] (I : Ideal R) (
     refine fun i _ => mul_le_right.trans ?_
     obtain h | h := le_or_gt n i
     · exact mul_le_right.trans ((pow_le_pow_right h).trans hn)
-    · exact mul_le_left.trans ((pow_le_pow_right (by omega)).trans hm)
+    · exact mul_le_left.trans ((pow_le_pow_right (by lia)).trans hm)
 
 theorem exists_pow_le_of_le_radical_of_fg_radical {R : Type*} [CommSemiring R] {I J : Ideal R}
     (hIJ : I ≤ J.radical) (hJ : J.radical.FG) :

Mathlib/RingTheory/PowerSeries/Schroder.lean

@@ -76,19 +76,19 @@ lemma coeff_X_mul_largeSchroderSeriesSeries_sq (n : ℕ) (hn : 0 < n) :
     split
     next h =>
       simp_all only [mul_eq_mul_right_iff]
-      simp [coeff_X_mul_largeSchroderSeries x (by omega)]
+      simp [coeff_X_mul_largeSchroderSeries x (by lia)]
     next h =>
       simp_all only [not_lt, nonpos_iff_eq_zero, coeff_zero_eq_constantCoeff, map_mul,
       constantCoeff_X, constantCoeff_largeSchroderSeries, mul_one, tsub_zero, zero_mul]
-  rw [this, sum_range_eq_add_Ico _ (by omega)]
+  rw [this, sum_range_eq_add_Ico _ (by lia)]
   simp only [lt_self_iff_false, reduceIte, zero_add]
   have : (∑ x ∈ Ico 1 n, if 0 < x then largeSchroder (x - 1) * largeSchroder (n - x) else 0) =
     ∑ x ∈ Ico 1 n, largeSchroder (x - 1) * largeSchroder (n - x) := by
     apply sum_congr rfl
     intros x hx
     have hx' : 0 < x := by grind
     rw [if_pos hx']
-  rw [this, sum_Ico_eq_sum_range, show n = n - 1 + 1 by omega,
+  rw [this, sum_Ico_eq_sum_range, show n = n - 1 + 1 by lia,
     sum_range_succ]
   grind [largeSchroder_zero]