chore: golf using omega (#11318)

Backported from #11314.

Mathlib/Analysis/BoundedVariation.lean

@@ -350,18 +350,10 @@ theorem add_point (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ 
         · apply Finset.sum_congr rfl fun i hi => ?_
           rw [Finset.mem_Ico] at hi
           dsimp only [w]
-          have A : ¬1 + i + 1 < N := fun h => by
-            rw [add_assoc, add_comm] at h
-            exact hi.left.not_lt (i.lt_succ_self.trans (i.succ.lt_succ_self.trans h))
-          have B : ¬1 + i + 1 = N := fun h => by
-            rw [← h, add_assoc, add_comm] at hi
-            exact Nat.not_succ_le_self i (i.succ.le_succ.trans hi.left)
-          have C : ¬1 + i < N := fun h => by
-            rw [add_comm] at h
-            exact hi.left.not_lt (i.lt_succ_self.trans h)
-          have D : ¬1 + i = N := fun h => by
-            rw [← h, add_comm, Nat.succ_le_iff] at hi
-            exact hi.left.ne rfl
+          have A : ¬1 + i + 1 < N := by omega
+          have B : ¬1 + i + 1 = N := by omega
+          have C : ¬1 + i < N := by omega
+          have D : ¬1 + i = N := by omega
           rw [if_neg A, if_neg B, if_neg C, if_neg D]
           congr 3 <;> · rw [add_comm, Nat.sub_one]; apply Nat.pred_succ
       _ = (∑ i in Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) +
@@ -532,10 +524,11 @@ theorem comp_le_of_antitoneOn (f : α → E) {s : Set α} {t : Set β} (φ : β
     ⟨n, fun i => φ (u <| n - i), fun x y xy => hφ (ut _) (ut _) (hu <| Nat.sub_le_sub_left xy n),
       fun i => φst (ut _)⟩
     le_rfl
-  dsimp only [Subtype.coe_mk]
-  rw [edist_comm, Nat.sub_sub, add_comm, Nat.sub_succ, Nat.add_one, Nat.succ_pred_eq_of_pos]
-  simp only [Function.comp_apply]
-  simpa only [tsub_pos_iff_lt, Finset.mem_range] using hx
+  rw [edist_comm, Nat.sub_sub, add_comm, Nat.sub_succ, Nat.add_one, Nat.succ_eq_add_one]
+  simp only [Function.comp_apply, Nat.pred_eq_sub_one, Nat.sub_add_eq]
+  congr
+  simp only [Finset.mem_range] at hx
+  omega
 #align evariation_on.comp_le_of_antitone_on eVariationOn.comp_le_of_antitoneOn
 
 theorem comp_eq_of_monotoneOn (f : α → E) {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t) :

Mathlib/Data/Nat/Order/Basic.lean

@@ -171,16 +171,12 @@ theorem add_eq_one_iff : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 := by
 #align nat.add_eq_one_iff Nat.add_eq_one_iff
 
 theorem add_eq_two_iff : m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0 := by
-  cases n <;>
-  simp [(succ_ne_zero 1).symm, (show 2 = Nat.succ 1 from rfl),
-    succ_eq_add_one, ← add_assoc, succ_inj', add_eq_one_iff]
+  omega
 #align nat.add_eq_two_iff Nat.add_eq_two_iff
 
 theorem add_eq_three_iff :
     m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0 := by
-  cases n <;>
-  simp [(succ_ne_zero 1).symm, succ_eq_add_one, (show 3 = Nat.succ 2 from rfl),
-    ← add_assoc, succ_inj', add_eq_two_iff]
+  omega
 #align nat.add_eq_three_iff Nat.add_eq_three_iff
 
 theorem le_add_one_iff : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1 := by

Mathlib/Data/Polynomial/Derivative.lean

@@ -449,7 +449,7 @@ theorem iterate_derivative_mul {n} (p q : R[X]) :
     refine' sum_congr rfl fun k hk => _
     rw [mem_range] at hk
     congr
-    rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hk), Nat.succ_sub_succ]
+    omega
   · rw [Nat.choose_zero_right, tsub_zero]
 #align polynomial.iterate_derivative_mul Polynomial.iterate_derivative_mul
 

Mathlib/MeasureTheory/OuterMeasure/Basic.lean

@@ -200,7 +200,7 @@ theorem iUnion_nat_of_monotone_of_tsum_ne_top (m : OuterMeasure α) {s : ℕ →
   clear hx i
   rcases le_or_lt j n with hjn | hnj
   · exact Or.inl (h' hjn hj)
-  have : j - (n + 1) + n + 1 = j := by rw [add_assoc, tsub_add_cancel_of_le hnj.nat_succ_le]
+  have : j - (n + 1) + n + 1 = j := by omega
   refine' Or.inr (mem_iUnion.2 ⟨j - (n + 1), _, hlt _ _⟩)
   · rwa [this]
   · rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]

Mathlib/RingTheory/Polynomial/Bernstein.lean

@@ -227,9 +227,9 @@ theorem iterate_derivative_at_1 (n ν : ℕ) (h : ν ≤ n) :
   simp [Polynomial.eval_comp, h]
   obtain rfl | h' := h.eq_or_lt
   · simp
-  · congr
-    norm_cast
-    rw [← tsub_add_eq_tsub_tsub, tsub_tsub_cancel_of_le (Nat.succ_le_iff.mpr h')]
+  · norm_cast
+    congr
+    omega
 #align bernstein_polynomial.iterate_derivative_at_1 bernsteinPolynomial.iterate_derivative_at_1
 
 theorem iterate_derivative_at_1_ne_zero [CharZero R] (n ν : ℕ) (h : ν ≤ n) :