chore: simplify some proofs with omega (#20919)

Those simplifications were found by [`tryAtEachStep`](https://github.com/dwrensha/tryAtEachStep).



Co-authored-by: Moritz Firsching <[email protected]>

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -187,11 +187,7 @@ theorem isRoot_of_isRoot_of_dvd_derivative_mul [CharZero R] {f g : R[X]} (hf0 :
   rw [rootMultiplicity_mul hdfg0, derivative_rootMultiplicity_of_root haf,
     rootMultiplicity_eq_zero hg, add_zero, rootMultiplicity_mul (hr ▸ hdfg0), add_comm,
     Nat.sub_eq_iff_eq_add (Nat.succ_le_iff.2 ((rootMultiplicity_pos hf0).2 haf))] at hr'
-  refine lt_irrefl (rootMultiplicity a f) ?_
-  refine lt_of_lt_of_le (Nat.lt_succ_self _)
-    (le_trans (le_add_of_nonneg_left (Nat.zero_le (rootMultiplicity a r))) ?_)
-  conv_rhs => rw [hr']
-  simp [add_assoc]
+  omega
 
 section NormalizationMonoid
 

Mathlib/Algebra/Ring/Int/Parity.lean

@@ -113,20 +113,7 @@ lemma four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : Odd a) (hb : Odd b) :
     4 ∣ a + b ∨ 4 ∣ a - b := by
   obtain ⟨m, rfl⟩ := ha
   obtain ⟨n, rfl⟩ := hb
-  obtain h | h := Int.even_or_odd (m + n)
-  · right
-    rw [Int.even_add, ← Int.even_sub] at h
-    obtain ⟨k, hk⟩ := h
-    convert dvd_mul_right 4 k using 1
-    rw [eq_add_of_sub_eq hk, mul_add, add_assoc, add_sub_cancel_right, ← two_mul, ← mul_assoc]
-    rfl
-  · left
-    obtain ⟨k, hk⟩ := h
-    convert dvd_mul_right 4 (k + 1) using 1
-    rw [eq_sub_of_add_eq hk, add_right_comm, ← add_sub, mul_add, mul_sub, add_assoc, add_assoc,
-      sub_add, add_assoc, ← sub_sub (2 * n), sub_self, zero_sub, sub_neg_eq_add, ← mul_assoc,
-      mul_add]
-    rfl
+  omega
 
 lemma two_mul_ediv_two_add_one_of_odd : Odd n → 2 * (n / 2) + 1 = n := by
   rintro ⟨c, rfl⟩

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -903,14 +903,7 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk
       rw [Fin.succAbove_of_le_castSucc i.succ _]
       simp only [Fin.lt_iff_val_lt_val, Fin.le_iff_val_le_val, Fin.val_succ, Fin.coe_castSucc,
         Nat.lt_succ_iff, Fin.ext_iff] at h' h'' ⊢
-      cases' Nat.le.dest h' with c hc
-      cases c
-      · exfalso
-        simp only [add_zero, len_mk, Fin.coe_pred] at hc
-        rw [hc] at h''
-        exact h'' rfl
-      · rw [← hc]
-        simp only [add_le_add_iff_left, Nat.succ_eq_add_one, le_add_iff_nonneg_left, zero_le]
+      omega
 
 theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : mk (n + 1) ⟶ Δ')
     (hθ : ¬Function.Injective θ.toOrderHom) :

Mathlib/Analysis/Complex/Polynomial/Basic.lean

@@ -159,15 +159,7 @@ theorem galActionHom_bijective_of_prime_degree' {p : ℚ[X]} (p_irr : Irreducibl
           MonoidHom.map_one, MonoidHom.map_one])
   have key := card_complex_roots_eq_card_real_add_card_not_gal_inv p
   simp_rw [Set.toFinset_card] at key
-  rw [key, add_le_add_iff_left] at p_roots1 p_roots2
-  rw [key, add_right_inj]
-  suffices ∀ m : ℕ, 2 ∣ m → 1 ≤ m → m ≤ 3 → m = 2 by exact this n hn p_roots1 p_roots2
-  rintro m ⟨k, rfl⟩ h2 h3
-  exact le_antisymm
-      (Nat.lt_succ_iff.mp
-        (lt_of_le_of_ne h3 (show 2 * k ≠ 2 * 1 + 1 from Nat.two_mul_ne_two_mul_add_one)))
-      (Nat.succ_le_iff.mpr
-        (lt_of_le_of_ne h2 (show 2 * 0 + 1 ≠ 2 * k from Nat.two_mul_ne_two_mul_add_one.symm)))
+  omega
 
 end Rationals
 

Mathlib/Combinatorics/Enumerative/Composition.lean

@@ -747,9 +747,7 @@ def compositionAsSetEquiv (n : ℕ) : CompositionAsSet n ≃ Finset (Fin (n - 1)
         exact Nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr i_ne_zero)
       refine ⟨⟨i - 1, ?_⟩, ?_, ?_⟩
       · have : (i : ℕ) < n + 1 := i.2
-        simp? [Nat.lt_succ_iff_lt_or_eq, i_ne_last] at this says
-          simp only [Nat.succ_eq_add_one, Nat.lt_succ_iff_lt_or_eq, i_ne_last, or_false] at this
-        exact Nat.pred_lt_pred i_ne_zero this
+        omega
       · convert i_mem
         simp only
         rwa [add_comm]

Mathlib/Computability/PartrecCode.lean

@@ -198,11 +198,7 @@ theorem encode_lt_prec (cf cg) :
 
 theorem encode_lt_rfind' (cf) : encode cf < encode (rfind' cf) := by
   simp only [encodeCode_eq, encodeCode]
