refactor(*): remove some uses of omega in the library (#7620)

In #6129, we stopped using `omega` to avoid porting it to lean4.
Some new uses were added since then.





Co-authored-by: Eric <ericrboidi@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>

archive/100-theorems-list/83_friendship_graphs.lean

@@ -8,7 +8,6 @@ import linear_algebra.char_poly.coeff
 import data.int.modeq
 import data.zmod.basic
 import tactic.interval_cases
-import tactic.omega
 
 /-!
 # The Friendship Theorem
@@ -224,8 +223,7 @@ begin
   iterate 2 {cases k with k, { exfalso, linarith, }, },
   induction k with k hind,
   { exact adj_matrix_sq_mod_p_of_regular hG dmod hd, },
-  have h2 : 2 ≤ k.succ.succ := by omega,
-  rw [pow_succ, hind h2],
+  rw [pow_succ, hind (nat.le_add_left 2 k)],
   exact adj_matrix_mul_const_one_mod_p_of_regular dmod hd,
 end
 
@@ -334,8 +332,7 @@ theorem friendship_theorem [nonempty V] : exists_politician G :=
 begin
   by_contradiction npG,
   rcases hG.is_regular_of_not_exists_politician npG with ⟨d, dreg⟩,
-  have h : d ≤ 2 ∨ 3 ≤ d := by omega,
-  cases h with dle2 dge3,
-  { exact npG (hG.exists_politician_of_degree_le_two dreg dle2) },
+  cases lt_or_le d 3 with dle2 dge3,
+  { exact npG (hG.exists_politician_of_degree_le_two dreg (nat.lt_succ_iff.mp dle2)) },
   { exact hG.false_of_three_le_degree dreg dge3 },
 end

archive/imo/imo1988_q6.lean

@@ -8,7 +8,6 @@ import data.nat.prime
 import data.rat.basic
 import order.well_founded
 import tactic.linarith
-import tactic.omega
 
 /-!
 # IMO 1988 Q6 and constant descent Vieta jumping
@@ -292,6 +291,6 @@ begin
     { simp only [mul_one, one_mul, add_comm, zero_add] at h,
       have y_dvd : y ∣ y * k := dvd_mul_right y k,
       rw [← h, ← add_assoc, nat.dvd_add_left (dvd_mul_left y y)] at y_dvd,
-      obtain rfl|rfl : y = 1 ∨ y = 2 := nat.prime_two.2 y y_dvd,
-      all_goals { ring_nf at h, omega } } }
+      obtain rfl|rfl := (nat.dvd_prime nat.prime_two).mp y_dvd; apply nat.eq_of_mul_eq_mul_left,
+      exacts [zero_lt_one, h.symm, zero_lt_two, h.symm] } }
 end

src/algebra/homology/augment.lean

@@ -30,7 +30,7 @@ def truncate [has_zero_morphisms V] : chain_complex V ℕ ⥤ chain_complex V 
 { obj := λ C,
   { X := λ i, C.X (i+1),
     d := λ i j, C.d (i+1) (j+1),
-    shape' := λ i j w, by { apply C.shape, dsimp at w ⊢, omega, }, },
+    shape' := λ i j w, by { apply C.shape, simpa }, },
   map := λ C D f,
   { f := λ i, f.f (i+1), }, }
 
@@ -67,14 +67,14 @@ def augment (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫
     simp at s,
     rcases i with _|_|i; cases j; unfold_aux; try { simp },
     { simpa using s, },
-    { rw [C.shape], simp, omega, },
+    { rw [C.shape], simpa [← ne.def, nat.succ_ne_succ] using s },
   end,
   d_comp_d' := λ i j k hij hjk, begin
     rcases i with _|_|i; rcases j with _|_|j; cases k; unfold_aux; try { simp },
     cases i,
     { exact w, },
     { rw [C.shape, zero_comp],
-      simp, omega, },
+      simpa using i.succ_succ_ne_one.symm },
   end, }
 
 @[simp] lemma augment_X_zero (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) :
@@ -117,7 +117,7 @@ by { cases i; refl, }
 
 @[simp] lemma chain_complex_d_succ_succ_zero (C : chain_complex V ℕ) (i : ℕ) :
   C.d (i+2) 0 = 0 :=
-by { rw C.shape, simp, omega, }
+by { rw C.shape, simpa using i.succ_succ_ne_one.symm }
 
 /--
 Augmenting a truncated complex with the original object and morphism is isomorphic

src/algebra/homology/single.lean

@@ -189,7 +189,7 @@ def to_single₀_equiv (C : chain_complex V ℕ) (X : V) :
       rcases i with _|_|i; cases j; unfold_aux; simp only [comp_zero, zero_comp, single₀_obj_X_d],
       { rw [C.shape, zero_comp], simp, },
       { exact f.2.symm, },
-      { rw [C.shape, zero_comp], simp only [complex_shape.down_rel, zero_add], omega, },
+      { rw [C.shape, zero_comp], simp [i.succ_succ_ne_one.symm] },
     end, },
   left_inv := λ f, begin
     ext i,

src/algebra/ordered_monoid.lean

