From bbf2206016a67e7d54812dcf76f830c704df378c Mon Sep 17 00:00:00 2001 From: grunweg Date: Tue, 12 Mar 2024 11:33:08 +0000 Subject: [PATCH] chore: golf using omega (#11318) Backported from #11314. --- Mathlib/Analysis/BoundedVariation.lean | 25 +++++++------------ Mathlib/Data/Nat/Order/Basic.lean | 8 ++---- Mathlib/Data/Polynomial/Derivative.lean | 2 +- Mathlib/MeasureTheory/OuterMeasure/Basic.lean | 2 +- Mathlib/RingTheory/Polynomial/Bernstein.lean | 6 ++--- 5 files changed, 16 insertions(+), 27 deletions(-) diff --git a/Mathlib/Analysis/BoundedVariation.lean b/Mathlib/Analysis/BoundedVariation.lean index 7c657ee5b1448..19605cc218253 100644 --- a/Mathlib/Analysis/BoundedVariation.lean +++ b/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) : diff --git a/Mathlib/Data/Nat/Order/Basic.lean b/Mathlib/Data/Nat/Order/Basic.lean index 181abb4713e6d..b5c0d20783bc4 100644 --- a/Mathlib/Data/Nat/Order/Basic.lean +++ b/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 diff --git a/Mathlib/Data/Polynomial/Derivative.lean b/Mathlib/Data/Polynomial/Derivative.lean index 28a5410ce8add..05a3b7bdb9fe8 100644 --- a/Mathlib/Data/Polynomial/Derivative.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/OuterMeasure/Basic.lean b/Mathlib/MeasureTheory/OuterMeasure/Basic.lean index 94c38401ac847..137dcb587aed0 100644 --- a/Mathlib/MeasureTheory/OuterMeasure/Basic.lean +++ b/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] diff --git a/Mathlib/RingTheory/Polynomial/Bernstein.lean b/Mathlib/RingTheory/Polynomial/Bernstein.lean index 64d8ef871dfad..6cf981c7b8a7c 100644 --- a/Mathlib/RingTheory/Polynomial/Bernstein.lean +++ b/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) :