-  have := Nat.mul_le_mul_right cf.encodeCode (by decide : 1 ≤ 2 * 2)
-  rw [one_mul, mul_assoc] at this
-  refine lt_of_le_of_lt (le_trans this ?_) (lt_add_of_pos_right _ (by decide : 0 < 4))
-  exact le_of_lt (Nat.lt_succ_of_le <| Nat.mul_le_mul_left _ <| le_of_lt <|
-    Nat.lt_succ_of_le <| Nat.mul_le_mul_left _ <| le_rfl)
+  omega
 
 end Nat.Partrec.Code
 

Mathlib/Data/Int/Defs.lean

@@ -228,8 +228,7 @@ where
   | 0 => Hp _ Int.le_rfl H0
   | n+1 => by
     refine cast (by rw [Int.add_sub_assoc]; rfl) (Hp _ (Int.le_of_lt ?_) (neg n))
-    conv => rhs; exact b.add_zero.symm
-    rw [Int.add_lt_add_iff_left]; apply negSucc_lt_zero
+    omega
 
 variable {z b H0 Hs Hp}
 

Mathlib/Data/List/Intervals.lean

@@ -56,12 +56,7 @@ theorem nodup (n m : ℕ) : Nodup (Ico n m) := by
 @[simp]
 theorem mem {n m l : ℕ} : l ∈ Ico n m ↔ n ≤ l ∧ l < m := by
   suffices n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m by simp [Ico, this]