@@ -616,6 +616,9 @@ instance canonically_ordered_monoid.has_exists_mul_of_le (α : Type u)
 
 end canonically_ordered_monoid
 
+lemma pos_of_gt {M : Type*} [canonically_ordered_add_monoid M] {n m : M} (h : n < m) : 0 < m :=
+lt_of_le_of_lt (zero_le _) h
+
 /-- A canonically linear-ordered additive monoid is a canonically ordered additive monoid
     whose ordering is a linear order. -/
 @[protect_proj, ancestor canonically_ordered_add_monoid linear_order]

src/number_theory/arithmetic_function.lean

@@ -766,7 +766,7 @@ begin
       use j,
       apply multiset.mem_to_finset.2 hj },
     rw nat.is_unit_iff,
-    omega },
+    norm_num },
 end
 
 @[simp] lemma coe_zeta_mul_coe_moebius [comm_ring R] : (ζ * μ : arithmetic_function R) = 1 :=

src/ring_theory/polynomial/bernstein.lean

@@ -94,9 +94,9 @@ begin
   dsimp [bernstein_polynomial],
   split_ifs,
   { subst h, simp, },
-  { by_cases w : 0 < n - ν,
-    { simp [zero_pow w], },
-    { simp [(show n < ν, by omega), nat.choose_eq_zero_of_lt], }, },
+  { obtain w | w := (n - ν).eq_zero_or_pos,
+    { simp [nat.choose_eq_zero_of_lt ((nat.le_of_sub_eq_zero w).lt_of_ne (ne.symm h))] },
+    { simp [zero_pow w] } },
 end.
 
 lemma derivative_succ_aux (n ν : ℕ) :
@@ -148,9 +148,7 @@ lemma iterate_derivative_at_0_eq_zero_of_lt (n : ℕ) {ν k : ℕ} :
 begin
   cases ν,
   { rintro ⟨⟩, },
-  { intro w,
-    replace w := nat.lt_succ_iff.mp w,
-    revert w,
+  { rw nat.lt_succ_iff,
     induction k with k ih generalizing n ν,
     { simp [eval_at_0], },
     { simp only [derivative_succ, int.coe_nat_eq_zero, int.nat_cast_eq_coe_nat, mul_eq_zero,
@@ -159,12 +157,9 @@ begin
         polynomial.eval_mul, polynomial.eval_nat_cast, polynomial.eval_sub],
       intro h,
       apply mul_eq_zero_of_right,
-      rw ih,
-      simp only [sub_zero],
-      convert @ih (n-1) (ν-1) _,
-      { omega, },
-      { omega, },
-      { exact le_of_lt h, }, }, },
+      rw [ih _ _ (nat.le_of_succ_le h), sub_zero],
+      convert ih _ _ (nat.pred_le_pred h),
+      exact (nat.succ_pred_eq_of_pos (k.succ_pos.trans_le h)).symm } },
 end
 
 @[simp]
@@ -188,17 +183,16 @@ begin
         iterate_derivative_sub, iterate_derivative_cast_nat_mul,
         eval_one, eval_mul, eval_add, eval_sub, eval_X, eval_comp, eval_nat_cast,
         function.comp_app, function.iterate_succ, pochhammer_succ_left],
-      by_cases h'' : ν = 0,
-      { simp [h''] },
-      { have : n - 1 - (ν - 1) = n - ν := by omega,
+      obtain rfl | h'' := ν.eq_zero_or_pos,
+      { simp },
+      { have : n - 1 - (ν - 1) = n - ν,
+        { rw ←nat.succ_le_iff at h'',
+          rw [nat.sub_sub, add_comm, nat.sub_add_cancel h''] },
         rw [this, pochhammer_eval_succ],
-        have : n - ν + ν = n := by omega,
-        rw_mod_cast this } } },
+        rw_mod_cast nat.sub_add_cancel (h'.trans n.pred_le) } } },
   { simp only [not_le] at h,
-    have w₁ : n - (ν - 1) = 0, { omega, },
-    have w₂ : ν ≠ 0, { omega, },
-    rw [w₁, eq_zero_of_lt R h],
-    simp [w₂], }
+    rw [nat.sub_eq_zero_of_le (nat.le_pred_of_lt h), eq_zero_of_lt R h],
+    simp [pos_iff_ne_zero.mp (pos_of_gt h)] },
 end
 
 lemma iterate_derivative_at_0_ne_zero [char_zero R] (n ν : ℕ) (h : ν ≤ n) :
@@ -209,10 +203,10 @@ begin
   simp only [←pochhammer_eval_cast],
   norm_cast,
   apply ne_of_gt,
-  by_cases h : ν = 0,
-  { subst h, simp, },
-  { apply pochhammer_pos,
-    omega, },
+  obtain rfl|h' := nat.eq_zero_or_pos ν,
+  { simp, },
+  { rw ← nat.succ_pred_eq_of_pos h' at h,
+    exact pochhammer_pos _ _ (nat.sub_pos_of_lt (nat.lt_of_succ_le h)) }
 end
 
 /-!