-  rcases le_total n m with hnm | hmn
-  · rw [Nat.add_sub_cancel' hnm]
-  · rw [Nat.sub_eq_zero_iff_le.mpr hmn, Nat.add_zero]
-    exact
-      and_congr_right fun hnl =>
-        Iff.intro (fun hln => (not_le_of_gt hln hnl).elim) fun hlm => lt_of_lt_of_le hlm hmn
+  omega
 
 theorem eq_nil_of_le {n m : ℕ} (h : m ≤ n) : Ico n m = [] := by
   simp [Ico, Nat.sub_eq_zero_iff_le.mpr h]

Mathlib/Data/Nat/Choose/Sum.lean

@@ -104,11 +104,7 @@ theorem sum_range_choose_halfway (m : ℕ) : (∑ i ∈ range (m + 1), (2 * m +
             ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i := by
         rw [range_eq_Ico, sum_Ico_reflect _ _ (by omega)]
         congr
-        have A : m + 1 ≤ 2 * m + 1 := by omega
-        rw [add_comm, add_tsub_assoc_of_le A, ← add_comm]
-        congr
-        rw [tsub_eq_iff_eq_add_of_le A]
-        ring
+        omega
       _ = ∑ i ∈ range (2 * m + 2), (2 * m + 1).choose i := sum_range_add_sum_Ico _ (by omega)
       _ = 2 ^ (2 * m + 1) := sum_range_choose (2 * m + 1)
       _ = 2 * 4 ^ m := by rw [pow_succ, pow_mul, mul_comm]; rfl

Mathlib/Data/Nat/Defs.lean

@@ -493,16 +493,10 @@ lemma div_mul_div_le_div (a b c : ℕ) : a / c * b / a ≤ b / c := by
 lemma eq_zero_of_le_half (h : n ≤ n / 2) : n = 0 := eq_zero_of_le_div (Nat.le_refl _) h
 
 lemma le_half_of_half_lt_sub (h : a / 2 < a - b) : b ≤ a / 2 := by
-  rw [Nat.le_div_iff_mul_le Nat.two_pos]
-  rw [Nat.div_lt_iff_lt_mul Nat.two_pos, Nat.sub_mul, Nat.lt_sub_iff_add_lt,
-    Nat.mul_two a] at h
-  exact Nat.le_of_lt (Nat.lt_of_add_lt_add_left h)
+  omega
 
 lemma half_le_of_sub_le_half (h : a - b ≤ a / 2) : a / 2 ≤ b := by
-  rw [Nat.le_div_iff_mul_le Nat.two_pos, Nat.sub_mul, Nat.sub_le_iff_le_add,
-    Nat.mul_two, Nat.add_le_add_iff_left] at h
-  rw [← Nat.mul_div_left b Nat.two_pos]
-  exact Nat.div_le_div_right h
+  omega
 
 protected lemma div_le_of_le_mul' (h : m ≤ k * n) : m / k ≤ n := by
   obtain rfl | hk := k.eq_zero_or_pos

Mathlib/RingTheory/Ideal/Basic.lean

@@ -77,12 +77,7 @@ theorem add_pow_mem_of_pow_mem_of_le {m n k : ℕ}
   by_cases h : m ≤ c
   · exact I.mul_mem_right _ (I.pow_mem_of_pow_mem ha h)
   · refine I.mul_mem_left _ (I.pow_mem_of_pow_mem hb ?_)
-    simp only [not_le, Nat.lt_iff_add_one_le] at h
-    have hck : c ≤ k := by
-      rw [← add_le_add_iff_right 1]
-      exact le_trans h (le_trans (Nat.le_add_right _ _) hk)
-    rw [Nat.le_sub_iff_add_le hck, ← add_le_add_iff_right 1]
-    exact le_trans (by rwa [add_comm _ n, add_assoc, add_le_add_iff_left]) hk
+    omega
 
 theorem add_pow_add_pred_mem_of_pow_mem  {m n : ℕ}
     (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) :

Mathlib/RingTheory/Polynomial/Basic.lean

@@ -723,12 +723,7 @@ theorem isPrime_map_C_iff_isPrime (P : Ideal R) :
         rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
         simp only [Ne, Prod.mk.inj_iff, not_and_or] at hij
         obtain hi | hj : i < m ∨ j < n := by
-          rw [or_iff_not_imp_left, not_lt, le_iff_lt_or_eq]
-          rintro (hmi | rfl)
-          · rw [← not_le]
-            intro hnj
-            exact (add_lt_add_of_lt_of_le hmi hnj).ne hij.2.symm
-          · simp only [eq_self_iff_true, not_true, false_or, add_right_inj, not_and_self_iff] at hij
+          omega
         · rw [mul_comm]
           apply P.mul_mem_left
           exact Classical.not_not.1 (Nat.find_min hf hi)

Mathlib/RingTheory/RootsOfUnity/Complex.lean

@@ -130,17 +130,7 @@ theorem IsPrimitiveRoot.arg {n : ℕ} {ζ : ℂ} (h : IsPrimitiveRoot ζ n) (hn
     · exact hin
     · convert hin.add_mul_left_left (-1) using 1
       rw [mul_neg_one, sub_eq_add_neg]
-  on_goal 2 =>
-    split_ifs with h₂
-    · exact mod_cast h
-    suffices (i - n : ℤ).natAbs = n - i by
-      rw [this]
-      apply tsub_lt_self hn.bot_lt
-      contrapose! h₂
-      rw [Nat.eq_zero_of_le_zero h₂, zero_mul]
-      exact zero_le _
-    rw [← Int.natAbs_neg, neg_sub, Int.natAbs_eq_iff]
-    exact Or.inl (Int.ofNat_sub h.le).symm
+  on_goal 2 => omega
   split_ifs with h₂
   · convert Complex.arg_cos_add_sin_mul_I _
     · push_cast; rfl

Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

@@ -426,11 +426,7 @@ theorem HasProd.nat_mul_neg {f : ℤ → M} (hf : HasProd f m) :
       · intro x hx
         simp only [u1, u2, mem_inter, mem_image, exists_prop] at hx
         suffices x = 0 by simp only [this, eq_self_iff_true, if_true]
-        apply le_antisymm
-        · rcases hx.2 with ⟨a, _, rfl⟩
-          simp only [Right.neg_nonpos_iff, Nat.cast_nonneg]
-        · rcases hx.1 with ⟨a, _, rfl⟩
-          simp only [Nat.cast_nonneg]
+        omega
     _ = (∏ x ∈ u1, f x) * ∏ x ∈ u2, f x := prod_union_inter
     _ = (∏ b ∈ v', f b) * ∏ b ∈ v', f (-b) := by
       simp only [u1, u2, Nat.cast_inj, imp_self, implies_true, forall_const, prod_image, neg_inj]