@@ -223,7 +217,7 @@ lemma iterate_derivative_at_1_eq_zero_of_lt (n : ℕ) {ν k : ℕ} :
   k < n - ν → (polynomial.derivative^[k] (bernstein_polynomial R n ν)).eval 1 = 0 :=
 begin
   intro w,
-  rw flip' _ _ _ (show ν ≤ n, by omega),
+  rw flip' _ _ _ (nat.lt_of_sub_pos (pos_of_gt w)).le,
   simp [polynomial.eval_comp, iterate_derivative_at_0_eq_zero_of_lt R n w],
 end
 
@@ -234,26 +228,19 @@ lemma iterate_derivative_at_1 (n ν : ℕ) (h : ν ≤ n) :
 begin
   rw flip' _ _ _ h,
   simp [polynomial.eval_comp, h],
-  by_cases h' : n = ν,
-  { subst h', simp, },
-  { replace h : ν < n, { omega, },
-    congr,
+  obtain rfl | h' := h.eq_or_lt,
+  { simp, },
+  { congr,
     norm_cast,
-    congr,
-    omega, },
+    rw [nat.sub_sub, nat.sub_sub_self (nat.succ_le_iff.mpr h')] },
 end
 
 lemma iterate_derivative_at_1_ne_zero [char_zero R] (n ν : ℕ) (h : ν ≤ n) :
   (polynomial.derivative^[n-ν] (bernstein_polynomial R n ν)).eval 1 ≠ 0 :=
 begin
-  simp only [bernstein_polynomial.iterate_derivative_at_1 _ _ _ h, ne.def,
-    int.coe_nat_eq_zero, neg_one_pow_mul_eq_zero_iff, nat.cast_eq_zero],
-    rw ←nat.cast_succ,
-  simp only [←pochhammer_eval_cast],
-  norm_cast,
-  apply ne_of_gt,
-  apply pochhammer_pos,
-  exact nat.succ_pos ν,
+  rw [bernstein_polynomial.iterate_derivative_at_1 _ _ _ h, ne.def, neg_one_pow_mul_eq_zero_iff,
+    ←nat.cast_succ, ←pochhammer_eval_cast, ←nat.cast_zero, nat.cast_inj],
+  exact (pochhammer_pos _ _ (nat.succ_pos ν)).ne',
 end
 
 open submodule
@@ -287,7 +274,7 @@ begin
       apply span_induction m,
       { simp,
         rintro ⟨a, w⟩, simp only [fin.coe_mk],
-        rw [iterate_derivative_at_1_eq_zero_of_lt ℚ _ (show n - k < n - a, by omega)], },
+        rw [iterate_derivative_at_1_eq_zero_of_lt ℚ n ((nat.sub_lt_sub_left_iff h).mpr w)] },
       { simp, },
       { intros x y hx hy, simp [hx, hy], },
       { intros a x h, simp [h], }, }, },

src/ring_theory/witt_vector/frobenius.lean

@@ -134,7 +134,9 @@ lemma map_frobenius_poly.key₂ {n i j : ℕ} (hi : i < n) (hj : j < p ^ (n - i)
 begin
   generalize h : (v p ⟨j + 1, j.succ_pos⟩) = m,
   suffices : m ≤ n - i ∧ m ≤ j,
-  { cases this, unfreezingI { clear_dependent p }, omega },
+  { rw [←nat.sub_add_comm this.2, add_comm i j, nat.add_sub_assoc (this.1.trans (nat.sub_le n i)),
+      add_assoc, nat.sub.right_comm, add_comm i, nat.sub_add_cancel (nat.le_sub_right_of_add_le
+      ((nat.le_sub_left_iff_add_le hi.le).mp this.1))] },
   split,
   { rw [← h, ← enat.coe_le_coe, pnat_multiplicity, enat.coe_get,
         ← hp.1.multiplicity_choose_prime_pow hj j.succ_pos],

src/ring_theory/witt_vector/structure_polynomial.lean

@@ -242,15 +242,15 @@ begin
   rw key, clear key IH,
   rw [bind₁, aeval_witt_polynomial, ring_hom.map_sum, ring_hom.map_sum, finset.sum_congr rfl],
   intros k hk,
-  rw finset.mem_range at hk,
+  rw [finset.mem_range, nat.lt_succ_iff] at hk,
   simp only [← sub_eq_zero, ← ring_hom.map_sub, ← C_dvd_iff_zmod, C_eq_coe_nat, ← mul_sub,
     ← int.nat_cast_eq_coe_nat, ← nat.cast_pow],
   rw show p ^ (n + 1) = p ^ k * p ^ (n - k + 1),
-  { rw ← pow_add, congr' 1, omega },
+  { rw [← pow_add, ←add_assoc], congr' 2, rw [add_comm, ←nat.sub_eq_iff_eq_add hk] },
   rw [nat.cast_mul, nat.cast_pow, nat.cast_pow],
   apply mul_dvd_mul_left,
   rw show p ^ (n + 1 - k) = p * p ^ (n - k),
-  { rw ← pow_succ, congr' 1, omega },
+  { rw [← pow_succ, nat.sub_add_comm hk] },
   rw [pow_mul],
   -- the machine!
   apply dvd_sub_pow_of_dvd_sub,