diff --git a/archive/100-theorems-list/83_friendship_graphs.lean b/archive/100-theorems-list/83_friendship_graphs.lean index bf2f99f99942f..f6033c4a2cc7c 100644 --- a/archive/100-theorems-list/83_friendship_graphs.lean +++ b/archive/100-theorems-list/83_friendship_graphs.lean @@ -274,7 +274,7 @@ begin { cases fintype.card V with n, { exact zero_le _, }, { have : n = 0, - { rw [nat.succ_sub_succ_eq_sub, nat.sub_zero] at h, + { rw [nat.succ_sub_succ_eq_sub, tsub_zero] at h, linarith }, subst n, } }, use classical.arbitrary V, diff --git a/archive/imo/imo1977_q6.lean b/archive/imo/imo1977_q6.lean index b8361db94a990..1c65f6af0c855 100644 --- a/archive/imo/imo1977_q6.lean +++ b/archive/imo/imo1977_q6.lean @@ -25,7 +25,7 @@ begin { intros n hk, apply nat.succ_le_of_lt, calc k ≤ f (f (n - 1)) : h_ind _ (h_ind (n - 1) (le_tsub_of_add_le_right hk)) - ... < f n : nat.sub_add_cancel + ... < f n : tsub_add_cancel_of_le (le_trans (nat.succ_le_succ (nat.zero_le _)) hk) ▸ h _ } }, have hf : ∀ n, n ≤ f n := λ n, h' n n rfl.le, have hf_mono : strict_mono f := strict_mono_nat_of_lt_succ (λ _, lt_of_le_of_lt (hf _) (h _)), diff --git a/archive/imo/imo1981_q3.lean b/archive/imo/imo1981_q3.lean index 2e6a97b1f7064..1560499391ba1 100644 --- a/archive/imo/imo1981_q3.lean +++ b/archive/imo/imo1981_q3.lean @@ -130,7 +130,7 @@ begin { have h7 : nat_predicate N (n - m) m, from h2.reduction h4, obtain ⟨k : ℕ, hnm : n - m = fib k, rfl : m = fib (k+1)⟩ := h1 m h6 (n - m) h7, use [k + 1, rfl], - rw [fib_succ_succ, ← hnm, nat.sub_add_cancel h3] } } + rw [fib_succ_succ, ← hnm, tsub_add_cancel_of_le h3] } } end end nat_predicate diff --git a/archive/miu_language/decision_suf.lean b/archive/miu_language/decision_suf.lean index 797067d871fa5..6ead3de8bc3ff 100644 --- a/archive/miu_language/decision_suf.lean +++ b/archive/miu_language/decision_suf.lean @@ -181,7 +181,7 @@ end arithmetic lemma repeat_pow_minus_append {m : ℕ} : M :: repeat I (2^m - 1) ++ [I] = M::(repeat I (2^m)) := begin change [I] with repeat I 1, - rw [cons_append, ←repeat_add, nat.sub_add_cancel (one_le_pow' m 1)], + rw [cons_append, ←repeat_add, tsub_add_cancel_of_le (one_le_pow' m 1)], end /-- @@ -204,7 +204,7 @@ begin { apply der_cons_repeat_I_repeat_U_append_of_der_cons_repeat_I_append c ((2^m-c)/3) h, convert hw₂, -- now we must show `c + 3 * ((2 ^ m - c) / 3) = 2 ^ m` rw nat.mul_div_cancel', - { exact nat.add_sub_of_le hm.1 }, + { exact add_tsub_cancel_of_le hm.1 }, { exact (modeq_iff_dvd' hm.1).mp hm.2.symm } }, rw [append_assoc, ←repeat_add _ _] at hw₃, cases add_mod2 ((2^m-c)/3) with t ht, @@ -228,7 +228,7 @@ begin { apply der_cons_repeat_I_repeat_U_append_of_der_cons_repeat_I_append c ((2^m-c)/3) h, convert hw₂, -- now we must show `c + 3 * ((2 ^ m - c) / 3) = 2 ^ m` rw nat.mul_div_cancel', - { exact nat.add_sub_of_le hm.1 }, + { exact add_tsub_cancel_of_le hm.1 }, { exact (modeq_iff_dvd' hm.1).mp hm.2.symm } }, rw [append_assoc, ←repeat_add _ _] at hw₃, cases add_mod2 ((2^m-c)/3) with t ht, diff --git a/archive/oxford_invariants/2021summer/week3_p1.lean b/archive/oxford_invariants/2021summer/week3_p1.lean index d89951b691bb4..e6c9599da8f9d 100644 --- a/archive/oxford_invariants/2021summer/week3_p1.lean +++ b/archive/oxford_invariants/2021summer/week3_p1.lean @@ -97,7 +97,7 @@ begin { rw [nat.cast_one, finset.sum_range_one, div_self], exact (mul_pos (a_pos 0 (nat.zero_le _)) (a_pos 1 (nat.zero_lt_succ _))).ne' }, -- Check the divisibility condition - { rw [mul_one, nat.sub_self], + { rw [mul_one, tsub_self], exact dvd_zero _ } }, /- Induction step `b` is the value of the previous sum as a natural, `hb` is the proof that it is indeed the value, @@ -133,7 +133,7 @@ begin (a_pos _ $ nat.le_succ _).ne', mul_comm], end }, -- Check the divisibility condition - { rw [nat.mul_sub_left_distrib, ← mul_assoc, nat.mul_div_cancel' ha, add_mul, - nat.mul_div_cancel' han, add_tsub_tsub_cancel ha₀, nat.add_sub_cancel], + { rw [mul_tsub, ← mul_assoc, nat.mul_div_cancel' ha, add_mul, + nat.mul_div_cancel' han, add_tsub_tsub_cancel ha₀, add_tsub_cancel_right], exact dvd_mul_right _ _ } end diff --git a/counterexamples/canonically_ordered_comm_semiring_two_mul.lean b/counterexamples/canonically_ordered_comm_semiring_two_mul.lean index 21de9c7a63458..3b9ad504389da 100644 --- a/counterexamples/canonically_ordered_comm_semiring_two_mul.lean +++ b/counterexamples/canonically_ordered_comm_semiring_two_mul.lean @@ -231,7 +231,7 @@ begin { exact ⟨(0 : L), (add_zero _).symm⟩ }, { refine ⟨⟨⟨bn - an, b2 + a2⟩, _⟩, _⟩, { rw [ne.def, prod.mk.inj_iff, not_and_distrib], - exact or.inl (ne_of_gt (nat.sub_pos_of_lt h)) }, + exact or.inl (ne_of_gt (tsub_pos_of_lt h)) }, { congr, { exact (add_tsub_cancel_of_le h.le).symm }, { change b2 = a2 + (b2 + a2), diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean index 25341b15e9a64..782e32bd0bc44 100644 --- a/src/algebra/big_operators/basic.lean +++ b/src/algebra/big_operators/basic.lean @@ -928,10 +928,10 @@ when the function we are summing is monotone. lemma sum_range_sub_of_monotone {f : ℕ → ℕ} (h : monotone f) (n : ℕ) : ∑ i in range n, (f (i+1) - f i) = f n - f 0 := begin - refine sum_range_induction _ _ (nat.sub_self _) (λ n, _) _, + refine sum_range_induction _ _ (tsub_self _) (λ n, _) _, have h₁ : f n ≤ f (n+1) := h (nat.le_succ _), have h₂ : f 0 ≤ f n := h (nat.zero_le _), - rw [←nat.sub_add_comm h₂, add_tsub_cancel_of_le h₁], + rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁], end @[simp] lemma prod_const (b : β) : (∏ x in s, b) = b ^ s.card := diff --git a/src/algebra/big_operators/intervals.lean b/src/algebra/big_operators/intervals.lean index 336b2fb82b230..8c184540716ef 100644 --- a/src/algebra/big_operators/intervals.lean +++ b/src/algebra/big_operators/intervals.lean @@ -90,9 +90,9 @@ lemma prod_Ico_eq_prod_range (f : ℕ → β) (m n : ℕ) : (∏ k in Ico m n, f k) = (∏ k in range (n - m), f (m + k)) := begin by_cases h : m ≤ n, - { rw [←nat.Ico_zero_eq_range, prod_Ico_add, zero_add, nat.sub_add_cancel h] }, + { rw [←nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h] }, { replace h : n ≤ m := le_of_not_ge h, - rw [Ico_eq_empty_of_le h, nat.sub_eq_zero_of_le h, range_zero, prod_empty, prod_empty] } + rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty] } end lemma prod_Ico_reflect (f : ℕ → β) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1) : @@ -106,8 +106,8 @@ begin refine (prod_image _).symm, simp only [mem_Ico], rintros i ⟨ki, im⟩ j ⟨kj, jm⟩ Hij, - rw [← nat.sub_sub_self (this _ im), Hij, nat.sub_sub_self (this _ jm)] }, - { simp [Ico_eq_empty_of_le, nat.sub_le_sub_left, hkm] } + rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)] }, + { simp [Ico_eq_empty_of_le, tsub_le_tsub_left, hkm] } end lemma sum_Ico_reflect {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) (k : ℕ) {m n : ℕ} @@ -120,7 +120,7 @@ lemma prod_range_reflect (f : ℕ → β) (n : ℕ) : begin cases n, { simp }, - { simp only [←nat.Ico_zero_eq_range, nat.succ_sub_succ_eq_sub, nat.sub_zero], + { simp only [←nat.Ico_zero_eq_range, nat.succ_sub_succ_eq_sub, tsub_zero], rw prod_Ico_reflect _ _ le_rfl, simp } end diff --git a/src/algebra/char_p/basic.lean b/src/algebra/char_p/basic.lean index a66b93baf0c67..628f83aed6678 100644 --- a/src/algebra/char_p/basic.lean +++ b/src/algebra/char_p/basic.lean @@ -117,10 +117,10 @@ theorem add_pow_char_of_commute [semiring R] {p : ℕ} [fact p.prime] [char_p R p] (x y : R) (h : commute x y) : (x + y)^p = x^p + y^p := begin - rw [commute.add_pow h, finset.sum_range_succ_comm, nat.sub_self, pow_zero, nat.choose_self], + rw [commute.add_pow h, finset.sum_range_succ_comm, tsub_self, pow_zero, nat.choose_self], rw [nat.cast_one, mul_one, mul_one], congr' 1, convert finset.sum_eq_single 0 _ _, - { simp only [mul_one, one_mul, nat.choose_zero_right, nat.sub_zero, nat.cast_one, pow_zero] }, + { simp only [mul_one, one_mul, nat.choose_zero_right, tsub_zero, nat.cast_one, pow_zero] }, { intros b h1 h2, suffices : (p.choose b : R) = 0, { rw this, simp }, rw char_p.cast_eq_zero_iff R p, diff --git a/src/algebra/continued_fractions/terminated_stable.lean b/src/algebra/continued_fractions/terminated_stable.lean index 7fa841e7cfcbc..2e593c632282f 100644 --- a/src/algebra/continued_fractions/terminated_stable.lean +++ b/src/algebra/continued_fractions/terminated_stable.lean @@ -40,8 +40,8 @@ begin have stable_step : g.continuants_aux (m - 1 + 2) = g.continuants_aux (m - 1 + 1), from continuants_aux_stable_step_of_terminated this, have one_le_m : 1 ≤ m, from nat.one_le_of_lt succ_n_le_m, - have : m - 1 + 2 = m + 2 - 1, from (nat.sub_add_comm one_le_m).symm, - have : m - 1 + 1 = m + 1 - 1, from (nat.sub_add_comm one_le_m).symm, + have : m - 1 + 2 = m + 2 - 1, from tsub_add_eq_add_tsub one_le_m, + have : m - 1 + 1 = m + 1 - 1, from tsub_add_eq_add_tsub one_le_m, simpa [*] using stable_step }, exact (eq.trans this IH) } end diff --git a/src/algebra/geom_sum.lean b/src/algebra/geom_sum.lean index 7e5d01cdf737f..33d41c87e49dd 100644 --- a/src/algebra/geom_sum.lean +++ b/src/algebra/geom_sum.lean @@ -82,7 +82,7 @@ begin refine sum_congr rfl (λ j j_in, _), rw [mem_range, nat.lt_iff_add_one_le] at j_in, congr, - apply nat.sub_sub_self, + apply tsub_tsub_cancel_of_le, exact le_tsub_of_add_le_right j_in end @@ -100,7 +100,7 @@ begin { rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero] }, { have f_last : f (n + 1) n = (x + y) ^ n := by { dsimp [f], - rw [nat.sub_sub, nat.add_comm, nat.sub_self, pow_zero, mul_one] }, + rw [← tsub_add_eq_tsub_tsub, nat.add_comm, tsub_self, pow_zero, mul_one] }, have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := λ i hi, by { dsimp [f], @@ -108,11 +108,11 @@ begin (h.symm.add_right (commute.refl y)).pow_right i, rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ y (n - 1 - i)], congr' 2, - rw [nat.add_sub_cancel, nat.sub_sub, add_comm 1 i], - have : i + 1 + (n - (i + 1)) = n := nat.add_sub_of_le (mem_range.mp hi), + rw [add_tsub_cancel_right, ← tsub_add_eq_tsub_tsub, add_comm 1 i], + have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi), rw [add_comm (i + 1)] at this, - rw [← this, nat.add_sub_cancel, add_comm i 1, ← add_assoc, - nat.add_sub_cancel] }, + rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, + add_tsub_cancel_right] }, rw [pow_succ (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc], rw (((commute.refl x).add_right h).pow_right n).eq, congr' 1, @@ -221,12 +221,12 @@ begin congr, rw [mem_range, nat.lt_iff_add_one_le, add_comm] at j_in, have h' : n - m + (m - (1 + j)) = n - (1 + j) := tsub_add_tsub_cancel hmn j_in, - rw [nat.sub_sub m, h', nat.sub_sub] }, + rw [← tsub_add_eq_tsub_tsub m, h', ← tsub_add_eq_tsub_tsub] }, rw this, simp_rw pow_mul_comm y (n-m) _, simp_rw ← mul_assoc, rw [← sum_mul, ← geom_sum₂_def, mul_sub, h.mul_geom_sum₂, ← mul_assoc, - h.mul_geom_sum₂, sub_mul, ← pow_add, nat.add_sub_of_le hmn, + h.mul_geom_sum₂, sub_mul, ← pow_add, add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ n)], end @@ -234,14 +234,14 @@ protected theorem commute.geom_sum₂_succ_eq {α : Type u} [ring α] {x y : α} (h : commute x y) {n : ℕ} : geom_sum₂ x y (n + 1) = x ^ n + y * (geom_sum₂ x y n) := begin - simp_rw [geom_sum₂, mul_sum, sum_range_succ_comm, nat.add_succ_sub_one, add_zero, nat.sub_self, + simp_rw [geom_sum₂, mul_sum, sum_range_succ_comm, nat.add_succ_sub_one, add_zero, tsub_self, pow_zero, mul_one, add_right_inj, ←mul_assoc, (h.symm.pow_right _).eq, mul_assoc, ←pow_succ], refine sum_congr rfl (λ i hi, _), suffices : n - 1 - i + 1 = n - i, { rw this }, cases n, { exact absurd (list.mem_range.mp hi) i.not_lt_zero }, { rw [tsub_add_eq_add_tsub (nat.le_pred_of_lt (list.mem_range.mp hi)), - nat.sub_add_cancel (nat.succ_le_iff.mpr n.succ_pos)] }, + tsub_add_cancel_of_le (nat.succ_le_iff.mpr n.succ_pos)] }, end theorem geom_sum₂_succ_eq {α : Type u} [comm_ring α] (x y : α) {n : ℕ} : @@ -329,20 +329,20 @@ calc (b - 1) * (∑ i in range n.succ, a/b^i) = ∑ i in range n, a/b^(i + 1) * b + a * b - (∑ i in range n, a/b^i + a/b^n) - : by rw [nat.mul_sub_right_distrib, mul_comm, sum_mul, one_mul, sum_range_succ', + : by rw [tsub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero, nat.div_one] ... ≤ ∑ i in range n, a/b^i + a * b - (∑ i in range n, a/b^i + a/b^n) : begin - refine nat.sub_le_sub_right (add_le_add_right (sum_le_sum $ λ i _, _) _) _, + refine tsub_le_tsub_right (add_le_add_right (sum_le_sum $ λ i _, _) _) _, rw [pow_succ', ←nat.div_div_eq_div_mul], exact nat.div_mul_le_self _ _, end - ... = a * b - a/b^n : nat.add_sub_add_left _ _ _ + ... = a * b - a/b^n : add_tsub_add_eq_tsub_left _ _ _ lemma nat.geom_sum_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) : ∑ i in range n, a/b^i ≤ a * b/(b - 1) := begin - refine (nat.le_div_iff_mul_le _ _ $ nat.sub_pos_of_lt hb).2 _, + refine (nat.le_div_iff_mul_le _ _ $ tsub_pos_of_lt hb).2 _, cases n, { rw [sum_range_zero, zero_mul], exact nat.zero_le _ }, @@ -368,5 +368,5 @@ begin ... = (a * 1 + a * (b - 1))/(b - 1) : by rw [←mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)] ... = a + a/(b - 1) - : by rw [mul_one, nat.add_mul_div_right _ _ (nat.sub_pos_of_lt hb), add_comm] + : by rw [mul_one, nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm] end diff --git a/src/algebra/group_power/basic.lean b/src/algebra/group_power/basic.lean index c082d5b0b56ca..0a03c45def955 100644 --- a/src/algebra/group_power/basic.lean +++ b/src/algebra/group_power/basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Robert Y. Lewis -/ -import algebra.order.ring +import data.nat.basic import tactic.monotonicity.basic import group_theory.group_action.defs @@ -172,11 +172,11 @@ by rw [nat.mul_comm, pow_mul] @[to_additive nsmul_add_sub_nsmul] theorem pow_mul_pow_sub (a : M) {m n : ℕ} (h : m ≤ n) : a ^ m * a ^ (n - m) = a ^ n := -by rw [←pow_add, nat.add_comm, nat.sub_add_cancel h] +by rw [←pow_add, nat.add_comm, tsub_add_cancel_of_le h] @[to_additive sub_nsmul_nsmul_add] theorem pow_sub_mul_pow (a : M) {m n : ℕ} (h : m ≤ n) : a ^ (n - m) * a ^ m = a ^ n := -by rw [←pow_add, nat.sub_add_cancel h] +by rw [←pow_add, tsub_add_cancel_of_le h] @[to_additive bit0_nsmul] theorem pow_bit0 (a : M) (n : ℕ) : a ^ bit0 n = a^n * a^n := pow_add _ _ _ @@ -303,7 +303,7 @@ end @[to_additive nsmul_sub] -- rename to sub_nsmul? theorem pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ := -have h1 : m - n + n = m, from nat.sub_add_cancel h, +have h1 : m - n + n = m, from tsub_add_cancel_of_le h, have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1], eq_mul_inv_of_mul_eq h2 @@ -376,7 +376,7 @@ end lemma pow_eq_zero_of_le [monoid_with_zero M] {x : M} {n m : ℕ} (hn : n ≤ m) (hx : x^n = 0) : x^m = 0 := -by rw [← nat.sub_add_cancel hn, pow_add, hx, mul_zero] +by rw [← tsub_add_cancel_of_le hn, pow_add, hx, mul_zero] namespace ring_hom @@ -408,7 +408,7 @@ lemma mul_neg_one_pow_eq_zero_iff [ring R] {n : ℕ} {r : R} : r * (-1)^n = 0 by rcases neg_one_pow_eq_or R n; simp [h] lemma pow_dvd_pow [monoid R] (a : R) {m n : ℕ} (h : m ≤ n) : - a ^ m ∣ a ^ n := ⟨a ^ (n - m), by rw [← pow_add, nat.add_comm, nat.sub_add_cancel h]⟩ + a ^ m ∣ a ^ n := ⟨a ^ (n - m), by rw [← pow_add, nat.add_comm, tsub_add_cancel_of_le h]⟩ theorem pow_dvd_pow_of_dvd [comm_monoid R] {a b : R} (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n | 0 := by rw [pow_zero, pow_zero] diff --git a/src/algebra/group_power/lemmas.lean b/src/algebra/group_power/lemmas.lean index ff1c7d04530a5..3d179cab974d0 100644 --- a/src/algebra/group_power/lemmas.lean +++ b/src/algebra/group_power/lemmas.lean @@ -73,7 +73,7 @@ def invertible_of_pow_eq_one (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : 0 < n) : begin apply invertible_of_pow_succ_eq_one x (n - 1), convert hx, - exact nat.sub_add_cancel (nat.succ_le_of_lt hn), + exact tsub_add_cancel_of_le (nat.succ_le_of_lt hn), end lemma is_unit_of_pow_eq_one (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : 0 < n) : diff --git a/src/algebra/group_power/order.lean b/src/algebra/group_power/order.lean index 84922ed7d5424..c2fe4946e3e03 100644 --- a/src/algebra/group_power/order.lean +++ b/src/algebra/group_power/order.lean @@ -156,7 +156,7 @@ theorem pow_lt_pow_of_lt_left {x y : R} {n : ℕ} (Hxy : x < y) (Hxpos : 0 ≤ x x ^ n < y ^ n := begin cases lt_or_eq_of_le Hxpos, - { rw ←nat.sub_add_cancel Hnpos, + { rw ← tsub_add_cancel_of_le (nat.succ_le_of_lt Hnpos), induction (n - 1), { simpa only [pow_one] }, rw [pow_add, pow_add, nat.succ_eq_add_one, pow_one, pow_one], apply mul_lt_mul ih (le_of_lt Hxy) h (le_of_lt (pow_pos (lt_trans h Hxy) _)) }, diff --git a/src/algebra/group_with_zero/power.lean b/src/algebra/group_with_zero/power.lean index a2d9c2570006d..e6d46601c63a3 100644 --- a/src/algebra/group_with_zero/power.lean +++ b/src/algebra/group_with_zero/power.lean @@ -44,7 +44,7 @@ begin end theorem pow_sub₀ (a : G₀) {m n : ℕ} (ha : a ≠ 0) (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ := -have h1 : m - n + n = m, from nat.sub_add_cancel h, +have h1 : m - n + n = m, from tsub_add_cancel_of_le h, have h2 : a ^ (m - n) * a ^ n = a ^ m, by rw [←pow_add, h1], by simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2 diff --git a/src/algebra/linear_recurrence.lean b/src/algebra/linear_recurrence.lean index 92bc6b48ae49e..929df10a66830 100644 --- a/src/algebra/linear_recurrence.lean +++ b/src/algebra/linear_recurrence.lean @@ -65,7 +65,7 @@ def mk_sol (init : fin E.order → α) : ℕ → α ∑ k : fin E.order, have n - E.order + k < n := begin - rw [add_comm, ← nat.add_sub_assoc (not_lt.mp h), tsub_lt_iff_left], + rw [add_comm, ← add_tsub_assoc_of_le (not_lt.mp h), tsub_lt_iff_left], { exact add_lt_add_right k.is_lt n }, { convert add_le_add (zero_le (k : ℕ)) (not_lt.mp h), simp only [zero_add] } @@ -88,12 +88,12 @@ lemma eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : fin E.order → α} | n := if h' : n < E.order then by rw mk_sol; simp only [h', dif_pos]; exact_mod_cast heq ⟨n, h'⟩ else begin - rw [mk_sol, ← nat.sub_add_cancel (le_of_not_lt h'), h (n-E.order)], + rw [mk_sol, ← tsub_add_cancel_of_le (le_of_not_lt h'), h (n-E.order)], simp [h'], congr' with k, exact have wf : n - E.order + k < n := begin - rw [add_comm, ← nat.add_sub_assoc (not_lt.mp h'), tsub_lt_iff_left], + rw [add_comm, ← add_tsub_assoc_of_le (not_lt.mp h'), tsub_lt_iff_left], { exact add_lt_add_right k.is_lt n }, { convert add_le_add (zero_le (k : ℕ)) (not_lt.mp h'), simp only [zero_add] } diff --git a/src/algebra/order/ring.lean b/src/algebra/order/ring.lean index a9a293049dbd2..f06a123e755bb 100644 --- a/src/algebra/order/ring.lean +++ b/src/algebra/order/ring.lean @@ -1412,7 +1412,7 @@ variables [has_sub α] [has_ordered_sub α] variables [is_total α (≤)] namespace add_le_cancellable -protected lemma mul_sub (h : add_le_cancellable (a * c)) : +protected lemma mul_tsub (h : add_le_cancellable (a * c)) : a * (b - c) = a * b - a * c := begin cases total_of (≤) b c with hbc hcb, @@ -1420,18 +1420,18 @@ begin { apply h.eq_tsub_of_add_eq, rw [← mul_add, tsub_add_cancel_of_le hcb] } end -protected lemma sub_mul (h : add_le_cancellable (b * c)) : (a - b) * c = a * c - b * c := -by { simp only [mul_comm _ c] at *, exact h.mul_sub } +protected lemma tsub_mul (h : add_le_cancellable (b * c)) : (a - b) * c = a * c - b * c := +by { simp only [mul_comm _ c] at *, exact h.mul_tsub } end add_le_cancellable variables [contravariant_class α α (+) (≤)] -lemma mul_sub' (a b c : α) : a * (b - c) = a * b - a * c := -contravariant.add_le_cancellable.mul_sub +lemma mul_tsub (a b c : α) : a * (b - c) = a * b - a * c := +contravariant.add_le_cancellable.mul_tsub -lemma sub_mul' (a b c : α) : (a - b) * c = a * c - b * c := -contravariant.add_le_cancellable.sub_mul +lemma tsub_mul (a b c : α) : (a - b) * c = a * c - b * c := +contravariant.add_le_cancellable.tsub_mul end sub diff --git a/src/algebra/order/sub.lean b/src/algebra/order/sub.lean index f8cf147fdaad4..b5e5a9aecdb5f 100644 --- a/src/algebra/order/sub.lean +++ b/src/algebra/order/sub.lean @@ -33,6 +33,8 @@ second version we replace this type-class assumption by explicit `add_le_cancell TODO: maybe we should make a multiplicative version of this, so that we can replace some identical lemmas about subtraction/division in `ordered_[add_]comm_group` with these. +TODO: generalize `nat.le_of_le_of_sub_le_sub_right`, `nat.sub_le_sub_right_iff`, + `nat.mul_self_sub_mul_self_eq` -/ variables {α β : Type*} @@ -141,7 +143,7 @@ tsub_le_iff_left.mpr $ le_add_tsub.trans $ add_le_add_right h _ lemma tsub_le_tsub (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c := (tsub_le_tsub_right hab _).trans $ tsub_le_tsub_left hcd _ -lemma tsub_add_eq_tsub_tsub : a - (b + c) = a - b - c := +lemma tsub_add_eq_tsub_tsub (a b c : α) : a - (b + c) = a - b - c := begin refine le_antisymm (tsub_le_iff_left.mpr _) (tsub_le_iff_left.mpr $ tsub_le_iff_left.mpr _), @@ -149,8 +151,8 @@ begin { rw [← add_assoc], apply le_add_tsub } end -lemma tsub_add_eq_tsub_tsub_swap : a - (b + c) = a - c - b := -by { rw [add_comm], exact tsub_add_eq_tsub_tsub } +lemma tsub_add_eq_tsub_tsub_swap (a b c : α) : a - (b + c) = a - c - b := +by { rw [add_comm], apply tsub_add_eq_tsub_tsub } lemma add_le_add_add_tsub : a + b ≤ (a + c) + (b - c) := by { rw [add_assoc], exact add_le_add_left le_add_tsub a } @@ -275,7 +277,7 @@ end contra section both variables [covariant_class α α (+) (≤)] [contravariant_class α α (+) (≤)] -lemma add_tsub_add_right_eq_tsub (a c b : α) : (a + c) - (b + c) = a - b := +lemma add_tsub_add_eq_tsub_right (a c b : α) : (a + c) - (b + c) = a - b := begin apply le_antisymm, { rw [tsub_le_iff_left, add_right_comm], exact add_le_add_right le_add_tsub c }, @@ -286,7 +288,7 @@ begin end lemma add_tsub_add_eq_tsub_left (a b c : α) : (a + b) - (a + c) = b - c := -by rw [add_comm a b, add_comm a c, add_tsub_add_right_eq_tsub] +by rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right] end both @@ -311,6 +313,8 @@ lt_iff_lt_of_le_iff_le tsub_le_iff_left lemma lt_tsub_comm : a < b - c ↔ c < b - a := lt_tsub_iff_left.trans lt_tsub_iff_right.symm + + section cov variable [covariant_class α α (+) (≤)] diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean index 8104190f10124..90ae6333f9b4e 100644 --- a/src/algebra/pointwise.lean +++ b/src/algebra/pointwise.lean @@ -194,7 +194,7 @@ lemma empty_mul [has_mul α] : ∅ * s = ∅ := image2_empty_left lemma mul_empty [has_mul α] : s * ∅ = ∅ := image2_empty_right lemma empty_pow [monoid α] (n : ℕ) (hn : n ≠ 0) : (∅ : set α) ^ n = ∅ := -by rw [←nat.sub_add_cancel (nat.pos_of_ne_zero hn), pow_succ, empty_mul] +by rw [← tsub_add_cancel_of_le (nat.succ_le_of_lt $ nat.pos_of_ne_zero hn), pow_succ, empty_mul] instance decidable_mem_mul [monoid α] [fintype α] [decidable_eq α] [decidable_pred (∈ s)] [decidable_pred (∈ t)] : diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean index 3faf3ec43a8c4..de77aa78bad7b 100644 --- a/src/analysis/analytic/basic.lean +++ b/src/analysis/analytic/basic.lean @@ -121,7 +121,8 @@ p.radius_eq_top_of_forall_nnreal_is_O $ λ r, (is_O_zero _ _).congr' (h.mono $ λ n hn, by simp [hn]) eventually_eq.rfl lemma radius_eq_top_of_forall_image_add_eq_zero (n : ℕ) (hn : ∀ m, p (m + n) = 0) : p.radius = ∞ := -p.radius_eq_top_of_eventually_eq_zero $ mem_at_top_sets.2 ⟨n, λ k hk, nat.sub_add_cancel hk ▸ hn _⟩ +p.radius_eq_top_of_eventually_eq_zero $ mem_at_top_sets.2 + ⟨n, λ k hk, tsub_add_cancel_of_le hk ▸ hn _⟩ /-- For `r` strictly smaller than the radius of `p`, then `∥pₙ∥ rⁿ` tends to zero exponentially: for some `0 < a < 1`, `∥p n∥ rⁿ = o(aⁿ)`. -/ @@ -715,7 +716,7 @@ is itself an analytic function of `x` given by the series `p.change_origin_serie def change_origin_series_term (k l : ℕ) (s : finset (fin (k + l))) (hs : s.card = l) : E [×l]→L[𝕜] E [×k]→L[𝕜] F := continuous_multilinear_map.curry_fin_finset 𝕜 E F hs - (by erw [finset.card_compl, fintype.card_fin, hs, nat.add_sub_cancel]) (p $ k + l) + (by erw [finset.card_compl, fintype.card_fin, hs, add_tsub_cancel_right]) (p $ k + l) lemma change_origin_series_term_apply (k l : ℕ) (s : finset (fin (k + l))) (hs : s.card = l) (x y : E) : @@ -783,7 +784,7 @@ with non-definitional equalities. -/ (Σ k l : ℕ, {s : finset (fin (k + l)) // s.card = l}) ≃ Σ n : ℕ, finset (fin n) := { to_fun := λ s, ⟨s.1 + s.2.1, s.2.2⟩, inv_fun := λ s, ⟨s.1 - s.2.card, s.2.card, ⟨s.2.map - (fin.cast $ (nat.sub_add_cancel $ card_finset_fin_le s.2).symm).to_equiv.to_embedding, + (fin.cast $ (tsub_add_cancel_of_le $ card_finset_fin_le s.2).symm).to_equiv.to_embedding, finset.card_map _⟩⟩, left_inv := begin @@ -794,7 +795,7 @@ with non-definitional equalities. -/ suffices : ∀ k' l', k' = k → l' = l → ∀ (hkl : k + l = k' + l') hs', (⟨k', l', ⟨finset.map (fin.cast hkl).to_equiv.to_embedding s, hs'⟩⟩ : (Σ k l : ℕ, {s : finset (fin (k + l)) // s.card = l})) = ⟨k, l, ⟨s, hs⟩⟩, - { apply this; simp only [hs, nat.add_sub_cancel] }, + { apply this; simp only [hs, add_tsub_cancel_right] }, rintro _ _ rfl rfl hkl hs', simp only [equiv.refl_to_embedding, fin.cast_refl, finset.map_refl, eq_self_iff_true, order_iso.refl_to_equiv, and_self, heq_iff_eq] @@ -802,7 +803,7 @@ with non-definitional equalities. -/ right_inv := begin rintro ⟨n, s⟩, - simp [nat.sub_add_cancel (card_finset_fin_le s), fin.cast_to_equiv] + simp [tsub_add_cancel_of_le (card_finset_fin_le s), fin.cast_to_equiv] end } lemma change_origin_series_summable_aux₁ {r r' : ℝ≥0} (hr : (r + r' : ℝ≥0∞) < p.radius) : @@ -816,9 +817,9 @@ begin (λ s : finset (fin n), ∥p (n - s.card + s.card)∥₊ * r ^ s.card * r' ^ (n - s.card)) (∥p n∥₊ * (r + r') ^ n), { intro n, - -- TODO: why `simp only [nat.sub_add_cancel (card_finset_fin_le _)]` fails? + -- TODO: why `simp only [tsub_add_cancel_of_le (card_finset_fin_le _)]` fails? convert_to has_sum (λ s : finset (fin n), ∥p n∥₊ * (r ^ s.card * r' ^ (n - s.card))) _, - { ext1 s, rw [nat.sub_add_cancel (card_finset_fin_le _), mul_assoc] }, + { ext1 s, rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc] }, rw ← fin.sum_pow_mul_eq_add_pow, exact (has_sum_fintype _).mul_left _ }, refine nnreal.summable_sigma.2 ⟨λ n, (this n).summable, _⟩, diff --git a/src/analysis/analytic/composition.lean b/src/analysis/analytic/composition.lean index 0f0b05283927f..6b789341b2acd 100644 --- a/src/analysis/analytic/composition.lean +++ b/src/analysis/analytic/composition.lean @@ -488,7 +488,7 @@ begin refine nnreal.summable_sigma.2 ⟨λ n, (this n).summable, (nnreal.summable_nat_add_iff 1).1 _⟩, convert (nnreal.summable_geometric (nnreal.div_lt_one_of_lt one_lt_two)).mul_left (1 / 4), ext1 n, - rw [(this _).tsum_eq, nat.add_sub_cancel], + rw [(this _).tsum_eq, add_tsub_cancel_right], field_simp [← mul_assoc, pow_succ', mul_pow, show (4 : ℝ≥0) = 2 * 2, from (two_mul 2).symm, mul_right_comm] end diff --git a/src/analysis/asymptotics/asymptotics.lean b/src/analysis/asymptotics/asymptotics.lean index ae5528effff18..b5dbd2365514a 100644 --- a/src/analysis/asymptotics/asymptotics.lean +++ b/src/analysis/asymptotics/asymptotics.lean @@ -1307,7 +1307,7 @@ begin simp only [this, pow_add, nmp], refine is_O.mul_is_o (is_O_refl _ _) ((is_o_one_iff _).2 _), convert (continuous_pow p).tendsto (0 : 𝕜), - exact (zero_pow (nat.sub_pos_of_lt h)).symm + exact (zero_pow (tsub_pos_of_lt h)).symm end theorem is_o_norm_pow_norm_pow {m n : ℕ} (h : m < n) : diff --git a/src/analysis/calculus/specific_functions.lean b/src/analysis/calculus/specific_functions.lean index 2459c6eb36a1d..2b22731aa29c5 100644 --- a/src/analysis/calculus/specific_functions.lean +++ b/src/analysis/calculus/specific_functions.lean @@ -83,7 +83,7 @@ lemma f_aux_deriv (n : ℕ) (x : ℝ) (hx : x ≠ 0) : begin have A : ∀k:ℕ, 2 * (k + 1) - 1 = 2 * k + 1, { assume k, - rw nat.sub_eq_iff_eq_add, + rw tsub_eq_iff_eq_add_of_le, { ring }, { simpa [mul_add] using add_le_add (zero_le (2 * k)) one_le_two } }, convert (((P_aux n).has_deriv_at x).mul diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean index de5334013b83f..beba708cba473 100644 --- a/src/analysis/specific_limits.lean +++ b/src/analysis/specific_limits.lean @@ -65,8 +65,8 @@ sub_add_cancel r 1 ▸ tendsto_add_one_pow_at_top_at_top_of_pos (sub_pos.2 h) lemma nat.tendsto_pow_at_top_at_top_of_one_lt {m : ℕ} (h : 1 < m) : tendsto (λn:ℕ, m ^ n) at_top at_top := -nat.sub_add_cancel (le_of_lt h) ▸ - tendsto_add_one_pow_at_top_at_top_of_pos (nat.sub_pos_of_lt h) +tsub_add_cancel_of_le (le_of_lt h) ▸ + tendsto_add_one_pow_at_top_at_top_of_pos (tsub_pos_of_lt h) lemma tendsto_norm_zero' {𝕜 : Type*} [normed_group 𝕜] : tendsto (norm : 𝕜 → ℝ) (𝓝[{0}ᶜ] 0) (𝓝[set.Ioi 0] 0) := diff --git a/src/combinatorics/composition.lean b/src/combinatorics/composition.lean index 7a6569d08923f..c39e2ab926480 100644 --- a/src/combinatorics/composition.lean +++ b/src/combinatorics/composition.lean @@ -387,7 +387,7 @@ end lemma inv_embedding_comp (i : fin c.length) (j : fin (c.blocks_fun i)) : (c.inv_embedding (c.embedding i j) : ℕ) = j := -by simp_rw [coe_inv_embedding, index_embedding, coe_embedding, nat.add_sub_cancel_left] +by simp_rw [coe_inv_embedding, index_embedding, coe_embedding, add_tsub_cancel_left] /-- Equivalence between the disjoint union of the blocks (each of them seen as `fin (c.blocks_fun i)`) with `fin n`. -/ @@ -645,7 +645,7 @@ begin induction ns with n ns IH; intros l h; simp at h ⊢, { exact (length_eq_zero.1 h.symm).symm }, rw IH, {simp}, - rwa [length_drop, ← h, nat.add_sub_cancel_left] + rwa [length_drop, ← h, add_tsub_cancel_left] end /-- If one splits a list along a composition, and then joins the sublists, one gets back the @@ -749,7 +749,7 @@ finset.card_pos.mpr c.boundaries_nonempty def length : ℕ := finset.card c.boundaries - 1 lemma card_boundaries_eq_succ_length : c.boundaries.card = c.length + 1 := -(nat.sub_eq_iff_eq_add c.card_boundaries_pos).mp rfl +(tsub_eq_iff_eq_add_of_le (nat.succ_le_of_lt c.card_boundaries_pos)).mp rfl lemma length_lt_card_boundaries : c.length < c.boundaries.card := by { rw c.card_boundaries_eq_succ_length, exact lt_add_one _ } diff --git a/src/combinatorics/derangements/finite.lean b/src/combinatorics/derangements/finite.lean index 58ee7553b161b..4bae0101ad9fd 100644 --- a/src/combinatorics/derangements/finite.lean +++ b/src/combinatorics/derangements/finite.lean @@ -103,7 +103,7 @@ theorem num_derangements_sum (n : ℕ) : (num_derangements n : ℤ) = ∑ k in finset.range (n + 1), (-1:ℤ)^k * nat.asc_factorial k (n - k) := begin induction n with n hn, { refl }, - rw [finset.sum_range_succ, num_derangements_succ, hn, finset.mul_sum, nat.sub_self, + rw [finset.sum_range_succ, num_derangements_succ, hn, finset.mul_sum, tsub_self, nat.asc_factorial_zero, int.coe_nat_one, mul_one, pow_succ, neg_one_mul, sub_eq_add_neg, add_left_inj, finset.sum_congr rfl], -- show that (n + 1) * (-1)^x * asc_fac x (n - x) = (-1)^x * asc_fac x (n.succ - x) diff --git a/src/combinatorics/hall/finite.lean b/src/combinatorics/hall/finite.lean index 1924706d8ef03..db339cc948d5e 100644 --- a/src/combinatorics/hall/finite.lean +++ b/src/combinatorics/hall/finite.lean @@ -146,14 +146,14 @@ lemma hall_cond_of_compl {ι : Type u} {t : ι → finset α} {s : finset ι} begin haveI := classical.dec_eq ι, have : s'.card = (s ∪ s'.image coe).card - s.card, - { rw [card_disjoint_union, nat.add_sub_cancel_left, + { rw [card_disjoint_union, add_tsub_cancel_left, card_image_of_injective _ subtype.coe_injective], simp only [disjoint_left, not_exists, mem_image, exists_prop, set_coe.exists, exists_and_distrib_right, exists_eq_right, subtype.coe_mk], intros x hx hc h, exact (hc hx).elim }, rw [this, hus], - apply (nat.sub_le_sub_right (ht _) _).trans _, + apply (tsub_le_tsub_right (ht _) _).trans _, rw ← card_sdiff, { have : (s ∪ s'.image subtype.val).bUnion t \ s.bUnion t ⊆ s'.bUnion (λ x', t x' \ s.bUnion t), { intros t, diff --git a/src/combinatorics/simple_graph/degree_sum.lean b/src/combinatorics/simple_graph/degree_sum.lean index be8db2653e04b..9d874fffb28b3 100644 --- a/src/combinatorics/simple_graph/degree_sum.lean +++ b/src/combinatorics/simple_graph/degree_sum.lean @@ -215,10 +215,10 @@ begin simp only [hc, filter_congr_decidable], rw [←filter_filter, filter_ne', card_erase_of_mem], { use k - 1, - rw [nat.pred_eq_succ_iff, hg, nat.mul_sub_left_distrib, ← nat.sub_add_comm, eq_comm, - ← (nat.sub_eq_iff_eq_add _).symm], + rw [nat.pred_eq_succ_iff, hg, mul_tsub, tsub_add_eq_add_tsub, eq_comm, + tsub_eq_iff_eq_add_of_le], { ring }, - { exact add_le_add_right (zero_le (2 * k)) 2 }, + { exact add_le_add_right (zero_le _) 2 }, { exact nat.mul_le_mul_left _ hk } }, { simpa only [true_and, mem_filter, mem_univ] }, end diff --git a/src/computability/DFA.lean b/src/computability/DFA.lean index 0ed721a448539..778349df0f303 100644 --- a/src/computability/DFA.lean +++ b/src/computability/DFA.lean @@ -79,7 +79,7 @@ begin { intro h, have hlen' := congr_arg list.length h, simp only [list.length_drop, list.length, list.length_take] at hlen', - rw [min_eq_left, nat.sub_eq_zero_iff_le] at hlen', + rw [min_eq_left, tsub_eq_zero_iff_le] at hlen', { apply hneq, apply le_antisymm, assumption' }, diff --git a/src/computability/primrec.lean b/src/computability/primrec.lean index 0ab8b75fcfa67..5374fa3ae0d5b 100644 --- a/src/computability/primrec.lean +++ b/src/computability/primrec.lean @@ -571,7 +571,7 @@ theorem nat_le : primrec_rel ((≤) : ℕ → ℕ → Prop) := λ p, begin dsimp [swap], cases e : p.1 - p.2 with n, - { simp [nat.sub_eq_zero_iff_le.1 e] }, + { simp [tsub_eq_zero_iff_le.1 e] }, { simp [not_le.2 (nat.lt_of_sub_eq_succ e)] } end @@ -1283,7 +1283,7 @@ theorem if_lt {n a b f g} (prec' (sub.comp₂ _ hb ha) hg (tail $ tail hf)).of_eq $ λ v, begin cases e : b v - a v, - { simp [not_lt.2 (nat.le_of_sub_eq_zero e)] }, + { simp [not_lt.2 (tsub_eq_zero_iff_le.mp e)] }, { simp [nat.lt_of_sub_eq_succ e] } end diff --git a/src/computability/turing_machine.lean b/src/computability/turing_machine.lean index 80f91d4e16735..405bd17944b8c 100644 --- a/src/computability/turing_machine.lean +++ b/src/computability/turing_machine.lean @@ -98,7 +98,7 @@ theorem blank_extends.above_of_le {Γ} [inhabited Γ] {l l₁ l₂ : list Γ} : begin rintro ⟨i, rfl⟩ ⟨j, e⟩ h, use i - j, refine list.append_right_cancel (e.symm.trans _), - rw [list.append_assoc, ← list.repeat_add, nat.sub_add_cancel], + rw [list.append_assoc, ← list.repeat_add, tsub_add_cancel_of_le], apply_fun list.length at e, simp only [list.length_append, list.length_repeat] at e, rwa [← add_le_add_iff_left, e, add_le_add_iff_right] @@ -269,7 +269,7 @@ begin swap, { exact (this $ λ i, (H i).symm).symm }, refine quotient.sound' (or.inl ⟨l₂.length - l₁.length, _⟩), refine list.ext_le _ (λ i h h₂, eq.symm _), - { simp only [nat.add_sub_of_le h, list.length_append, list.length_repeat] }, + { simp only [add_tsub_cancel_of_le h, list.length_append, list.length_repeat] }, simp at H, cases lt_or_le i l₁.length with h' h', { simpa only [list.nth_le_append _ h', diff --git a/src/data/bitvec/core.lean b/src/data/bitvec/core.lean index fdb608c1c47c1..3053d766e754e 100644 --- a/src/data/bitvec/core.lean +++ b/src/data/bitvec/core.lean @@ -60,9 +60,9 @@ bitvec.cong by_cases (i ≤ n), { have h₁ := nat.sub_le n i, rw [min_eq_right h], - rw [min_eq_left h₁, ← nat.add_sub_assoc h, nat.add_comm, nat.add_sub_cancel] }, + rw [min_eq_left h₁, ← add_tsub_assoc_of_le h, nat.add_comm, add_tsub_cancel_right] }, { have h₁ := le_of_not_ge h, - rw [min_eq_left h₁, nat.sub_eq_zero_of_le h₁, nat.zero_min, nat.add_zero] } + rw [min_eq_left h₁, tsub_eq_zero_iff_le.mpr h₁, zero_min, nat.add_zero] } end $ repeat fill (min n i) ++ₜ take (n-i) x diff --git a/src/data/buffer/parser/basic.lean b/src/data/buffer/parser/basic.lean index f441a8aa34eeb..00905223fea94 100644 --- a/src/data/buffer/parser/basic.lean +++ b/src/data/buffer/parser/basic.lean @@ -683,7 +683,7 @@ lemma remaining_ne_fail : remaining cb n ≠ fail n' err := by simp [remaining] lemma eof_eq_done {u : unit} : eof cb n = done n' u ↔ n = n' ∧ cb.size ≤ n := -by simp [eof, guard_eq_done, remaining_eq_done, nat.sub_eq_zero_iff_le, and_comm, and_assoc] +by simp [eof, guard_eq_done, remaining_eq_done, tsub_eq_zero_iff_le, and_comm, and_assoc] @[simp] lemma foldr_core_zero_eq_done {f : α → β → β} {p : parser α} {b' : β} : foldr_core f p b 0 cb n ≠ done n' b' := @@ -719,7 +719,7 @@ lemma foldr_eq_fail_iff_mono_at_end {f : α → β → β} {p : parser α} {err [p.mono] (hc : cb.size ≤ n) : foldr f p b cb n = fail n' err ↔ n < n' ∧ (p cb n = fail n' err ∨ ∃ (a : α), p cb n = done n' a ∧ err = dlist.empty) := begin - have : cb.size - n = 0 := nat.sub_eq_zero_of_le hc, + have : cb.size - n = 0 := tsub_eq_zero_iff_le.mpr hc, simp only [foldr, foldr_core_succ_eq_fail, this, and.left_comm, foldr_core_zero_eq_fail, ne_iff_lt_iff_le, exists_and_distrib_right, exists_eq_left, and.congr_left_iff, exists_and_distrib_left], @@ -773,7 +773,7 @@ lemma foldl_eq_fail_iff_mono_at_end {f : β → α → β} {p : parser α} {err [p.mono] (hc : cb.size ≤ n) : foldl f b p cb n = fail n' err ↔ n < n' ∧ (p cb n = fail n' err ∨ ∃ (a : α), p cb n = done n' a ∧ err = dlist.empty) := begin - have : cb.size - n = 0 := nat.sub_eq_zero_of_le hc, + have : cb.size - n = 0 := tsub_eq_zero_iff_le.mpr hc, simp only [foldl, foldl_core_succ_eq_fail, this, and.left_comm, ne_iff_lt_iff_le, exists_eq_left, exists_and_distrib_right, and.congr_left_iff, exists_and_distrib_left, foldl_core_zero_eq_fail], @@ -882,7 +882,7 @@ begin { simp only [digit, sat_eq_done, pure_eq_done, decorate_error_eq_done, bind_eq_done, ←c9], rintro ⟨np, c, ⟨hn, ⟨ge0, le9⟩, rfl, rfl⟩, rfl, rfl⟩, simpa [hn, ge0, le9, true_and, and_true, eq_self_iff_true, exists_prop_of_true, - nat.sub_le_sub_right_iff, l09] using (le_iff_le.mp le9) }, + tsub_le_tsub_iff_right, l09] using (le_iff_le.mp le9) }, { simp only [digit, sat_eq_done, pure_eq_done, decorate_error_eq_done, bind_eq_done, ←c9, le_iff_le], rintro ⟨hn, rfl, -, rfl, ge0, le9⟩, @@ -1851,7 +1851,7 @@ begin have hn : n < cb.size := bounded.of_done hp, subst this, obtain ⟨k, hk⟩ : ∃ k, cb.size - n = k + 1 := - nat.exists_eq_succ_of_ne_zero (ne_of_gt (nat.sub_pos_of_lt hn)), + nat.exists_eq_succ_of_ne_zero (ne_of_gt (tsub_pos_of_lt hn)), cases k, { cases tl; simpa [many_eq_done_nil, nat.sub_succ, hk, many_eq_done, hp, foldr_core_eq_done] using hm }, @@ -1869,7 +1869,7 @@ begin have hn : n < cb.size := bounded.of_done hp, subst this, obtain ⟨k, hk⟩ : ∃ k, cb.size - n = k + 1 := - nat.exists_eq_succ_of_ne_zero (ne_of_gt (nat.sub_pos_of_lt hn)), + nat.exists_eq_succ_of_ne_zero (ne_of_gt (tsub_pos_of_lt hn)), cases k, { cases tl; simpa [many_eq_done_nil, nat.sub_succ, hk, many_eq_done, hp, foldr_core_eq_done] using hm }, @@ -2300,11 +2300,11 @@ begin { simp [hk, add_assoc] }, subst this, simp only [nat.sub_succ, add_comm, ←nat.pred_sub, buffer.length_to_list, nat.pred_one_add, - min_eq_left_iff, list.length_drop, nat.add_sub_cancel_left, list.length_take, - nat.sub_zero], + min_eq_left_iff, list.length_drop, add_tsub_cancel_left, list.length_take, + tsub_zero], -- We now have a goal of proving an inequality dealing with `nat` subtraction and `nat.pred`, -- both of which require special care to provide positivity hypotheses. - rw [nat.sub_le_sub_right_iff, nat.pred_le_iff], + rw [tsub_le_tsub_iff_right, nat.pred_le_iff], { -- We know that `n' ≤ cb.size` because of the `bounded` property, that a parser will not -- produce a `done` result at a position farther than the size of the underlying -- `char_buffer`. @@ -2576,7 +2576,7 @@ begin { -- We rewrite the statement to be a statement about characters instead, and split the -- inequality into the case that our hypotheses prove, and that `'0' ≤ '9'`, which -- is true by computation, handled by `dec_trivial`. - rw [show 9 = '9'.to_nat - '0'.to_nat, from dec_trivial, nat.sub_le_sub_right_iff], + rw [show 9 = '9'.to_nat - '0'.to_nat, from dec_trivial, tsub_le_tsub_iff_right], { exact ho.right }, { dec_trivial } }, -- We rely on the simplifier, mostly powered by `digit_eq_done`, and supply all the @@ -2622,7 +2622,7 @@ begin obtain ⟨m, rfl⟩ : ∃ m, n' = n + m + 1 := nat.exists_eq_add_of_lt hn, -- The following rearrangement lemma is to simplify the `list.take (n' - n)` expression we had have : n + m + 1 - n = m + 1, - { rw [add_assoc, nat.sub_eq_iff_eq_add, add_comm], + { rw [add_assoc, tsub_eq_iff_eq_add_of_le, add_comm], exact nat.le_add_right _ _ }, -- We also have to prove what is the `prod.snd` of the result of the fold of a `list (ℕ × ℕ)` -- with the function above. We use this lemma to finish our inductive case. @@ -2642,7 +2642,7 @@ begin { -- On the way to proving this, we have to actually show that `m ≤ tl.length`, by showing -- that since `tl` was a subsequence in `cb`, and was retrieved from `n + 1` to `n + m + 1`, -- then since `n + m + 1 ≤ cb.size`, we have that `tl` must be at least `m` in length. - simpa [←H.right, ←nat.add_le_to_le_sub _ (hn''.trans_le hn').le, add_comm, add_assoc, + simpa [←H.right, le_tsub_iff_right (hn''.trans_le hn').le, add_comm, add_assoc, add_left_comm] using hn' }, -- Finally, we rely on the simplifier. We already expressions of `nat.of_digits` on both -- the LHS and RHS. All that is left to do is to prove that the summand on the LHS is produced @@ -2666,7 +2666,7 @@ begin -- character. simp only [many1_eq_done, many_eq_done_nil, digit_eq_fail, natm, and.comm, and.left_comm, hdigit, true_and, mul_one, nat.of_digits_singleton, list.take, exists_eq_left, - exists_and_distrib_right, nat.add_sub_cancel_left, eq_self_iff_true, + exists_and_distrib_right, add_tsub_cancel_left, eq_self_iff_true, list.reverse_singleton, zero_add, list.foldr, list.map], -- We take the route of proving that we hit a nonnumeric character, since we already have -- a hypothesis that says that characters at `n'` and past it are nonnumeric. (Note, by now diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index f0463becfd3a4..b03711502d10f 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -92,7 +92,7 @@ begin refine lt_of_le_of_lt (le_trans (le_trans _ (le_abs_self _)) sub_le) this, generalize hk : j - max n i = k, clear this hi₂ hi₁ hi ε0 ε hg sub_le, - rw nat.sub_eq_iff_eq_add ji at hk, + rw tsub_eq_iff_eq_add_of_le ji at hk, rw hk, clear hk ji j, induction k with k' hi, @@ -160,7 +160,7 @@ begin simpa [r_zero, nat.succ_pred_eq_of_pos m_pos, pow_succ] }, generalize hk : m - n.succ = k, have r_pos : 0 < r := lt_of_le_of_ne hr0 (ne.symm r_ne_zero), - replace hk : m = k + n.succ := (nat.sub_eq_iff_eq_add hmn).1 hk, + replace hk : m = k + n.succ := (tsub_eq_iff_eq_add_of_le hmn).1 hk, induction k with k ih generalizing m n, { rw [hk, zero_add, mul_right_comm, inv_pow₀ _ _, ← div_eq_mul_inv, mul_div_cancel], exact (ne_of_lt (pow_pos r_pos _)).symm }, @@ -186,16 +186,16 @@ by rw [sum_sigma', sum_sigma']; exact sum_bij have hb : b₁ < n ∧ b₂ ≤ b₁ := ⟨mem_range.1 (mem_sigma.1 hb).1, nat.le_of_lt_succ (mem_range.1 (mem_sigma.1 hb).2)⟩, have h : a₂ = b₂ ∧ _ := sigma.mk.inj h, - have h' : a₁ = b₁ - b₂ + a₂ := (nat.sub_eq_iff_eq_add ha.2).1 (eq_of_heq h.2), + have h' : a₁ = b₁ - b₂ + a₂ := (tsub_eq_iff_eq_add_of_le ha.2).1 (eq_of_heq h.2), sigma.mk.inj_iff.2 - ⟨nat.sub_add_cancel hb.2 ▸ h'.symm ▸ h.1 ▸ rfl, + ⟨tsub_add_cancel_of_le hb.2 ▸ h'.symm ▸ h.1 ▸ rfl, (heq_of_eq h.1)⟩) (λ ⟨a₁, a₂⟩ ha, have ha : a₁ < n ∧ a₂ < n - a₁ := ⟨mem_range.1 (mem_sigma.1 ha).1, (mem_range.1 (mem_sigma.1 ha).2)⟩, ⟨⟨a₂ + a₁, a₁⟩, ⟨mem_sigma.2 ⟨mem_range.2 (lt_tsub_iff_right.1 ha.2), mem_range.2 (nat.lt_succ_of_le (nat.le_add_left _ _))⟩, - sigma.mk.inj_iff.2 ⟨rfl, heq_of_eq (nat.add_sub_cancel _ _).symm⟩⟩⟩) + sigma.mk.inj_iff.2 ⟨rfl, heq_of_eq (add_tsub_cancel_right _ _).symm⟩⟩⟩) -- TODO move to src/algebra/big_operators/basic.lean, rewrite with comm_group, and make to_additive lemma sum_range_sub_sum_range {α : Type*} [add_comm_group α] {f : ℕ → α} @@ -1139,7 +1139,7 @@ calc x + 1 ≤ lim (⟨(λ n : ℕ, ((exp' x) n).re), is_cau_seq_re (exp' x)⟩ from have h₁ : (((λ m : ℕ, (x ^ m / m! : ℂ)) ∘ nat.succ) 0).re = x, by simp, have h₂ : ((x : ℂ) ^ 0 / 0!).re = 1, by simp, begin - rw [← nat.sub_add_cancel hj, sum_range_succ', sum_range_succ', + rw [← tsub_add_cancel_of_le hj, sum_range_succ', sum_range_succ', add_re, add_re, h₁, h₂, add_assoc, ← coe_re_add_group_hom, (re_add_group_hom).map_sum, coe_re_add_group_hom ], refine le_add_of_nonneg_of_le (sum_nonneg (λ m hm, _)) (le_refl _), @@ -1204,14 +1204,14 @@ calc ∑ m in filter (λ k, n ≤ k) (range j), (1 / m! : α) sum_bij (λ m _, m - n) (λ m hm, mem_range.2 $ (tsub_lt_tsub_iff_right (by simp at hm; tauto)).2 (by simp at hm; tauto)) - (λ m hm, by rw nat.sub_add_cancel; simp at *; tauto) + (λ m hm, by rw tsub_add_cancel_of_le; simp at *; tauto) (λ a₁ a₂ ha₁ ha₂ h, - by rwa [nat.sub_eq_iff_eq_add, ← nat.sub_add_comm, eq_comm, nat.sub_eq_iff_eq_add, + by rwa [tsub_eq_iff_eq_add_of_le, tsub_add_eq_add_tsub, eq_comm, tsub_eq_iff_eq_add_of_le, add_left_inj, eq_comm] at h; simp at *; tauto) (λ b hb, ⟨b + n, mem_filter.2 ⟨mem_range.2 $ lt_tsub_iff_right.mp (mem_range.1 hb), nat.le_add_left _ _⟩, - by rw nat.add_sub_cancel⟩) + by rw add_tsub_cancel_right⟩) ... ≤ ∑ m in range (j - n), (n! * n.succ ^ m)⁻¹ : begin refine sum_le_sum (assume m n, _), @@ -1286,7 +1286,7 @@ begin simp_rw [←sub_eq_add_neg], show abs (∑ m in range j, x ^ m / m! - ∑ m in range n, x ^ m / m!) ≤ abs x ^ n / (n!) * 2, let k := j - n, - have hj : j = n + k := (nat.add_sub_of_le hj).symm, + have hj : j = n + k := (add_tsub_cancel_of_le hj).symm, rw [hj, sum_range_add_sub_sum_range], calc abs (∑ (i : ℕ) in range k, x ^ (n + i) / ((n + i)! : ℂ)) ≤ ∑ (i : ℕ) in range k, abs (x ^ (n + i) / ((n + i)! : ℂ)) : abv_sum_le_sum_abv _ _ diff --git a/src/data/equiv/list.lean b/src/data/equiv/list.lean index 0ddcd0e238ffa..a78557c219daa 100644 --- a/src/data/equiv/list.lean +++ b/src/data/equiv/list.lean @@ -226,13 +226,13 @@ def raise : list ℕ → ℕ → list ℕ lemma lower_raise : ∀ l n, lower (raise l n) n = l | [] n := rfl -| (m :: l) n := by rw [raise, lower, nat.add_sub_cancel, lower_raise] +| (m :: l) n := by rw [raise, lower, add_tsub_cancel_right, lower_raise] lemma raise_lower : ∀ {l n}, list.sorted (≤) (n :: l) → raise (lower l n) n = l | [] n h := rfl | (m :: l) n h := have n ≤ m, from list.rel_of_sorted_cons h _ (l.mem_cons_self _), - by simp [raise, lower, nat.sub_add_cancel this, + by simp [raise, lower, tsub_add_cancel_of_le this, raise_lower (list.sorted_of_sorted_cons h)] lemma raise_chain : ∀ l n, list.chain (≤) n (raise l n) @@ -273,13 +273,13 @@ def raise' : list ℕ → ℕ → list ℕ lemma lower_raise' : ∀ l n, lower' (raise' l n) n = l | [] n := rfl -| (m :: l) n := by simp [raise', lower', nat.add_sub_cancel, lower_raise'] +| (m :: l) n := by simp [raise', lower', add_tsub_cancel_right, lower_raise'] lemma raise_lower' : ∀ {l n}, (∀ m ∈ l, n ≤ m) → list.sorted (<) l → raise' (lower' l n) n = l | [] n h₁ h₂ := rfl | (m :: l) n h₁ h₂ := have n ≤ m, from h₁ _ (l.mem_cons_self _), - by simp [raise', lower', nat.sub_add_cancel this, raise_lower' + by simp [raise', lower', tsub_add_cancel_of_le this, raise_lower' (list.rel_of_sorted_cons h₂ : ∀ a ∈ l, m < a) (list.sorted_of_sorted_cons h₂)] lemma raise'_chain : ∀ l {m n}, m < n → list.chain (<) m (raise' l n) diff --git a/src/data/fin/basic.lean b/src/data/fin/basic.lean index dd7ad0426d7b4..14abcaf67191a 100644 --- a/src/data/fin/basic.lean +++ b/src/data/fin/basic.lean @@ -785,7 +785,7 @@ by { cases i, refl } @[simp] lemma pred_mk_succ (i : ℕ) (h : i < n + 1) : fin.pred ⟨i + 1, add_lt_add_right h 1⟩ (ne_of_vne (ne_of_gt (mk_succ_pos i h))) = ⟨i, h⟩ := -by simp only [ext_iff, coe_pred, coe_mk, nat.add_sub_cancel] +by simp only [ext_iff, coe_pred, coe_mk, add_tsub_cancel_right] -- This is not a simp lemma by default, because `pred_mk_succ` is nicer when it applies. lemma pred_mk {n : ℕ} (i : ℕ) (h : i < n + 1) (w) : @@ -812,7 +812,7 @@ by rw [←succ_lt_succ_iff, succ_pred, succ_pred] lemma pred_add_one (i : fin (n + 2)) (h : (i : ℕ) < n + 1) : pred (i + 1) (ne_of_gt (add_one_pos _ (lt_iff_coe_lt_coe.mpr h))) = cast_lt i h := begin - rw [ext_iff, coe_pred, coe_cast_lt, coe_add, coe_one, mod_eq_of_lt, nat.add_sub_cancel], + rw [ext_iff, coe_pred, coe_cast_lt, coe_add, coe_one, mod_eq_of_lt, add_tsub_cancel_right], exact add_lt_add_right h 1, end @@ -833,11 +833,11 @@ by simp [eq_iff_veq] @[simp] lemma add_nat_sub_nat {i : fin (n + m)} (h : m ≤ i) : add_nat m (sub_nat m i h) = i := -ext $ nat.sub_add_cancel h +ext $ tsub_add_cancel_of_le h @[simp] lemma sub_nat_add_nat (i : fin n) (m : ℕ) (h : m ≤ add_nat m i := le_coe_add_nat m i) : sub_nat m (add_nat m i) h = i := -ext $ nat.add_sub_cancel i m +ext $ add_tsub_cancel_right i m @[simp] lemma nat_add_sub_nat_cast {i : fin (n + m)} (h : n ≤ i) : nat_add n (sub_nat n (cast (add_comm _ _) i) h) = i := @@ -1053,7 +1053,7 @@ instance (n : ℕ) : has_neg (fin n) := /-- Abelian group structure on `fin (n+1)`. -/ instance (n : ℕ) : add_comm_group (fin (n+1)) := { add_left_neg := λ ⟨a, ha⟩, fin.ext $ trans (nat.mod_add_mod _ _ _) $ - by { rw [fin.coe_mk, fin.coe_zero, nat.sub_add_cancel, nat.mod_self], exact le_of_lt ha }, + by { rw [fin.coe_mk, fin.coe_zero, tsub_add_cancel_of_le, nat.mod_self], exact le_of_lt ha }, sub_eq_add_neg := λ ⟨a, ha⟩ ⟨b, hb⟩, fin.ext $ show (a + (n + 1 - b)) % (n + 1) = (a + (n + 1 - b) % (n + 1)) % (n + 1), by simp, sub := fin.sub, diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean index ced44b3d6fc50..dcb70dde64e5f 100644 --- a/src/data/finset/basic.lean +++ b/src/data/finset/basic.lean @@ -1630,7 +1630,7 @@ lemma mem_range_le {n x : ℕ} (hx : x ∈ range n) : x ≤ n := (mem_range.1 hx).le lemma mem_range_sub_ne_zero {n x : ℕ} (hx : x ∈ range n) : n - x ≠ 0 := -ne_of_gt $ nat.sub_pos_of_lt $ mem_range.1 hx +ne_of_gt $ tsub_pos_of_lt $ mem_range.1 hx @[simp] lemma nonempty_range_iff : (range n).nonempty ↔ n ≠ 0 := ⟨λ ⟨k, hk⟩, ((zero_le k).trans_lt $ mem_range.1 hk).ne', @@ -1671,10 +1671,10 @@ def not_mem_range_equiv (k : ℕ) : {n // n ∉ range k} ≃ ℕ := begin assume j, rw subtype.ext_iff_val, - apply nat.sub_add_cancel, + apply tsub_add_cancel_of_le, simpa using j.2 end, - right_inv := λ j, nat.add_sub_cancel _ _ } + right_inv := λ j, add_tsub_cancel_right _ _ } @[simp] lemma coe_not_mem_range_equiv (k : ℕ) : (not_mem_range_equiv k : {n // n ∉ range k} → ℕ) = (λ i, i - k) := rfl @@ -2921,7 +2921,7 @@ by rw [← card_union_add_card_inter, disjoint_iff_inter_eq_empty.1 h, card_empt theorem card_sdiff {s t : finset α} (h : s ⊆ t) : card (t \ s) = card t - card s := suffices card (t \ s) = card ((t \ s) ∪ s) - card s, by rwa sdiff_union_of_subset h at this, -by rw [card_disjoint_union sdiff_disjoint, nat.add_sub_cancel] +by rw [card_disjoint_union sdiff_disjoint, add_tsub_cancel_right] lemma card_sdiff_add_card {s t : finset α} : (s \ t).card + t.card = (s ∪ t).card := by rw [← card_disjoint_union sdiff_disjoint, sdiff_union_self_eq_union] @@ -2994,7 +2994,7 @@ begin { exact ⟨A, h₂, subset.refl _, h.symm⟩ }, { have : (A \ B).nonempty, { rw [← card_pos, card_sdiff h₂, ← h, nat.add_right_comm, - nat.add_sub_cancel, nat.add_succ], + add_tsub_cancel_right, nat.add_succ], apply nat.succ_pos }, rcases this with ⟨a, ha⟩, have z : i + card B + k = card (erase A a), diff --git a/src/data/hash_map.lean b/src/data/hash_map.lean index 048ef0bdd822f..85cf61a04c725 100644 --- a/src/data/hash_map.lean +++ b/src/data/hash_map.lean @@ -256,7 +256,7 @@ section rcases append_of_modify u v1 v2 w hl hfl with ⟨u', w', e₁, e₂⟩, rw [← v.len, e₁], suffices : valid bkts' (u' ++ v2 ++ w').length, - { simpa [ge, add_comm, add_left_comm, nat.le_add_right, nat.add_sub_cancel_left] }, + { simpa [ge, add_comm, add_left_comm, nat.le_add_right, add_tsub_cancel_left] }, refine ⟨congr_arg _ e₂, λ i a, _, λ i, _⟩, { by_cases bidx = i, { subst i, rw [bkts', array.read_write, hfl], diff --git a/src/data/int/basic.lean b/src/data/int/basic.lean index 21d2196f1a84a..8b492e6a11138 100644 --- a/src/data/int/basic.lean +++ b/src/data/int/basic.lean @@ -1024,7 +1024,7 @@ theorem of_nat_add_neg_succ_of_nat_of_ge {m n : ℕ} begin change sub_nat_nat _ _ = _, have h' : n.succ - m = 0, - apply nat.sub_eq_zero_of_le h, + apply tsub_eq_zero_iff_le.mpr h, simp [*, sub_nat_nat] end @@ -1346,15 +1346,15 @@ lemma shiftl_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), shiftl m (n + k) = shiftl | (m : ℕ) n -[1+k] := sub_nat_nat_elim n k.succ (λ n k i, shiftl ↑m i = nat.shiftr (nat.shiftl m n) k) (λ i n, congr_arg coe $ - by rw [← nat.shiftl_sub, nat.add_sub_cancel_left]; apply nat.le_add_right) + by rw [← nat.shiftl_sub, add_tsub_cancel_left]; apply nat.le_add_right) (λ i n, congr_arg coe $ - by rw [add_assoc, nat.shiftr_add, ← nat.shiftl_sub, nat.sub_self]; refl) + by rw [add_assoc, nat.shiftr_add, ← nat.shiftl_sub, tsub_self]; refl) | -[1+ m] n -[1+k] := sub_nat_nat_elim n k.succ (λ n k i, shiftl -[1+ m] i = -[1+ nat.shiftr (nat.shiftl' tt m n) k]) (λ i n, congr_arg neg_succ_of_nat $ - by rw [← nat.shiftl'_sub, nat.add_sub_cancel_left]; apply nat.le_add_right) + by rw [← nat.shiftl'_sub, add_tsub_cancel_left]; apply nat.le_add_right) (λ i n, congr_arg neg_succ_of_nat $ - by rw [add_assoc, nat.shiftr_add, ← nat.shiftl'_sub, nat.sub_self]; refl) + by rw [add_assoc, nat.shiftr_add, ← nat.shiftl'_sub, tsub_self]; refl) lemma shiftl_sub (m : ℤ) (n : ℕ) (k : ℤ) : shiftl m (n - k) = shiftr (shiftl m n) k := shiftl_add _ _ _ diff --git a/src/data/int/cast.lean b/src/data/int/cast.lean index 516d76b888216..0a27981734db4 100644 --- a/src/data/int/cast.lean +++ b/src/data/int/cast.lean @@ -69,7 +69,7 @@ end ((int.sub_nat_nat m n : ℤ) : α) = m - n := begin unfold sub_nat_nat, cases e : n - m, - { simp [sub_nat_nat, e, nat.le_of_sub_eq_zero e] }, + { simp [sub_nat_nat, e, tsub_eq_zero_iff_le.mp e] }, { rw [sub_nat_nat, cast_neg_succ_of_nat, ← nat.cast_succ, ← e, nat.cast_sub $ _root_.le_of_lt $ nat.lt_of_sub_eq_succ e, neg_sub] }, end diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean index 5c5a0bbf837da..3a4d64a29f161 100644 --- a/src/data/list/basic.lean +++ b/src/data/list/basic.lean @@ -1176,7 +1176,8 @@ lemma nth_le_append_right : ∀ {l₁ l₂ : list α} {n : ℕ} (h₁ : l₁.len | (a :: l) _ (n+1) h₁ h₂ := begin dsimp, - conv { to_rhs, congr, skip, rw [←nat.sub_sub, nat.sub.right_comm, nat.add_sub_cancel], }, + conv { to_rhs, congr, skip, + rw [tsub_add_eq_tsub_tsub, tsub_right_comm, add_tsub_cancel_right], }, rw nth_le_append_right (nat.lt_succ_iff.mp h₁), end @@ -1269,7 +1270,7 @@ theorem nth_le_reverse_aux2 : ∀ (l r : list α) (i : nat) (h1) (h2), have aux := nth_le_reverse_aux2 l (a :: r) i, have heq := calc length (a :: l) - 1 - (i + 1) = length l - (1 + i) : by rw add_comm; refl - ... = length l - 1 - i : by rw nat.sub_sub, + ... = length l - 1 - i : by rw ← tsub_add_eq_tsub_tsub, rw [← heq] at aux, apply aux end @@ -1309,12 +1310,12 @@ lemma modify_nth_tail_modify_nth_tail_le l.modify_nth_tail (λl, (f l).modify_nth_tail g (m - n)) n := begin rcases le_iff_exists_add.1 h with ⟨m, rfl⟩, - rw [nat.add_sub_cancel_left, add_comm, modify_nth_tail_modify_nth_tail] + rw [add_tsub_cancel_left, add_comm, modify_nth_tail_modify_nth_tail] end lemma modify_nth_tail_modify_nth_tail_same {f g : list α → list α} (n : ℕ) (l:list α) : (l.modify_nth_tail f n).modify_nth_tail g n = l.modify_nth_tail (g ∘ f) n := -by rw [modify_nth_tail_modify_nth_tail_le n n l (le_refl n), nat.sub_self]; refl +by rw [modify_nth_tail_modify_nth_tail_le n n l (le_refl n), tsub_self]; refl lemma modify_nth_tail_id : ∀n (l:list α), l.modify_nth_tail id n = l @@ -1716,8 +1717,8 @@ theorem take_left' {l₁ l₂ : list α} {n} (h : length l₁ = n) : by rw ← h; apply take_left theorem take_take : ∀ (n m) (l : list α), take n (take m l) = take (min n m) l -| n 0 l := by rw [nat.min_zero, take_zero, take_nil] -| 0 m l := by rw [nat.zero_min, take_zero, take_zero] +| n 0 l := by rw [min_zero, take_zero, take_nil] +| 0 m l := by rw [zero_min, take_zero, take_zero] | (succ n) (succ m) nil := by simp only [take_nil] | (succ n) (succ m) (a::l) := by simp only [take, min_succ_succ, take_take n m l]; split; refl @@ -1809,7 +1810,7 @@ by simp [init_eq_take, min_eq_left_of_lt h, take_take, pred_le] @[simp] lemma drop_eq_nil_of_le {l : list α} {k : ℕ} (h : l.length ≤ k) : l.drop k = [] := -by simpa [←length_eq_zero] using nat.sub_eq_zero_of_le h +by simpa [←length_eq_zero] using tsub_eq_zero_iff_le.mpr h lemma drop_eq_nil_iff_le {l : list α} {k : ℕ} : l.drop k = [] ↔ l.length ≤ k := @@ -1980,14 +1981,14 @@ lemma reverse_take {α} {xs : list α} (n : ℕ) xs.reverse.take n = (xs.drop (xs.length - n)).reverse := begin induction xs generalizing n; - simp only [reverse_cons, drop, reverse_nil, nat.zero_sub, length, take_nil], + simp only [reverse_cons, drop, reverse_nil, zero_tsub, length, take_nil], cases h.lt_or_eq_dec with h' h', { replace h' := le_of_succ_le_succ h', rwa [take_append_of_le_length, xs_ih _ h'], rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n), from _, drop], - { rwa [succ_eq_add_one, nat.sub_add_comm] }, + { rwa [succ_eq_add_one, ← tsub_add_eq_add_tsub] }, { rwa length_reverse } }, - { subst h', rw [length, nat.sub_self, drop], + { subst h', rw [length, tsub_self, drop], suffices : xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length, by rw [this, take_length, reverse_cons], rw [length_append, length_reverse], refl } @@ -2707,7 +2708,7 @@ lemma head_le_sum (L : list ℕ) : L.head ≤ L.sum := nat.le.intro (head_add_tail_sum L) lemma tail_sum (L : list ℕ) : L.tail.sum = L.sum - L.head := -by rw [← head_add_tail_sum L, add_comm, nat.add_sub_cancel] +by rw [← head_add_tail_sum L, add_comm, add_tsub_cancel_right] section variables {G : Type*} [comm_group G] @@ -3735,7 +3736,7 @@ theorem prefix_iff_eq_append {l₁ l₂ : list α} : l₁ <+: l₂ ↔ l₁ ++ d theorem suffix_iff_eq_append {l₁ l₂ : list α} : l₁ <:+ l₂ ↔ take (length l₂ - length l₁) l₂ ++ l₁ = l₂ := -⟨by rintros ⟨r, rfl⟩; simp only [length_append, nat.add_sub_cancel, take_left], λ e, ⟨_, e⟩⟩ +⟨by rintros ⟨r, rfl⟩; simp only [length_append, add_tsub_cancel_right, take_left], λ e, ⟨_, e⟩⟩ theorem prefix_iff_eq_take {l₁ l₂ : list α} : l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂ := ⟨λ h, append_right_cancel $ diff --git a/src/data/list/cycle.lean b/src/data/list/cycle.lean index 5feb9eb0f223c..452345150bc77 100644 --- a/src/data/list/cycle.lean +++ b/src/data/list/cycle.lean @@ -379,9 +379,9 @@ begin rw ←nth_le_pmap l.reverse.prev (λ _ h, h), { simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse, length_reverse, nat.mod_eq_of_lt (tsub_lt_self lpos nat.succ_pos'), - nat.sub_sub_self (nat.succ_le_of_lt lpos)], + tsub_tsub_cancel_of_le (nat.succ_le_of_lt lpos)], rw ←nth_le_reverse, - { simp [nat.sub_sub_self (nat.le_pred_of_lt hk)] }, + { simp [tsub_tsub_cancel_of_le (nat.le_pred_of_lt hk)] }, { simpa using (nat.sub_le _ _).trans_lt (tsub_lt_self lpos nat.succ_pos') } }, { simpa using (nat.sub_le _ _).trans_lt (tsub_lt_self lpos nat.succ_pos') } end diff --git a/src/data/list/intervals.lean b/src/data/list/intervals.lean index fa68a2c5c42e2..5c54a2ac9d7ca 100644 --- a/src/data/list/intervals.lean +++ b/src/data/list/intervals.lean @@ -35,33 +35,33 @@ def Ico (n m : ℕ) : list ℕ := range' n (m - n) namespace Ico theorem zero_bot (n : ℕ) : Ico 0 n = range n := -by rw [Ico, nat.sub_zero, range_eq_range'] +by rw [Ico, tsub_zero, range_eq_range'] @[simp] theorem length (n m : ℕ) : length (Ico n m) = m - n := -by dsimp [Ico]; simp only [length_range'] +by { dsimp [Ico], simp only [length_range'] } theorem pairwise_lt (n m : ℕ) : pairwise (<) (Ico n m) := -by dsimp [Ico]; simp only [pairwise_lt_range'] +by { dsimp [Ico], simp only [pairwise_lt_range'] } theorem nodup (n m : ℕ) : nodup (Ico n m) := -by dsimp [Ico]; simp only [nodup_range'] +by { dsimp [Ico], simp only [nodup_range'] } @[simp] theorem mem {n m l : ℕ} : l ∈ Ico n m ↔ n ≤ l ∧ l < m := suffices n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m, by simp [Ico, this], begin cases le_total n m with hnm hmn, - { rw [nat.add_sub_of_le hnm] }, - { rw [nat.sub_eq_zero_of_le hmn, add_zero], + { rw [add_tsub_cancel_of_le hnm] }, + { rw [tsub_eq_zero_iff_le.mpr hmn, add_zero], exact and_congr_right (assume hnl, iff.intro (assume hln, (not_le_of_gt hln hnl).elim) (assume hlm, lt_of_lt_of_le hlm hmn)) } end theorem eq_nil_of_le {n m : ℕ} (h : m ≤ n) : Ico n m = [] := -by simp [Ico, nat.sub_eq_zero_of_le h] +by simp [Ico, tsub_eq_zero_iff_le.mpr h] theorem map_add (n m k : ℕ) : (Ico n m).map ((+) k) = Ico (n + k) (m + k) := -by rw [Ico, Ico, map_add_range', add_tsub_add_right_eq_tsub, add_comm n k] +by rw [Ico, Ico, map_add_range', add_tsub_add_eq_tsub_right, add_comm n k] theorem map_sub (n m k : ℕ) (h₁ : k ≤ n) : (Ico n m).map (λ x, x - k) = Ico (n - k) (m - k) := begin @@ -71,7 +71,7 @@ begin rw [map_sub_range' _ _ _ h₁] }, { simp at h₂, rw [eq_nil_of_le h₂], - rw [eq_nil_of_le (nat.sub_le_sub_right h₂ _)], + rw [eq_nil_of_le (tsub_le_tsub_right h₂ _)], refl } end @@ -79,15 +79,15 @@ end eq_nil_of_le (le_refl n) @[simp] theorem eq_empty_iff {n m : ℕ} : Ico n m = [] ↔ m ≤ n := -iff.intro (assume h, nat.le_of_sub_eq_zero $ by rw [← length, h]; refl) eq_nil_of_le +iff.intro (assume h, tsub_eq_zero_iff_le.mp $ by rw [← length, h, list.length]) eq_nil_of_le lemma append_consecutive {n m l : ℕ} (hnm : n ≤ m) (hml : m ≤ l) : Ico n m ++ Ico m l = Ico n l := begin dunfold Ico, convert range'_append _ _ _, - { exact (nat.add_sub_of_le hnm).symm }, - { rwa [← nat.add_sub_assoc hnm, nat.sub_add_cancel] } + { exact (add_tsub_cancel_of_le hnm).symm }, + { rwa [← add_tsub_assoc_of_le hnm, tsub_add_cancel_of_le] } end @[simp] lemma inter_consecutive (n m l : ℕ) : Ico n m ∩ Ico m l = [] := @@ -104,16 +104,16 @@ end (bag_inter_nil_iff_inter_nil _ _).2 (inter_consecutive n m l) @[simp] theorem succ_singleton {n : ℕ} : Ico n (n+1) = [n] := -by dsimp [Ico]; simp [nat.add_sub_cancel_left] +by { dsimp [Ico], simp [add_tsub_cancel_left] } theorem succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = Ico n m ++ [m] := -by rwa [← succ_singleton, append_consecutive]; exact nat.le_succ _ +by { rwa [← succ_singleton, append_consecutive], exact nat.le_succ _ } theorem eq_cons {n m : ℕ} (h : n < m) : Ico n m = n :: Ico (n + 1) m := -by rw [← append_consecutive (nat.le_succ n) h, succ_singleton]; refl +by { rw [← append_consecutive (nat.le_succ n) h, succ_singleton], refl } @[simp] theorem pred_singleton {m : ℕ} (h : 0 < m) : Ico (m - 1) m = [m - 1] := -by dsimp [Ico]; rw nat.sub_sub_self h; simp +by { dsimp [Ico], rw tsub_tsub_cancel_of_le (succ_le_of_lt h), simp } theorem chain'_succ (n m : ℕ) : chain' (λa b, b = succ a) (Ico n m) := begin @@ -123,7 +123,7 @@ begin end @[simp] theorem not_mem_top {n m : ℕ} : m ∉ Ico n m := -by simp; intros; refl +by simp lemma filter_lt_of_top_le {n m l : ℕ} (hml : m ≤ l) : (Ico n m).filter (λ x, x < l) = Ico n m := filter_eq_self.2 $ assume k hk, lt_of_lt_of_le (mem.1 hk).2 hml diff --git a/src/data/list/nat_antidiagonal.lean b/src/data/list/nat_antidiagonal.lean index 425741eb2c28d..baa368e6e35a5 100644 --- a/src/data/list/nat_antidiagonal.lean +++ b/src/data/list/nat_antidiagonal.lean @@ -32,10 +32,10 @@ def antidiagonal (n : ℕ) : list (ℕ × ℕ) := x ∈ antidiagonal n ↔ x.1 + x.2 = n := begin rw [antidiagonal, mem_map], split, - { rintros ⟨i, hi, rfl⟩, rw [mem_range, lt_succ_iff] at hi, exact nat.add_sub_of_le hi }, + { rintros ⟨i, hi, rfl⟩, rw [mem_range, lt_succ_iff] at hi, exact add_tsub_cancel_of_le hi }, { rintro rfl, refine ⟨x.fst, _, _⟩, { rw [mem_range, add_assoc, lt_add_iff_pos_right], exact zero_lt_succ _ }, - { exact prod.ext rfl (nat.add_sub_cancel_left _ _) } } + { exact prod.ext rfl (add_tsub_cancel_left _ _) } } end /-- The length of the antidiagonal of `n` is `n + 1`. -/ @@ -54,7 +54,7 @@ nodup_map (@left_inverse.injective ℕ (ℕ × ℕ) prod.fst (λ i, (i, n-i)) $ antidiagonal (n + 1) = (0, n + 1) :: ((antidiagonal n).map (prod.map nat.succ id) ) := begin simp only [antidiagonal, range_succ_eq_map, map_cons, true_and, nat.add_succ_sub_one, add_zero, - id.def, eq_self_iff_true, nat.sub_zero, map_map, prod.map_mk], + id.def, eq_self_iff_true, tsub_zero, map_map, prod.map_mk], apply congr (congr rfl _) rfl, ext; simp, end diff --git a/src/data/list/nodup_equiv_fin.lean b/src/data/list/nodup_equiv_fin.lean index 52e91d4c08c2f..e8c4a863d7d4f 100644 --- a/src/data/list/nodup_equiv_fin.lean +++ b/src/data/list/nodup_equiv_fin.lean @@ -88,10 +88,10 @@ begin rw [eq_comm, list.nth_eq_some] at this, obtain ⟨w, h⟩ := this, let f' : ℕ ↪o ℕ := order_embedding.of_map_le_iff (λ i, f (i + 1) - (f 0 + 1)) - (λ a b, by simp [nat.sub_le_sub_right_iff, nat.succ_le_iff, nat.lt_succ_iff]), + (λ a b, by simp [tsub_le_tsub_iff_right, nat.succ_le_iff, nat.lt_succ_iff]), have : ∀ ix, tl.nth ix = (l'.drop (f 0 + 1)).nth (f' ix), { intro ix, - simp [list.nth_drop, nat.add_sub_of_le, nat.succ_le_iff, ←hf] }, + simp [list.nth_drop, add_tsub_cancel_of_le, nat.succ_le_iff, ←hf] }, rw [←list.take_append_drop (f 0 + 1) l', ←list.singleton_append], apply list.sublist.append _ (IH _ this), rw [list.singleton_sublist, ←h, l'.nth_le_take _ (nat.lt_succ_self _)], diff --git a/src/data/list/perm.lean b/src/data/list/perm.lean index 3317a3283a8a0..712bdcac4d58b 100644 --- a/src/data/list/perm.lean +++ b/src/data/list/perm.lean @@ -1024,7 +1024,7 @@ begin by_cases h'' : n ≤ xs.length, { let n' := xs.length - n, have h₀ : n = xs.length - n', - { dsimp [n'], rwa nat.sub_sub_self, } , + { dsimp [n'], rwa tsub_tsub_cancel_of_le, } , have h₁ : n' ≤ xs.length, { apply tsub_le_self }, have h₂ : xs.drop n = (xs.reverse.take n').reverse, @@ -1036,7 +1036,7 @@ begin apply (reverse_perm _).trans; assumption, }, { have : drop n xs = [], { apply eq_nil_of_length_eq_zero, - rw [length_drop, nat.sub_eq_zero_iff_le], + rw [length_drop, tsub_eq_zero_iff_le], apply le_of_not_ge h'' }, simp [this, list.inter], } end diff --git a/src/data/list/range.lean b/src/data/list/range.lean index db58125628a7f..7732a69fe7575 100644 --- a/src/data/list/range.lean +++ b/src/data/list/range.lean @@ -78,7 +78,7 @@ theorem nodup_range' (s n : ℕ) : nodup (range' s n) := theorem range'_sublist_right {s m n : ℕ} : range' s m <+ range' s n ↔ m ≤ n := ⟨λ h, by simpa only [length_range'] using length_le_of_sublist h, - λ h, by rw [← nat.sub_add_cancel h, ← range'_append]; apply sublist_append_left⟩ + λ h, by rw [← tsub_add_cancel_of_le h, ← range'_append]; apply sublist_append_left⟩ theorem range'_subset_right {s m n : ℕ} : range' s m ⊆ range' s n ↔ m ≤ n := ⟨λ h, le_of_not_lt $ λ hn, lt_irrefl (s+n) $ @@ -171,7 +171,7 @@ theorem reverse_range' : ∀ s n : ℕ, | s (n+1) := by rw [range'_concat, reverse_append, range_succ_eq_map]; simpa only [show s + (n + 1) - 1 = s + n, from rfl, (∘), λ a i, show a - 1 - i = a - succ i, from pred_sub _ _, - reverse_singleton, map_cons, nat.sub_zero, cons_append, + reverse_singleton, map_cons, tsub_zero, cons_append, nil_append, eq_self_iff_true, true_and, map_map] using reverse_range' s n diff --git a/src/data/list/rotate.lean b/src/data/list/rotate.lean index 31dc996ae06f1..2b66eb45cc505 100644 --- a/src/data/list/rotate.lean +++ b/src/data/list/rotate.lean @@ -238,7 +238,7 @@ begin { have mpos : 0 < m := k.zero_le.trans_lt hk, have hm : m - n % m < m := tsub_lt_self mpos hn, have hn' : n % m < m := nat.mod_lt _ mpos, - simpa [mod_eq_of_lt hm, nat.sub_add_cancel hn'.le] using nat.mod_eq_of_lt hk } + simpa [mod_eq_of_lt hm, tsub_add_cancel_of_le hn'.le] using nat.mod_eq_of_lt hk } end lemma rotate_injective (n : ℕ) : function.injective (λ l : list α, l.rotate n) := @@ -264,7 +264,7 @@ begin { rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil, rotate_eq_nil_iff] }, { cases (nat.zero_le (n % l'.length)).eq_or_lt with hn hn, { simp [←hn] }, - { rw [mod_eq_of_lt (tsub_lt_self hl hn), nat.sub_add_cancel, mod_self, rotate_zero], + { rw [mod_eq_of_lt (tsub_lt_self hl hn), tsub_add_cancel_of_le, mod_self, rotate_zero], exact (nat.mod_lt _ hl).le } } end @@ -294,7 +294,7 @@ begin { simp }, { have : k'.succ < (x :: l).length, { simp [←hk', hk, nat.mod_lt] }, - rw [nat.mod_eq_of_lt, nat.sub_add_cancel, rotate_length], + rw [nat.mod_eq_of_lt, tsub_add_cancel_of_le, rotate_length], { exact tsub_le_self }, { exact tsub_lt_self (by simp) nat.succ_pos' } } } end @@ -320,7 +320,7 @@ begin rw nodup_iff_nth_le_inj at hl, refine hl _ _ (mod_lt _ hl') hl' _, rw ←nth_le_rotate' _ n, - simp_rw [h, nat.sub_add_cancel (mod_lt _ hl').le, mod_self] }, + simp_rw [h, tsub_add_cancel_of_le (mod_lt _ hl').le, mod_self] }, { rintro (h|h), { rw [←rotate_mod, h], exact rotate_zero l }, @@ -334,7 +334,7 @@ begin have hj : j % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hn), refine (nodup_iff_nth_le_inj.mp hl) _ _ hi hj _, rw [←nth_le_rotate' l i, ←nth_le_rotate' l j], - simp [nat.sub_add_cancel, hi.le, hj.le, h] + simp [tsub_add_cancel_of_le, hi.le, hj.le, h] end section is_rotated @@ -595,7 +595,7 @@ begin refine ⟨k % l.length, _⟩, have hk' : k % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hl), rw [←nth_le_cyclic_permutations _ _ (hk'.trans_le hl'.ge), ←nth_le_rotate' _ k], - simp [hk, hl', nat.sub_add_cancel hk'.le] + simp [hk, hl', tsub_add_cancel_of_le hk'.le] end section decidable diff --git a/src/data/list/zip.lean b/src/data/list/zip.lean index 1f7603843ab2a..a59f35c18c338 100644 --- a/src/data/list/zip.lean +++ b/src/data/list/zip.lean @@ -55,7 +55,7 @@ zip_with_nil_right _ l @[simp] theorem length_zip_with (f : α → β → γ) : ∀ (l₁ : list α) (l₂ : list β), length (zip_with f l₁ l₂) = min (length l₁) (length l₂) | [] l₂ := rfl -| l₁ [] := by simp only [length, nat.min_zero, zip_with_nil_right] +| l₁ [] := by simp only [length, min_zero, zip_with_nil_right] | (a::l₁) (b::l₂) := by simp [length, zip_cons_cons, length_zip_with l₁ l₂, min_add_add_right] @[simp] theorem length_zip : ∀ (l₁ : list α) (l₂ : list β), diff --git a/src/data/multiset/nodup.lean b/src/data/multiset/nodup.lean index 4c86556e8adf5..1108e40e090bc 100644 --- a/src/data/multiset/nodup.lean +++ b/src/data/multiset/nodup.lean @@ -192,7 +192,7 @@ theorem range_le {m n : ℕ} : range m ≤ range n ↔ m ≤ n := theorem mem_sub_of_nodup [decidable_eq α] {a : α} {s t : multiset α} (d : nodup s) : a ∈ s - t ↔ a ∈ s ∧ a ∉ t := ⟨λ h, ⟨mem_of_le tsub_le_self h, λ h', - by refine count_eq_zero.1 _ h; rw [count_sub a s t, nat.sub_eq_zero_iff_le]; + by refine count_eq_zero.1 _ h; rw [count_sub a s t, tsub_eq_zero_iff_le]; exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')⟩, λ ⟨h₁, h₂⟩, or.resolve_right (mem_add.1 $ mem_of_le le_tsub_add h₁) h₂⟩ diff --git a/src/data/mv_polynomial/basic.lean b/src/data/mv_polynomial/basic.lean index dc65e16757796..adb797a1073c3 100644 --- a/src/data/mv_polynomial/basic.lean +++ b/src/data/mv_polynomial/basic.lean @@ -456,7 +456,8 @@ begin congr' with t, by_cases hj : s = t, { subst t, simp only [tsub_apply, add_apply, single_eq_same], - refine (nat.sub_add_cancel $ nat.pos_of_ne_zero _).symm, rwa finsupp.mem_support_iff at h }, + refine (tsub_add_cancel_of_le (nat.pos_of_ne_zero _).nat_succ_le).symm, + rwa finsupp.mem_support_iff at h }, { simp [single_eq_of_ne hj] } }, { rw ← not_mem_support_iff, intro hm, apply h, have H := support_mul _ _ hm, simp only [finset.mem_bUnion] at H, diff --git a/src/data/mv_polynomial/pderiv.lean b/src/data/mv_polynomial/pderiv.lean index 3abc1097912da..a523bee78aae1 100644 --- a/src/data/mv_polynomial/pderiv.lean +++ b/src/data/mv_polynomial/pderiv.lean @@ -162,7 +162,7 @@ lemma pderiv_pow {i : σ} {f : mv_polynomial σ R} {n : ℕ} : begin induction n with n ih, { simp, }, - { simp only [nat.succ_sub_succ_eq_sub, nat.cast_succ, nat.sub_zero, mv_polynomial.pderiv_mul, + { simp only [nat.succ_sub_succ_eq_sub, nat.cast_succ, tsub_zero, mv_polynomial.pderiv_mul, pow_succ, ih], cases n, { simp, }, diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean index fbaa6f34ab806..d782c895cb710 100644 --- a/src/data/nat/basic.lean +++ b/src/data/nat/basic.lean @@ -216,8 +216,7 @@ iff.intro eq_zero_of_mul_eq_zero (by simp [or_imp_distrib] {contextual := tt}) by rw [eq_comm, nat.mul_eq_zero] lemma eq_zero_of_double_le {a : ℕ} (h : 2 * a ≤ a) : a = 0 := -nat.eq_zero_of_le_zero $ - by rwa [two_mul, nat.add_le_to_le_sub, nat.sub_self] at h; refl +add_right_eq_self.mp $ le_antisymm ((two_mul a).symm.trans_le h) le_add_self lemma eq_zero_of_mul_le {a b : ℕ} (hb : 2 ≤ b) (h : b * a ≤ a) : a = 0 := eq_zero_of_double_le $ le_trans (nat.mul_le_mul_right _ hb) h @@ -279,6 +278,8 @@ eq_one_of_mul_eq_one_right (by rwa mul_comm) /-! ### `succ` -/ +lemma _root_.has_lt.lt.nat_succ_le {n m : ℕ} (h : n < m) : succ n ≤ m := succ_le_of_lt h + lemma succ_eq_one_add (n : ℕ) : n.succ = 1 + n := by rw [nat.succ_eq_add_one, nat.add_comm] @@ -462,7 +463,7 @@ theorem pred_eq_of_eq_succ {m n : ℕ} (H : m = n.succ) : m.pred = n := by simp by cases n; split; rintro ⟨⟩; refl theorem pred_sub (n m : ℕ) : pred n - m = pred (n - m) := -by rw [← nat.sub_one, nat.sub_sub, one_add]; refl +by rw [← nat.sub_one, nat.sub_sub, one_add, sub_succ] lemma le_pred_of_lt {n m : ℕ} (h : m < n) : m ≤ n - 1 := nat.sub_le_sub_right h 1 @@ -534,13 +535,13 @@ theorem le_mul_self : Π (n : ℕ), n ≤ n * n lemma le_mul_of_pos_left {m n : ℕ} (h : 0 < n) : m ≤ n * m := begin conv {to_lhs, rw [← one_mul(m)]}, - exact decidable.mul_le_mul_of_nonneg_right (nat.succ_le_of_lt h) dec_trivial, + exact decidable.mul_le_mul_of_nonneg_right h.nat_succ_le dec_trivial, end lemma le_mul_of_pos_right {m n : ℕ} (h : 0 < n) : m ≤ m * n := begin conv {to_lhs, rw [← mul_one(m)]}, - exact decidable.mul_le_mul_of_nonneg_left (nat.succ_le_of_lt h) dec_trivial, + exact decidable.mul_le_mul_of_nonneg_left h.nat_succ_le dec_trivial, end theorem two_mul_ne_two_mul_add_one {n m} : 2 * n ≠ 2 * m + 1 := @@ -858,7 +859,7 @@ protected theorem div_mod_unique {n k m d : ℕ} (h : 0 < k) : simp [div_eq_of_lt, mod_eq_of_lt, h₂]⟩ lemma two_mul_odd_div_two {n : ℕ} (hn : n % 2 = 1) : 2 * (n / 2) = n - 1 := -by conv {to_rhs, rw [← nat.mod_add_div n 2, hn, nat.add_sub_cancel_left]} +by conv {to_rhs, rw [← nat.mod_add_div n 2, hn, add_tsub_cancel_left]} lemma div_dvd_of_dvd {a b : ℕ} (h : b ∣ a) : (a / b) ∣ a := ⟨b, (nat.div_mul_cancel h).symm⟩ @@ -909,7 +910,7 @@ lemma dvd_sub' {k m n : ℕ} (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n := begin cases le_total n m with H H, { exact dvd_sub H h₁ h₂ }, - { rw nat.sub_eq_zero_of_le H, + { rw tsub_eq_zero_iff_le.mpr H, exact dvd_zero k }, end @@ -945,12 +946,12 @@ lemma succ_div : ∀ (a b : ℕ), (a + 1) / b = from ⟨succ_pos _, (add_le_add_iff_right _).2 hb_le_a⟩, have dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1, { rw [nat.dvd_add_iff_left (dvd_refl (b + 1)), - ← add_tsub_add_right_eq_tsub a 1 b, add_comm (_ - _), add_assoc, - nat.sub_add_cancel (succ_le_succ hb_le_a), add_comm 1] }, + ← add_tsub_add_eq_tsub_right a 1 b, add_comm (_ - _), add_assoc, + tsub_add_cancel_of_le (succ_le_succ hb_le_a), add_comm 1] }, have wf : a - b < a + 1, from lt_succ_of_le tsub_le_self, - rw [if_pos h₁, if_pos h₂, add_tsub_add_right_eq_tsub, nat.sub_add_comm hb_le_a, + rw [if_pos h₁, if_pos h₂, add_tsub_add_eq_tsub_right, ← tsub_add_eq_add_tsub hb_le_a, by exact have _ := wf, succ_div (a - b), - add_tsub_add_right_eq_tsub], + add_tsub_add_eq_tsub_right], simp [dvd_iff, succ_eq_add_one, add_comm 1, add_assoc] }, { have hba : ¬ b ≤ a, from not_le_of_gt (lt_trans (lt_succ_self a) (lt_of_not_ge hb_le_a1)), @@ -980,8 +981,8 @@ end /-- If `a` and `b` are equal mod `c`, `a - b` is zero mod `c`. -/ lemma sub_mod_eq_zero_of_mod_eq {a b c : ℕ} (h : a % c = b % c) : (a - b) % c = 0 := -by rw [←nat.mod_add_div a c, ←nat.mod_add_div b c, ←h, ←nat.sub_sub, nat.add_sub_cancel_left, - ←nat.mul_sub_left_distrib, nat.mul_mod_right] +by rw [←nat.mod_add_div a c, ←nat.mod_add_div b c, ←h, tsub_add_eq_tsub_tsub, add_tsub_cancel_left, + ←mul_tsub, nat.mul_mod_right] @[simp] lemma one_mod (n : ℕ) : 1 % (n + 2) = 1 := nat.mod_eq_of_lt (add_lt_add_right n.succ_pos 1) @@ -1122,7 +1123,7 @@ begin by_cases n0 : n = 0, { rw [n0, nat.div_zero, nat.div_zero] }, { rw [← mod_add_div m n] { occs := occurrences.pos [2] }, - rw [nat.add_sub_cancel_left, mul_div_right _ (nat.pos_of_ne_zero n0)] } + rw [add_tsub_cancel_left, mul_div_right _ (nat.pos_of_ne_zero n0)] } end lemma mul_div_le (m n : ℕ) : n * (m / n) ≤ m := @@ -1421,9 +1422,8 @@ decidable_of_iff (∀ k (h : k < succ n), P k (le_of_lt_succ h)) instance decidable_lo_hi (lo hi : ℕ) (P : ℕ → Prop) [H : decidable_pred P] : decidable (∀x, lo ≤ x → x < hi → P x) := decidable_of_iff (∀ x < hi - lo, P (lo + x)) -⟨λal x hl hh, by have := al (x - lo) (lt_of_not_ge $ - (not_congr (nat.sub_le_sub_right_iff _ _ _ hl)).2 $ not_le_of_gt hh); - rwa [nat.add_sub_of_le hl] at this, +⟨λal x hl hh, by { have := al (x - lo) ((tsub_lt_tsub_iff_right hl).mpr hh), + rwa [add_tsub_cancel_of_le hl] at this, }, λal x h, al _ (nat.le_add_right _ _) (lt_tsub_iff_left.mp h)⟩ instance decidable_lo_hi_le (lo hi : ℕ) (P : ℕ → Prop) [H : decidable_pred P] : diff --git a/src/data/nat/bitwise.lean b/src/data/nat/bitwise.lean index e16ac1883cf38..71488ae19e2d0 100644 --- a/src/data/nat/bitwise.lean +++ b/src/data/nat/bitwise.lean @@ -116,8 +116,8 @@ begin cases hm.lt_or_lt with hm hm, { rw [nat.div_eq_zero, bodd_zero], exact nat.pow_lt_pow_of_lt_right one_lt_two hm }, - { rw [pow_div hm.le zero_lt_two, ←nat.sub_add_cancel (nat.sub_pos_of_lt hm), pow_succ], - simp } + { rw [pow_div hm.le zero_lt_two, ← tsub_add_cancel_of_le (succ_le_of_lt $ tsub_pos_of_lt hm)], + simp [pow_succ] } end lemma test_bit_two_pow (n m : ℕ) : test_bit (2 ^ n) m = (n = m) := diff --git a/src/data/nat/cast.lean b/src/data/nat/cast.lean index 65d9a50f747a6..08921a39a59f1 100644 --- a/src/data/nat/cast.lean +++ b/src/data/nat/cast.lean @@ -124,7 +124,7 @@ lemma cast_two {α : Type*} [add_monoid α] [has_one α] : ((2 : ℕ) : α) = 2 @[simp, norm_cast] theorem cast_sub [add_group α] [has_one α] {m n} (h : m ≤ n) : ((n - m : ℕ) : α) = n - m := -eq_sub_of_add_eq $ by rw [← cast_add, nat.sub_add_cancel h] +eq_sub_of_add_eq $ by rw [← cast_add, tsub_add_cancel_of_le h] @[simp, norm_cast] theorem cast_mul [non_assoc_semiring α] (m) : ∀ n, ((m * n : ℕ) : α) = m * n | 0 := (mul_zero _).symm diff --git a/src/data/nat/choose/basic.lean b/src/data/nat/choose/basic.lean index 5e1601b3d1c43..b223f1400df93 100644 --- a/src/data/nat/choose/basic.lean +++ b/src/data/nat/choose/basic.lean @@ -61,7 +61,7 @@ by induction n; simp [*, choose, add_comm] /- The `n+1`-st triangle number is `n` more than the `n`-th triangle number -/ lemma triangle_succ (n : ℕ) : (n + 1) * ((n + 1) - 1) / 2 = n * (n - 1) / 2 + n := begin - rw [← add_mul_div_left, mul_comm 2 n, ← mul_add, nat.add_sub_cancel, mul_comm], + rw [← add_mul_div_left, mul_comm 2 n, ← mul_add, add_tsub_cancel_right, mul_comm], cases n; refl, apply zero_lt_succ end @@ -103,9 +103,9 @@ begin simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc], have h₃ : k * n! ≤ n * n! := nat.mul_le_mul_right _ (le_of_succ_le_succ hk), rw [choose_succ_succ, add_mul, add_mul, succ_sub_succ, h, h₁, h₂, add_mul, - nat.mul_sub_right_distrib, factorial_succ, ← nat.add_sub_assoc h₃, add_assoc, ← add_mul, - nat.add_sub_cancel_left, add_comm] }, - { simp [hk₁, mul_comm, choose, nat.sub_self] } + tsub_mul, factorial_succ, ← add_tsub_assoc_of_le h₃, add_assoc, ← add_mul, + add_tsub_cancel_left, add_comm] }, + { simp [hk₁, mul_comm, choose, tsub_self] } end lemma choose_mul {n k s : ℕ} (hkn : k ≤ n) (hsk : s ≤ k) : @@ -122,7 +122,7 @@ begin ... = n! : by rw [choose_mul_factorial_mul_factorial hsk, choose_mul_factorial_mul_factorial hkn] ... = n.choose s * s! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) - : by rw [choose_mul_factorial_mul_factorial (nat.sub_le_sub_right hkn _), + : by rw [choose_mul_factorial_mul_factorial (tsub_le_tsub_right hkn _), choose_mul_factorial_mul_factorial (hsk.trans hkn)] ... = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s!) : by rw [tsub_tsub_tsub_cancel_right hsk, mul_assoc, mul_left_comm s!, mul_assoc, @@ -137,11 +137,11 @@ begin end lemma add_choose (i j : ℕ) : (i + j).choose j = (i + j)! / (i! * j!) := -by rw [choose_eq_factorial_div_factorial (nat.le_add_left j i), nat.add_sub_cancel, mul_comm] +by rw [choose_eq_factorial_div_factorial (nat.le_add_left j i), add_tsub_cancel_right, mul_comm] lemma add_choose_mul_factorial_mul_factorial (i j : ℕ) : (i + j).choose j * i! * j! = (i + j)! := by rw [← choose_mul_factorial_mul_factorial (nat.le_add_left _ _), - nat.add_sub_cancel, mul_right_comm] + add_tsub_cancel_right, mul_right_comm] theorem factorial_mul_factorial_dvd_factorial {n k : ℕ} (hk : k ≤ n) : k! * (n - k)! ∣ n! := by rw [←choose_mul_factorial_mul_factorial hk, mul_assoc]; exact dvd_mul_left _ _ @@ -150,15 +150,15 @@ lemma factorial_mul_factorial_dvd_factorial_add (i j : ℕ) : i! * j! ∣ (i + j)! := begin convert factorial_mul_factorial_dvd_factorial (le.intro rfl), - rw nat.add_sub_cancel_left + rw add_tsub_cancel_left end @[simp] lemma choose_symm {n k : ℕ} (hk : k ≤ n) : choose n (n-k) = choose n k := by rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (nat.sub_le _ _), - nat.sub_sub_self hk, mul_comm] + tsub_tsub_cancel_of_le hk, mul_comm] lemma choose_symm_of_eq_add {n a b : ℕ} (h : n = a + b) : nat.choose n a = nat.choose n b := -by { convert nat.choose_symm (nat.le_add_left _ _), rw nat.add_sub_cancel} +by { convert nat.choose_symm (nat.le_add_left _ _), rw add_tsub_cancel_right} lemma choose_symm_add {a b : ℕ} : choose (a+b) a = choose (a+b) b := choose_symm_of_eq_add rfl @@ -171,7 +171,7 @@ lemma choose_succ_right_eq (n k : ℕ) : choose n (k + 1) * (k + 1) = choose n k begin have e : (n+1) * choose n k = choose n k * (k+1) + choose n (k+1) * (k+1), rw [← right_distrib, ← choose_succ_succ, succ_mul_choose_eq], - rw [← tsub_eq_of_eq_add_rev e, mul_comm, ← nat.mul_sub_left_distrib, add_tsub_add_right_eq_tsub] + rw [← tsub_eq_of_eq_add_rev e, mul_comm, ← mul_tsub, add_tsub_add_eq_tsub_right] end @[simp] lemma choose_succ_self_right : ∀ (n:ℕ), (n+1).choose n = n+1 @@ -184,7 +184,7 @@ begin induction k with k ih, { simp }, obtain hk | hk := le_or_lt (k + 1) (n + 1), { rw [choose_succ_succ, add_mul, succ_sub_succ, ←choose_succ_right_eq, ←succ_sub_succ, - nat.mul_sub_left_distrib, add_tsub_cancel_of_le (nat.mul_le_mul_left _ hk)] }, + mul_tsub, add_tsub_cancel_of_le (nat.mul_le_mul_left _ hk)] }, rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul, zero_mul], end @@ -193,7 +193,7 @@ lemma asc_factorial_eq_factorial_mul_choose (n k : ℕ) : begin rw mul_comm, apply mul_right_cancel₀ (factorial_ne_zero (n + k - k)), - rw [choose_mul_factorial_mul_factorial, nat.add_sub_cancel, ←factorial_mul_asc_factorial, + rw [choose_mul_factorial_mul_factorial, add_tsub_cancel_right, ←factorial_mul_asc_factorial, mul_comm], exact nat.le_add_left k n, end @@ -260,8 +260,8 @@ begin { rw ← choose_symm b, apply choose_le_middle_of_le_half_left, rw [div_lt_iff_lt_mul' zero_lt_two] at h, - rw [le_div_iff_mul_le' zero_lt_two, nat.mul_sub_right_distrib, tsub_le_iff_tsub_le, - mul_two, nat.add_sub_cancel], + rw [le_div_iff_mul_le' zero_lt_two, tsub_mul, tsub_le_iff_tsub_le, + mul_two, add_tsub_cancel_right], exact le_of_lt h } }, { rw choose_eq_zero_of_lt b, apply zero_le } diff --git a/src/data/nat/choose/cast.lean b/src/data/nat/choose/cast.lean index e6bf1db9655c6..935edef67ccf4 100644 --- a/src/data/nat/choose/cast.lean +++ b/src/data/nat/choose/cast.lean @@ -29,7 +29,7 @@ end lemma cast_add_choose {a b : ℕ} : ((a + b).choose a : K) = (a + b)! / (a! * b!) := -by rw [cast_choose K (le_add_right le_rfl), nat.add_sub_cancel_left] +by rw [cast_choose K (le_add_right le_rfl), add_tsub_cancel_left] lemma cast_choose_eq_pochhammer_div (a b : ℕ) : (a.choose b : K) = (pochhammer K b).eval (a - (b - 1) : ℕ) / b! := diff --git a/src/data/nat/choose/dvd.lean b/src/data/nat/choose/dvd.lean index 78200b71d7dff..61dc0c6023377 100644 --- a/src/data/nat/choose/dvd.lean +++ b/src/data/nat/choose/dvd.lean @@ -23,14 +23,14 @@ have h₂ : ¬p ∣ a!, from mt hp.dvd_factorial.1 (not_le_of_gt hap), have h₃ : ¬p ∣ b!, from mt hp.dvd_factorial.1 (not_le_of_gt hbp), by rw [← choose_mul_factorial_mul_factorial (le.intro rfl), mul_assoc, hp.dvd_mul, hp.dvd_mul, - nat.add_sub_cancel_left a b] at h₁; + add_tsub_cancel_left a b] at h₁; exact h₁.resolve_right (not_or_distrib.2 ⟨h₂, h₃⟩) lemma dvd_choose_self {p k : ℕ} (hk : 0 < k) (hkp : k < p) (hp : prime p) : p ∣ choose p k := begin have r : k + (p - k) = p, - by rw [← nat.add_sub_assoc (nat.le_of_lt hkp) k, nat.add_sub_cancel_left], + by rw [← add_tsub_assoc_of_le (nat.le_of_lt hkp) k, add_tsub_cancel_left], have e : p ∣ choose (k + (p - k)) k, by exact dvd_choose_add hkp (nat.sub_lt (hk.trans hkp) hk) (by rw r) hp, rwa r at e, diff --git a/src/data/nat/choose/sum.lean b/src/data/nat/choose/sum.lean index bed4e514dd40f..aa8d25b8f6352 100644 --- a/src/data/nat/choose/sum.lean +++ b/src/data/nat/choose/sum.lean @@ -103,9 +103,9 @@ calc 2 * (∑ i in range (m + 1), choose (2 * m + 1) i) = rw [range_eq_Ico, sum_Ico_reflect], { congr, have A : m + 1 ≤ 2 * m + 1, by linarith, - rw [add_comm, nat.add_sub_assoc A, ← add_comm], + rw [add_comm, add_tsub_assoc_of_le A, ← add_comm], congr, - rw nat.sub_eq_iff_eq_add A, + rw tsub_eq_iff_eq_add_of_le A, ring, }, { linarith } end diff --git a/src/data/nat/dist.lean b/src/data/nat/dist.lean index d07f482905a33..c6eacfc725510 100644 --- a/src/data/nat/dist.lean +++ b/src/data/nat/dist.lean @@ -22,20 +22,20 @@ theorem dist_comm (n m : ℕ) : dist n m = dist m n := by simp [dist.def, add_comm] @[simp] theorem dist_self (n : ℕ) : dist n n = 0 := -by simp [dist.def, nat.sub_self] +by simp [dist.def, tsub_self] theorem eq_of_dist_eq_zero {n m : ℕ} (h : dist n m = 0) : n = m := have n - m = 0, from nat.eq_zero_of_add_eq_zero_right h, -have n ≤ m, from nat.le_of_sub_eq_zero this, +have n ≤ m, from tsub_eq_zero_iff_le.mp this, have m - n = 0, from nat.eq_zero_of_add_eq_zero_left h, -have m ≤ n, from nat.le_of_sub_eq_zero this, +have m ≤ n, from tsub_eq_zero_iff_le.mp this, le_antisymm ‹n ≤ m› ‹m ≤ n› theorem dist_eq_zero {n m : ℕ} (h : n = m) : dist n m = 0 := begin rw [h, dist_self] end theorem dist_eq_sub_of_le {n m : ℕ} (h : n ≤ m) : dist n m = m - n := -begin rw [dist.def, nat.sub_eq_zero_of_le h, zero_add] end +begin rw [dist.def, tsub_eq_zero_iff_le.mpr h, zero_add] end theorem dist_eq_sub_of_le_right {n m : ℕ} (h : m ≤ n) : dist n m = n - m := begin rw [dist_comm], apply dist_eq_sub_of_le h end @@ -53,16 +53,16 @@ theorem dist_tri_right' (n m : ℕ) : n ≤ m + dist n m := by rw dist_comm; apply dist_tri_right theorem dist_zero_right (n : ℕ) : dist n 0 = n := -eq.trans (dist_eq_sub_of_le_right (zero_le n)) (nat.sub_zero n) +eq.trans (dist_eq_sub_of_le_right (zero_le n)) (tsub_zero n) theorem dist_zero_left (n : ℕ) : dist 0 n = n := -eq.trans (dist_eq_sub_of_le (zero_le n)) (nat.sub_zero n) +eq.trans (dist_eq_sub_of_le (zero_le n)) (tsub_zero n) theorem dist_add_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m := calc dist (n + k) (m + k) = ((n + k) - (m + k)) + ((m + k)-(n + k)) : rfl - ... = (n - m) + ((m + k) - (n + k)) : by rw add_tsub_add_right_eq_tsub - ... = (n - m) + (m - n) : by rw add_tsub_add_right_eq_tsub + ... = (n - m) + ((m + k) - (n + k)) : by rw add_tsub_add_eq_tsub_right + ... = (n - m) + (m - n) : by rw add_tsub_add_eq_tsub_right theorem dist_add_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m := begin rw [add_comm k n, add_comm k m], apply dist_add_add_right end @@ -79,7 +79,7 @@ have dist n m + dist m k = (n - m) + (m - k) + ((k - m) + (m - n)), by { rw [this, dist.def], exact add_le_add tsub_le_tsub_add_tsub tsub_le_tsub_add_tsub } theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k := -by rw [dist.def, dist.def, right_distrib, nat.mul_sub_right_distrib, nat.mul_sub_right_distrib] +by rw [dist.def, dist.def, right_distrib, tsub_mul, tsub_mul] theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m := by rw [mul_comm k n, mul_comm k m, dist_mul_right, mul_comm] @@ -101,9 +101,9 @@ by simp [dist.def, succ_sub_succ] theorem dist_pos_of_ne {i j : nat} : i ≠ j → 0 < dist i j := assume hne, nat.lt_by_cases (assume : i < j, - begin rw [dist_eq_sub_of_le (le_of_lt this)], apply nat.sub_pos_of_lt this end) + begin rw [dist_eq_sub_of_le (le_of_lt this)], apply tsub_pos_of_lt this end) (assume : i = j, by contradiction) (assume : i > j, - begin rw [dist_eq_sub_of_le_right (le_of_lt this)], apply nat.sub_pos_of_lt this end) + begin rw [dist_eq_sub_of_le_right (le_of_lt this)], apply tsub_pos_of_lt this end) end nat diff --git a/src/data/nat/enat.lean b/src/data/nat/enat.lean index 7f53e7b035da8..210a865ca809b 100644 --- a/src/data/nat/enat.lean +++ b/src/data/nat/enat.lean @@ -306,7 +306,7 @@ instance : canonically_ordered_add_monoid enat := (iff_of_false (not_le_of_gt (coe_lt_top _)) (not_exists.2 (λ x, ne_of_lt (by rw [top_add]; exact coe_lt_top _)))) (λ a, ⟨λ h, ⟨(b - a : ℕ), - by rw [← nat.cast_add, coe_inj, add_comm, nat.sub_add_cancel (coe_le_coe.1 h)]⟩, + by rw [← nat.cast_add, coe_inj, add_comm, tsub_add_cancel_of_le (coe_le_coe.1 h)]⟩, (λ ⟨c, hc⟩, enat.cases_on c (λ hc, hc.symm ▸ show (a : enat) ≤ a + ⊤, by rw [add_top]; exact le_top) (λ c (hc : (b : enat) = a + c), diff --git a/src/data/nat/factorial/basic.lean b/src/data/nat/factorial/basic.lean index ccc70b877591c..d971f5283a521 100644 --- a/src/data/nat/factorial/basic.lean +++ b/src/data/nat/factorial/basic.lean @@ -42,7 +42,7 @@ variables {m n : ℕ} @[simp] theorem factorial_two : 2! = 2 := rfl theorem mul_factorial_pred (hn : 0 < n) : n * (n - 1)! = n! := -nat.sub_add_cancel hn ▸ rfl +tsub_add_cancel_of_le (nat.succ_le_of_lt hn) ▸ rfl theorem factorial_pos : ∀ n, 0 < n! | 0 := zero_lt_one @@ -169,7 +169,7 @@ begin apply pow_le_pow_of_le_left (zero_le n) (le_succ n), exact factorial_pos n,}, convert nat.factorial_mul_pow_le_factorial, - exact (nat.add_sub_of_le hnm).symm, + exact (add_tsub_cancel_of_le hnm).symm, end @@ -282,11 +282,11 @@ def desc_factorial (n : ℕ) : ℕ → ℕ lemma zero_desc_factorial_succ (k : ℕ) : (0 : ℕ).desc_factorial k.succ = 0 := -by rw [desc_factorial_succ, nat.zero_sub, zero_mul] +by rw [desc_factorial_succ, zero_tsub, zero_mul] @[simp] lemma desc_factorial_one (n : ℕ) : n.desc_factorial 1 = n := -by rw [desc_factorial_succ, desc_factorial_zero, mul_one, nat.sub_zero] +by rw [desc_factorial_succ, desc_factorial_zero, mul_one, tsub_zero] @[simp] lemma succ_desc_factorial_succ (n : ℕ) : ∀ k : ℕ, (n + 1).desc_factorial (k + 1) = (n + 1) * n.desc_factorial k @@ -296,7 +296,7 @@ by rw [desc_factorial_succ, desc_factorial_zero, mul_one, nat.sub_zero] lemma succ_desc_factorial (n : ℕ) : ∀ k, (n + 1 - k) * (n + 1).desc_factorial k = (n + 1) * n.desc_factorial k -| 0 := by rw [nat.sub_zero, desc_factorial_zero, desc_factorial_zero] +| 0 := by rw [tsub_zero, desc_factorial_zero, desc_factorial_zero] | (k + 1) := by rw [desc_factorial, succ_desc_factorial, desc_factorial_succ, succ_sub_succ, mul_left_comm] @@ -308,7 +308,7 @@ lemma desc_factorial_self : ∀ n : ℕ, n.desc_factorial n = n! | 0 := by simp only [desc_factorial_zero, nat.one_ne_zero, nat.not_lt_zero] | (succ k) := begin rw [desc_factorial_succ, mul_eq_zero, desc_factorial_eq_zero_iff_lt, lt_succ_iff, - nat.sub_eq_zero_iff_le, lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp], + tsub_eq_zero_iff_le, lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp], exact λ h _, h, end @@ -323,7 +323,7 @@ lemma add_desc_factorial_eq_asc_factorial (n : ℕ) : /-- `n.desc_factorial k = n! / (n - k)!` but without ℕ-division. See `nat.desc_factorial_eq_div` for the version using ℕ-division. -/ theorem factorial_mul_desc_factorial : ∀ {n k : ℕ}, k ≤ n → (n - k)! * n.desc_factorial k = n! -| n 0 := λ _, by rw [desc_factorial_zero, mul_one, nat.sub_zero] +| n 0 := λ _, by rw [desc_factorial_zero, mul_one, tsub_zero] | 0 (succ k) := λ h, by { exfalso, exact not_succ_le_zero k h } | (succ n) (succ k) := λ h, by rw [succ_desc_factorial_succ, succ_sub_succ, ←mul_assoc, mul_comm (n - k)!, mul_assoc, factorial_mul_desc_factorial (nat.succ_le_succ_iff.1 h), @@ -342,7 +342,7 @@ lemma pow_sub_le_desc_factorial (n : ℕ) : ∀ (k : ℕ), (n + 1 - k)^k ≤ n.d | (k + 1) := begin rw [desc_factorial_succ, pow_succ, succ_sub_succ], exact nat.mul_le_mul_of_nonneg_left (le_trans (nat.pow_le_pow_of_le_left - (nat.sub_le_sub_right (le_succ _) _) k) (pow_sub_le_desc_factorial k)), + (tsub_le_tsub_right (le_succ _) _) k) (pow_sub_le_desc_factorial k)), end lemma pow_sub_lt_desc_factorial' {n : ℕ} : @@ -350,12 +350,12 @@ lemma pow_sub_lt_desc_factorial' {n : ℕ} : | 0 := λ h, begin rw [desc_factorial_succ, pow_succ, pow_one, desc_factorial_one], exact nat.mul_lt_mul_of_pos_left (tsub_lt_self (lt_of_lt_of_le zero_lt_two h) zero_lt_one) - (nat.sub_pos_of_lt h), + (tsub_pos_of_lt h), end | (k + 1) := λ h, begin rw [desc_factorial_succ, pow_succ], - refine nat.mul_lt_mul_of_pos_left ((nat.pow_le_pow_of_le_left (nat.sub_le_sub_right - (le_succ n) _) _).trans_lt _) (nat.sub_pos_of_lt h), + refine nat.mul_lt_mul_of_pos_left ((nat.pow_le_pow_of_le_left (tsub_le_tsub_right + (le_succ n) _) _).trans_lt _) (tsub_pos_of_lt h), rw succ_sub_succ, exact (pow_sub_lt_desc_factorial' ((le_succ _).trans h)), end diff --git a/src/data/nat/factorial/cast.lean b/src/data/nat/factorial/cast.lean index 0340d3652207f..27a4a241076ad 100644 --- a/src/data/nat/factorial/cast.lean +++ b/src/data/nat/factorial/cast.lean @@ -39,8 +39,8 @@ begin simp_rw [add_succ, succ_sub_one], obtain h | h := le_total a b, { rw [desc_factorial_of_lt (lt_succ_of_le h), desc_factorial_of_lt (lt_succ_of_le _)], - rw [nat.sub_eq_zero_of_le h, zero_add] }, - { rw nat.sub_add_cancel h } + rw [tsub_eq_zero_iff_le.mpr h, zero_add] }, + { rw tsub_add_cancel_of_le h } end lemma cast_factorial : @@ -59,8 +59,8 @@ lemma cast_desc_factorial_two : begin rw cast_desc_factorial, cases a, - { rw [nat.zero_sub, cast_zero, pochhammer_ne_zero_eval_zero _ (two_ne_zero), zero_mul] }, - { rw [succ_sub_succ, nat.sub_zero, cast_succ, add_sub_cancel, pochhammer_succ_right, + { rw [zero_tsub, cast_zero, pochhammer_ne_zero_eval_zero _ (two_ne_zero), zero_mul] }, + { rw [succ_sub_succ, tsub_zero, cast_succ, add_sub_cancel, pochhammer_succ_right, pochhammer_one, polynomial.X_mul, polynomial.eval_mul_X, polynomial.eval_add, polynomial.eval_X, cast_one, polynomial.eval_one] } end diff --git a/src/data/nat/interval.lean b/src/data/nat/interval.lean index 106575adb95e3..f710f95ba9b06 100644 --- a/src/data/nat/interval.lean +++ b/src/data/nat/interval.lean @@ -28,14 +28,14 @@ instance : locally_finite_order ℕ := rw [list.mem_to_finset, list.mem_range'], cases le_or_lt a b, { rw [add_tsub_cancel_of_le (nat.lt_succ_of_le h).le, nat.lt_succ_iff] }, - { rw [nat.sub_eq_zero_iff_le.2 h, add_zero], + { rw [tsub_eq_zero_iff_le.2 (succ_le_of_lt h), add_zero], exact iff_of_false (λ hx, hx.2.not_le hx.1) (λ hx, h.not_le (hx.1.trans hx.2)) } end, finset_mem_Ico := λ a b x, begin rw [list.mem_to_finset, list.mem_range'], cases le_or_lt a b, { rw [add_tsub_cancel_of_le h] }, - { rw [nat.sub_eq_zero_iff_le.2 h.le, add_zero], + { rw [tsub_eq_zero_iff_le.2 h.le, add_zero], exact iff_of_false (λ hx, hx.2.not_le hx.1) (λ hx, h.not_le (hx.1.trans hx.2.le)) } end, finset_mem_Ioc := λ a b x, begin @@ -43,14 +43,14 @@ instance : locally_finite_order ℕ := cases le_or_lt a b, { rw [←succ_sub_succ, add_tsub_cancel_of_le (succ_le_succ h), nat.lt_succ_iff, nat.succ_le_iff] }, - { rw [nat.sub_eq_zero_iff_le.2 h.le, add_zero], + { rw [tsub_eq_zero_iff_le.2 h.le, add_zero], exact iff_of_false (λ hx, hx.2.not_le hx.1) (λ hx, h.not_le (hx.1.le.trans hx.2)) } end, finset_mem_Ioo := λ a b x, begin - rw [list.mem_to_finset, list.mem_range', nat.sub_sub], + rw [list.mem_to_finset, list.mem_range', ← tsub_add_eq_tsub_tsub], cases le_or_lt (a + 1) b, { rw [add_tsub_cancel_of_le h, nat.succ_le_iff] }, - { rw [nat.sub_eq_zero_iff_le.2 h.le, add_zero], + { rw [tsub_eq_zero_iff_le.2 h.le, add_zero], exact iff_of_false (λ hx, hx.2.not_le hx.1) (λ hx, h.not_le (hx.1.trans hx.2)) } end } @@ -151,14 +151,14 @@ begin refine ⟨_, ((tsub_le_tsub_iff_left hac).2 hx.1).trans_lt ((tsub_lt_tsub_iff_right hac).2 (nat.lt_succ_self _))⟩, cases lt_or_le c b, - { rw nat.sub_eq_zero_of_le h, + { rw tsub_eq_zero_iff_le.mpr (succ_le_of_lt h), exact zero_le _ }, { rw ←succ_sub_succ c, exact (tsub_le_tsub_iff_left (succ_le_succ $ hx.2.le.trans h)).2 hx.2 } }, { rintro ⟨hb, ha⟩, rw [lt_tsub_iff_left, lt_succ_iff] at ha, have hx : x ≤ c := (nat.le_add_left _ _).trans ha, - refine ⟨c - x, _, nat.sub_sub_self hx⟩, + refine ⟨c - x, _, tsub_tsub_cancel_of_le hx⟩, { rw mem_Ico, exact ⟨le_tsub_of_add_le_right ha, (tsub_lt_iff_left hx).2 $ succ_le_iff.1 $ tsub_le_iff_right.1 hb⟩ } } @@ -170,7 +170,7 @@ begin cases n, { rw [range_zero, image_empty] }, { rw [finset.range_eq_Ico, Ico_image_const_sub_eq_Ico (zero_le _)], - simp_rw [succ_sub_succ, nat.sub_zero, nat.sub_self] } + simp_rw [succ_sub_succ, tsub_zero, tsub_self] } end end nat diff --git a/src/data/nat/log.lean b/src/data/nat/log.lean index 973cb3b33d122..57c08fad1e758 100644 --- a/src/data/nat/log.lean +++ b/src/data/nat/log.lean @@ -223,8 +223,8 @@ begin have b_pos : 0 < b := zero_lt_two.trans_le hb, rw clog, split_ifs, { rw [succ_eq_add_one, add_le_add_iff_right, ←ih ((x + b - 1)/b) (add_pred_div_lt hb h.2), - nat.div_le_iff_le_mul_add_pred b_pos, ←pow_succ, nat.add_sub_assoc b_pos, - add_le_add_iff_right] }, + nat.div_le_iff_le_mul_add_pred b_pos, + ← pow_succ, add_tsub_assoc_of_le (nat.succ_le_of_lt b_pos), add_le_add_iff_right] }, { exact iff_of_true ((not_lt.1 (not_and.1 h hb)).trans $ succ_le_of_lt $ pow_pos b_pos _) (zero_le _) } end diff --git a/src/data/nat/modeq.lean b/src/data/nat/modeq.lean index 29fa02a1e8191..f5564bfc25c27 100644 --- a/src/data/nat/modeq.lean +++ b/src/data/nat/modeq.lean @@ -318,8 +318,9 @@ have hm0 : 0 < m := nat.pos_of_ne_zero (λ h, by simp * at *), have hn0 : 0 < n := nat.pos_of_ne_zero (λ h, by simp * at *), (nat.mul_right_inj (show 0 < 2, from dec_trivial)).1 $ by rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1, - two_mul_odd_div_two (nat.odd_mul_odd hm1 hn1), nat.mul_sub_left_distrib, mul_one, - ← nat.add_sub_assoc hm0, nat.sub_add_cancel (le_mul_of_one_le_right (nat.zero_le _) hn0)] + two_mul_odd_div_two (nat.odd_mul_odd hm1 hn1), mul_tsub, mul_one, + ← add_tsub_assoc_of_le (succ_le_of_lt hm0), + tsub_add_cancel_of_le (le_mul_of_one_le_right (nat.zero_le _) hn0)] lemma odd_of_mod_four_eq_one {n : ℕ} : n % 4 = 1 → n % 2 = 1 := by simpa [modeq, show 2 * 2 = 4, by norm_num] using @modeq.of_modeq_mul_left 2 n 1 2 diff --git a/src/data/nat/pairing.lean b/src/data/nat/pairing.lean index 71ecc35d681db..f9ffbe624e911 100644 --- a/src/data/nat/pairing.lean +++ b/src/data/nat/pairing.lean @@ -56,7 +56,7 @@ begin { show unpair (b * b + a) = (a, b), have be : sqrt (b * b + a) = b, from sqrt_add_eq _ (le_trans (le_of_lt h) (nat.le_add_left _ _)), - simp [unpair, be, nat.add_sub_cancel, h] }, + simp [unpair, be, add_tsub_cancel_right, h] }, { show unpair (a * a + a + b) = (a, b), have ae : sqrt (a * a + (a + b)) = a, { rw sqrt_add_eq, exact add_le_add_left (le_of_not_gt h) _ }, diff --git a/src/data/nat/parity.lean b/src/data/nat/parity.lean index 3dd6e757b90c9..ada084b20aea1 100644 --- a/src/data/nat/parity.lean +++ b/src/data/nat/parity.lean @@ -118,14 +118,14 @@ lemma two_not_dvd_two_mul_sub_one : Π {n} (w : 0 < n), ¬(2 ∣ 2 * n - 1) @[parity_simps] theorem even_sub (h : n ≤ m) : even (m - n) ↔ (even m ↔ even n) := begin - conv { to_rhs, rw [←nat.sub_add_cancel h, even_add] }, + conv { to_rhs, rw [←tsub_add_cancel_of_le h, even_add] }, by_cases h : even n; simp [h] end theorem even.sub_even (hm : even m) (hn : even n) : even (m - n) := (le_total n m).elim (λ h, by simp only [even_sub h, *]) - (λ h, by simp only [nat.sub_eq_zero_of_le h, even_zero]) + (λ h, by simp only [tsub_eq_zero_iff_le.mpr h, even_zero]) theorem even_sub' (h : n ≤ m) : even (m - n) ↔ (odd m ↔ odd n) := by rw [even_sub h, even_iff_not_odd, even_iff_not_odd, not_iff_not] @@ -133,7 +133,7 @@ by rw [even_sub h, even_iff_not_odd, even_iff_not_odd, not_iff_not] theorem odd.sub_odd (hm : odd m) (hn : odd n) : even (m - n) := (le_total n m).elim (λ h, by simp only [even_sub' h, *]) - (λ h, by simp only [nat.sub_eq_zero_of_le h, even_zero]) + (λ h, by simp only [tsub_eq_zero_iff_le.mpr h, even_zero]) @[parity_simps] theorem even_succ : even (succ n) ↔ ¬ even n := by rw [succ_eq_add_one, even_add]; simp [not_even_one] diff --git a/src/data/nat/pow.lean b/src/data/nat/pow.lean index 76a3f14b6f619..3370f2761690a 100644 --- a/src/data/nat/pow.lean +++ b/src/data/nat/pow.lean @@ -3,7 +3,6 @@ Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights r Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro -/ -import data.nat.basic import algebra.group_power.order /-! # `nat.pow` @@ -132,8 +131,7 @@ begin -- step: p ≥ b^succ w { -- Generate condition for induction hypothesis have h₂ : p - b^succ w < p, - { apply nat.sub_lt_of_pos_le _ _ (pow_pos b_pos _) h₁ }, - + { exact tsub_lt_self ((pow_pos b_pos _).trans_le h₁) (pow_pos b_pos _) }, -- Apply induction rw [mod_eq_sub_mod h₁, IH _ h₂], -- Normalize goal and h1 @@ -157,7 +155,7 @@ begin { simp only [one_pow], }, { have le := (pow_le_iff_le_right (nat.le_add_left _ _)).mp a, use (x+2)^(l-k), - rw [←pow_add, add_comm k, nat.sub_add_cancel le], } } + rw [←pow_add, add_comm k, tsub_add_cancel_of_le le], } } end /-- If `1 < x`, then `x^k` divides `x^l` if and only if `k` is at most `l`. -/ diff --git a/src/data/nat/prime.lean b/src/data/nat/prime.lean index cc4c328d80b08..b716196530076 100644 --- a/src/data/nat/prime.lean +++ b/src/data/nat/prime.lean @@ -420,7 +420,7 @@ lemma prod_factors : ∀ {n}, 0 < n → list.prod (factors n) = n lemma factors_prime {p : ℕ} (hp : nat.prime p) : p.factors = [p] := begin - have : p = (p - 2) + 2 := (nat.sub_eq_iff_eq_add hp.1).mp rfl, + have : p = (p - 2) + 2 := (tsub_eq_iff_eq_add_of_le hp.1).mp rfl, rw [this, nat.factors], simp only [eq.symm this], have : nat.min_fac p = p := (nat.prime_def_min_fac.mp hp).2, diff --git a/src/data/nat/psub.lean b/src/data/nat/psub.lean index 7aff367b0e79d..f9b9d539694dc 100644 --- a/src/data/nat/psub.lean +++ b/src/data/nat/psub.lean @@ -69,7 +69,7 @@ theorem ppred_eq_pred {n} (h : 0 < n) : ppred n = some (pred n) := ppred_eq_some.2 $ succ_pred_eq_of_pos h theorem psub_eq_sub {m n} (h : n ≤ m) : psub m n = some (m - n) := -psub_eq_some.2 $ nat.sub_add_cancel h +psub_eq_some.2 $ tsub_add_cancel_of_le h theorem psub_add (m n k) : psub m (n + k) = do x ← psub m n, psub x k := by induction k; simp [*, add_succ, bind_assoc] diff --git a/src/data/nat/totient.lean b/src/data/nat/totient.lean index 08321d2317cc2..add12c6e49f98 100644 --- a/src/data/nat/totient.lean +++ b/src/data/nat/totient.lean @@ -159,7 +159,7 @@ have h2 : (range (p ^ n)).image (* p) ⊆ range (p ^ (n + 1)), end, begin rw [card_sdiff h2, card_image_of_inj_on h1, card_range, - card_range, ← one_mul (p ^ n), pow_succ, ← nat.mul_sub_right_distrib, + card_range, ← one_mul (p ^ n), pow_succ, ← tsub_mul, one_mul, mul_comm] end @@ -179,7 +179,7 @@ begin { apply lt_of_le_of_ne, { rwa succ_le_iff }, { rintro rfl, - rw [totient_one, nat.sub_self] at h, + rw [totient_one, tsub_self] at h, exact one_ne_zero h } }, rw [totient_eq_card_coprime, range_eq_Ico, ←Ico_insert_succ_left hp.le, finset.filter_insert, if_neg (tactic.norm_num.nat_coprime_helper_zero_right p hp), ←nat.card_Ico 1 p] at h, diff --git a/src/data/pnat/basic.lean b/src/data/pnat/basic.lean index 9b3eae7fb90af..89f01acb723e1 100644 --- a/src/data/pnat/basic.lean +++ b/src/data/pnat/basic.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Neil Strickland -/ import algebra.group_power.basic -import data.nat.basic /-! # The positive natural numbers @@ -194,13 +193,13 @@ begin change ((to_pnat' ((a : ℕ) - (b : ℕ)) : ℕ)) = ite ((a : ℕ) > (b : ℕ)) ((a : ℕ) - (b : ℕ)) 1, split_ifs with h, - { exact to_pnat'_coe (nat.sub_pos_of_lt h) }, - { rw [nat.sub_eq_zero_iff_le.mpr (le_of_not_gt h)], refl } + { exact to_pnat'_coe (tsub_pos_of_lt h) }, + { rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h)], refl } end theorem add_sub_of_lt {a b : ℕ+} : a < b → a + (b - a) = b := λ h, eq $ by { rw [add_coe, sub_coe, if_pos h], - exact nat.add_sub_of_le h.le } + exact add_tsub_cancel_of_le h.le } instance : has_well_founded ℕ+ := ⟨(<), measure_wf coe⟩ diff --git a/src/data/pnat/xgcd.lean b/src/data/pnat/xgcd.lean index f58589a851047..c12bd5ca12848 100644 --- a/src/data/pnat/xgcd.lean +++ b/src/data/pnat/xgcd.lean @@ -211,7 +211,7 @@ theorem step_v (hr : u.r ≠ 0) : u.step.v = (u.v).swap := begin let ha : u.r + u.b * u.q = u.a := u.rq_eq, let hr : (u.r - 1) + 1 = u.r := - (add_comm _ 1).trans (nat.add_sub_of_le (nat.pos_of_ne_zero hr)), + (add_comm _ 1).trans (add_tsub_cancel_of_le (nat.pos_of_ne_zero hr)), ext, { change ((u.y * u.q + u.z) * u.b + u.y * (u.r - 1 + 1) : ℕ) = u.y * u.a + u.z * u.b, rw [← ha, hr], ring }, diff --git a/src/data/polynomial/cancel_leads.lean b/src/data/polynomial/cancel_leads.lean index 67d8b2c5b4890..5d8ac8894f5ba 100644 --- a/src/data/polynomial/cancel_leads.lean +++ b/src/data/polynomial/cancel_leads.lean @@ -48,7 +48,7 @@ begin by_cases hp : p = 0, { convert hq, simp [hp, cancel_leads], }, - rw [cancel_leads, sub_eq_add_neg, nat.sub_eq_zero_of_le h, pow_zero, mul_one], + rw [cancel_leads, sub_eq_add_neg, tsub_eq_zero_iff_le.mpr h, pow_zero, mul_one], by_cases h0 : C p.leading_coeff * q + -(C q.leading_coeff * X ^ (q.nat_degree - p.nat_degree) * p) = 0, { convert hq, @@ -64,12 +64,12 @@ begin nsmul_one, degree_neg, degree_mul, zero_add, degree_X, degree_pow], rw leading_coeff_eq_zero at hp hq0, rw [degree_eq_nat_degree hp, degree_eq_nat_degree hq0, ← with_bot.coe_add, with_bot.coe_le_coe, - nat.sub_add_cancel h], }, + tsub_add_cancel_of_le h], }, { contrapose! h0, rw [← leading_coeff_eq_zero, leading_coeff, h0, mul_assoc, mul_comm _ p, - ← nat.sub_add_cancel h, add_comm _ p.nat_degree], - simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, nat.add_sub_cancel_left, coeff_add], - rw [add_comm p.nat_degree, nat.sub_add_cancel h, ← leading_coeff, ← leading_coeff, + ← tsub_add_cancel_of_le h, add_comm _ p.nat_degree], + simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add], + rw [add_comm p.nat_degree, tsub_add_cancel_of_le h, ← leading_coeff, ← leading_coeff, mul_comm _ q.leading_coeff, ← sub_eq_add_neg, ← mul_sub, sub_self, mul_zero] } end diff --git a/src/data/polynomial/coeff.lean b/src/data/polynomial/coeff.lean index ef98cf20159c1..099ef2d77a6d9 100644 --- a/src/data/polynomial/coeff.lean +++ b/src/data/polynomial/coeff.lean @@ -138,7 +138,7 @@ lemma coeff_mul_X_pow' (p : polynomial R) (n d : ℕ) : (p * X ^ n).coeff d = ite (n ≤ d) (p.coeff (d - n)) 0 := begin split_ifs, - { rw [←@nat.sub_add_cancel d n h, coeff_mul_X_pow, nat.add_sub_cancel] }, + { rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right] }, { refine (coeff_mul _ _ _).trans (finset.sum_eq_zero (λ x hx, _)), rw [coeff_X_pow, if_neg, mul_zero], exact ne_of_lt (lt_of_le_of_lt (nat.le_of_add_le_right diff --git a/src/data/polynomial/degree/trailing_degree.lean b/src/data/polynomial/degree/trailing_degree.lean index 0a5853e417ba4..f456ae4dd0ddc 100644 --- a/src/data/polynomial/degree/trailing_degree.lean +++ b/src/data/polynomial/degree/trailing_degree.lean @@ -262,7 +262,7 @@ begin { rw [mem_support_iff, coeff_mul_X_pow'] at hy, exact by_contra (λ h, hy (if_neg h)) }, rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy, - exact (nat.add_le_to_le_sub _ key).mpr (nat_trailing_degree_le_of_ne_zero hy) }, + exact (le_tsub_iff_right key).mp (nat_trailing_degree_le_of_ne_zero hy) }, end end semiring diff --git a/src/data/polynomial/denoms_clearable.lean b/src/data/polynomial/denoms_clearable.lean index f3398f6d7cbe0..0dc884f4b526a 100644 --- a/src/data/polynomial/denoms_clearable.lean +++ b/src/data/polynomial/denoms_clearable.lean @@ -43,7 +43,7 @@ begin refine ⟨r * a ^ n * b ^ (N - n), bi, bu, _⟩, rw [C_mul_X_pow_eq_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, eval_mul, eval_pow, eval_C], rw [ring_hom.map_mul, ring_hom.map_mul, ring_hom.map_pow, ring_hom.map_pow, eval_X, mul_comm], - rw [← nat.sub_add_cancel nN] {occs := occurrences.pos [2]}, + rw [← tsub_add_cancel_of_le nN] {occs := occurrences.pos [2]}, rw [pow_add, mul_assoc, mul_comm (i b ^ n), mul_pow, mul_assoc, mul_assoc (i a ^ n), ← mul_pow], rw [bu, one_pow, mul_one], end diff --git a/src/data/polynomial/derivative.lean b/src/data/polynomial/derivative.lean index 21923bbe1eb60..b95c210e4d7cf 100644 --- a/src/data/polynomial/derivative.lean +++ b/src/data/polynomial/derivative.lean @@ -50,7 +50,8 @@ begin { assume b, cases b, { intros, rw [nat.cast_zero, mul_zero, zero_mul], }, { intros _ H, rw [nat.succ_sub_one b, if_neg (mt (congr_arg nat.succ) H.symm), mul_zero] } }, - { rw [if_pos (nat.add_sub_cancel _ _).symm, mul_one, nat.cast_add, nat.cast_one, mem_support_iff], + { rw [if_pos (add_tsub_cancel_right n 1).symm, mul_one, nat.cast_add, nat.cast_one, + mem_support_iff], intro h, push_neg at h, simp [h], }, end @@ -173,7 +174,7 @@ calc derivative (f * g) = f.sum (λn a, g.sum (λm b, C ((a * b) * (n + m : ℕ) by simp only [nat.cast_add, mul_add, add_mul, C_add, C_mul]; cases n; simp only [nat.succ_sub_succ, pow_zero]; cases m; simp only [nat.cast_zero, C_0, nat.succ_sub_succ, zero_mul, mul_zero, nat.add_succ, - nat.sub_zero, pow_zero, pow_add, one_mul, pow_succ, mul_comm, mul_left_comm] + tsub_zero, pow_zero, pow_add, one_mul, pow_succ, mul_comm, mul_left_comm] ... = derivative f * g + f * derivative g : begin conv { to_rhs, congr, @@ -320,10 +321,10 @@ begin apply le_antisymm, { rw derivative_apply, apply le_trans (degree_sum_le _ _) (sup_le (λ n hn, _)), - apply le_trans (degree_C_mul_X_pow_le _ _) (with_bot.coe_le_coe.2 (nat.sub_le_sub_right _ _)), + apply le_trans (degree_C_mul_X_pow_le _ _) (with_bot.coe_le_coe.2 (tsub_le_tsub_right _ _)), apply le_nat_degree_of_mem_supp _ hn }, { refine le_sup _, - rw [mem_support_derivative, nat.sub_add_cancel, mem_support_iff], + rw [mem_support_derivative, tsub_add_cancel_of_le, mem_support_iff], { show ¬ leading_coeff p = 0, rw [leading_coeff_eq_zero], assume h, rw [h, nat_degree_zero] at hp, @@ -342,7 +343,7 @@ begin have f_nat_degree_pos : 0 < f.nat_degree, { rwa [not_le, ←nat_degree_pos_iff_degree_pos] at absurd }, let m := f.nat_degree - 1, - have hm : m + 1 = f.nat_degree := nat.sub_add_cancel f_nat_degree_pos, + have hm : m + 1 = f.nat_degree := tsub_add_cancel_of_le f_nat_degree_pos, have h2 := coeff_derivative f m, rw polynomial.ext_iff at h, rw [h m, coeff_zero, zero_eq_mul] at h2, diff --git a/src/data/polynomial/div.lean b/src/data/polynomial/div.lean index b426f79fcdc5c..457af91652db4 100644 --- a/src/data/polynomial/div.lean +++ b/src/data/polynomial/div.lean @@ -79,7 +79,7 @@ else exact h.1), degree_sub_lt (by rw [hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_nat_degree h.2, - degree_eq_nat_degree hq0, ← with_bot.coe_add, nat.sub_add_cancel hlt]) + degree_eq_nat_degree hq0, ← with_bot.coe_add, tsub_add_cancel_of_le hlt]) h.2 (by rw [leading_coeff_mul_monic hq, leading_coeff_mul_X_pow, leading_coeff_C]) @@ -265,13 +265,13 @@ begin haveI : nontrivial R := ⟨⟨0, 1, h01⟩⟩, by_cases hfg : f /ₘ g = 0, { rw [hfg, nat_degree_zero], rw div_by_monic_eq_zero_iff hg at hfg, - rw nat.sub_eq_zero_of_le (nat_degree_le_nat_degree $ le_of_lt hfg) }, + rw tsub_eq_zero_iff_le.mpr (nat_degree_le_nat_degree $ le_of_lt hfg) }, have hgf := hfg, rw div_by_monic_eq_zero_iff hg at hgf, push_neg at hgf, have := degree_add_div_by_monic hg hgf, have hf : f ≠ 0, { intro hf, apply hfg, rw [hf, zero_div_by_monic] }, rw [degree_eq_nat_degree hf, degree_eq_nat_degree hg.ne_zero, degree_eq_nat_degree hfg, ← with_bot.coe_add, with_bot.coe_eq_coe] at this, - rw [← this, nat.add_sub_cancel_left] + rw [← this, add_tsub_cancel_left] end lemma div_mod_by_monic_unique {f g} (q r : polynomial R) (hg : monic g) diff --git a/src/data/polynomial/erase_lead.lean b/src/data/polynomial/erase_lead.lean index 3456ab2949a85..6dc66ac43f2fd 100644 --- a/src/data/polynomial/erase_lead.lean +++ b/src/data/polynomial/erase_lead.lean @@ -77,7 +77,7 @@ by rw [C_mul_X_pow_eq_monomial, self_sub_monomial_nat_degree_leading_coeff] lemma erase_lead_ne_zero (f0 : 2 ≤ f.support.card) : erase_lead f ≠ 0 := begin rw [ne.def, ← card_support_eq_zero, erase_lead_support], - exact (zero_lt_one.trans_le $ (nat.sub_le_sub_right f0 1).trans + exact (zero_lt_one.trans_le $ (tsub_le_tsub_right f0 1).trans finset.pred_card_le_card_erase).ne.symm end diff --git a/src/data/polynomial/hasse_deriv.lean b/src/data/polynomial/hasse_deriv.lean index f5410233ee370..1586e250644e6 100644 --- a/src/data/polynomial/hasse_deriv.lean +++ b/src/data/polynomial/hasse_deriv.lean @@ -59,17 +59,18 @@ lemma hasse_deriv_coeff (n : ℕ) : (hasse_deriv k f).coeff n = (n + k).choose k * f.coeff (n + k) := begin rw [hasse_deriv_apply, coeff_sum, sum_def, finset.sum_eq_single (n + k), coeff_monomial], - { simp only [if_true, nat.add_sub_cancel, eq_self_iff_true], }, + { simp only [if_true, add_tsub_cancel_right, eq_self_iff_true], }, { intros i hi hink, rw [coeff_monomial], by_cases hik : i < k, { simp only [nat.choose_eq_zero_of_lt hik, if_t_t, nat.cast_zero, zero_mul], }, - { push_neg at hik, rw if_neg, contrapose! hink, exact (nat.sub_eq_iff_eq_add hik).mp hink, } }, + { push_neg at hik, rw if_neg, contrapose! hink, + exact (tsub_eq_iff_eq_add_of_le hik).mp hink, } }, { intro h, simp only [not_mem_support_iff.mp h, monomial_zero_right, mul_zero, coeff_zero] } end lemma hasse_deriv_zero' : hasse_deriv 0 f = f := -by simp only [hasse_deriv_apply, nat.sub_zero, nat.choose_zero_right, +by simp only [hasse_deriv_apply, tsub_zero, nat.choose_zero_right, nat.cast_one, one_mul, sum_monomial_eq] @[simp] lemma hasse_deriv_zero : @hasse_deriv R _ 0 = linear_map.id := @@ -91,7 +92,7 @@ begin { rw [if_pos hnik, if_pos, ← hnik], apply tsub_eq_of_eq_add_rev, rwa add_comm }, { rw [if_neg hnik, mul_zero], by_cases hkn : k ≤ n, - { rw [← nat.sub_eq_iff_eq_add hkn] at hnik, rw [if_neg hnik] }, + { rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik, rw [if_neg hnik] }, { push_neg at hkn, rw [nat.choose_eq_zero_of_lt hkn, nat.cast_zero, zero_mul, if_t_t] } } end @@ -125,7 +126,7 @@ begin have H : ∀ (n : ℕ), (n! : ℚ) ≠ 0, { exact_mod_cast factorial_ne_zero }, -- why can't `field_simp` help me here? simp only [cast_mul, cast_choose ℚ, h1, h2, -one_div, -mul_eq_zero, - succ_sub_succ_eq_sub, nat.add_sub_cancel, add_tsub_cancel_left] with field_simps, + succ_sub_succ_eq_sub, add_tsub_cancel_right, add_tsub_cancel_left] with field_simps, rw [eq_div_iff_mul_eq (mul_ne_zero (H _) (H _)), eq_comm, div_mul_eq_mul_div, eq_div_iff_mul_eq (mul_ne_zero (H _) (H _))], norm_cast, @@ -138,7 +139,7 @@ begin ext i : 2, simp only [linear_map.smul_apply, comp_app, linear_map.coe_comp, smul_monomial, hasse_deriv_apply, mul_one, monomial_eq_zero_iff, sum_monomial_index, mul_zero, - nat.sub_sub, add_comm l k], + ← tsub_add_eq_tsub_tsub, add_comm l k], rw_mod_cast nsmul_eq_mul, congr' 2, by_cases hikl : i < k + l, @@ -154,8 +155,9 @@ begin have H : ∀ (n : ℕ), (n! : ℚ) ≠ 0, { exact_mod_cast factorial_ne_zero }, -- why can't `field_simp` help me here? simp only [cast_mul, cast_choose ℚ, h1, h2, h3, hikl, -one_div, -mul_eq_zero, - succ_sub_succ_eq_sub, nat.add_sub_cancel, add_tsub_cancel_left] with field_simps, - rw [eq_div_iff_mul_eq, eq_comm, div_mul_eq_mul_div, eq_div_iff_mul_eq, nat.sub_sub, add_comm l k], + succ_sub_succ_eq_sub, add_tsub_cancel_right, add_tsub_cancel_left] with field_simps, + rw [eq_div_iff_mul_eq, eq_comm, div_mul_eq_mul_div, eq_div_iff_mul_eq, ← tsub_add_eq_tsub_tsub, + add_comm l k], { ring, }, all_goals { apply_rules [mul_ne_zero, H] } end @@ -186,8 +188,9 @@ begin { simp only [nat.choose_eq_zero_of_lt hn, nat.cast_zero, zero_mul, mul_zero, monomial_zero_right], }, push_neg at hm hn, - rw [← nat.sub_add_comm hm, ← nat.add_sub_assoc hn, nat.sub_sub, add_comm x.2 x.1, mul_assoc, - ← mul_assoc r, ← (nat.cast_commute _ r).eq, mul_assoc, mul_assoc], }, + rw [tsub_add_eq_add_tsub hm, ← add_tsub_assoc_of_le hn, ← tsub_add_eq_tsub_tsub, + add_comm x.2 x.1, mul_assoc, ← mul_assoc r, ← (nat.cast_commute _ r).eq, mul_assoc, + mul_assoc], }, conv_rhs { apply_congr, skip, rw aux _ H, }, rw_mod_cast [← linear_map.map_sum, ← finset.sum_mul, ← nat.add_choose_eq], end diff --git a/src/data/polynomial/integral_normalization.lean b/src/data/polynomial/integral_normalization.lean index fdec91cd359c9..03b0c5d9e94bc 100644 --- a/src/data/polynomial/integral_normalization.lean +++ b/src/data/polynomial/integral_normalization.lean @@ -111,12 +111,12 @@ calc eval₂ f (z * f p.leading_coeff) (integral_normalization p) congr' 2, by_cases hi : i.1 = nat_degree p, { rw [hi, integral_normalization_coeff_degree, one_mul, leading_coeff, ←pow_succ, - nat.sub_add_cancel one_le_deg], + tsub_add_cancel_of_le one_le_deg], exact degree_eq_nat_degree hp }, { have : i.1 ≤ p.nat_degree - 1 := nat.le_pred_of_lt (lt_of_le_of_ne (le_nat_degree_of_ne_zero (mem_support_iff.mp i.2)) hi), rw [integral_normalization_coeff_ne_nat_degree hi, mul_assoc, ←pow_add, - nat.sub_add_cancel this] } + tsub_add_cancel_of_le this] } end ... = f p.leading_coeff ^ (nat_degree p - 1) * eval₂ f z p : by { simp_rw [eval₂, sum_def, λ i, mul_comm (coeff p i), ring_hom.map_mul, diff --git a/src/data/polynomial/iterated_deriv.lean b/src/data/polynomial/iterated_deriv.lean index 3c5164c3ccdeb..0e3a5cd2f2502 100644 --- a/src/data/polynomial/iterated_deriv.lean +++ b/src/data/polynomial/iterated_deriv.lean @@ -153,7 +153,7 @@ begin ... = f.coeff (m + k.succ) * (∏ i in range k, ↑(m + k.succ - i)) * ↑(m + 1) : by push_cast ... = f.coeff (m + k.succ) * (∏ i in range k.succ, ↑(m + k.succ - i)) : - by rw [prod_range_succ, nat.add_sub_assoc k.le_succ, succ_sub le_rfl, nat.sub_self, mul_assoc] + by rw [prod_range_succ, add_tsub_assoc_of_le k.le_succ, succ_sub le_rfl, tsub_self, mul_assoc] end lemma iterated_deriv_eq_zero_of_nat_degree_lt (h : f.nat_degree < n) : iterated_deriv f n = 0 := @@ -198,7 +198,7 @@ begin by simp_rw [choose_succ_succ, succ_sub_succ, cast_add, C.map_add, add_mul, sum_add_distrib] ... = ∑ (k : ℕ) in range n.succ.succ, C ↑(n.succ.choose k) * p.iterated_deriv (n.succ - k) * q.iterated_deriv k : - by rw [sum_range_succ' _ n.succ, choose_zero_right, nat.sub_zero], + by rw [sum_range_succ' _ n.succ, choose_zero_right, tsub_zero], congr, refine (sum_range_succ' _ _).trans (congr_arg2 (+) _ _), @@ -206,8 +206,8 @@ begin refine sum_congr rfl (λ k hk, _), rw mem_range at hk, congr, - rw [← nat.sub_add_comm (nat.succ_le_of_lt hk), nat.succ_sub_succ] }, - { rw [choose_zero_right, nat.sub_zero] }, + rw [tsub_add_eq_add_tsub (nat.succ_le_of_lt hk), nat.succ_sub_succ] }, + { rw [choose_zero_right, tsub_zero] }, end end comm_semiring diff --git a/src/data/polynomial/mirror.lean b/src/data/polynomial/mirror.lean index d8e8471c0b7cd..5564f7f5247fd 100644 --- a/src/data/polynomial/mirror.lean +++ b/src/data/polynomial/mirror.lean @@ -44,7 +44,7 @@ begin { rw [ha, monomial_zero_right, mirror_zero] }, { rw [mirror, reverse, nat_degree_monomial n a ha, nat_trailing_degree_monomial ha, ←C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, rev_at_le (le_refl n), - nat.sub_self, pow_zero, mul_one] }, + tsub_self, pow_zero, mul_one] }, end lemma mirror_C (a : R) : (C a).mirror = C a := @@ -60,7 +60,7 @@ begin by_cases hR : nontrivial R, { haveI := hR, rw [mirror, nat_degree_mul', reverse_nat_degree, nat_degree_X_pow, - nat.sub_add_cancel p.nat_trailing_degree_le_nat_degree], + tsub_add_cancel_of_le p.nat_trailing_degree_le_nat_degree], rwa [leading_coeff_X_pow, mul_one, reverse_leading_coeff, ne, trailing_coeff_eq_zero] }, { haveI := not_nontrivial_iff_subsingleton.mp hR, exact congr_arg nat_degree (subsingleton.elim p.mirror p) }, @@ -102,7 +102,7 @@ begin { intros n hn hp, rw finset.mem_range_succ_iff at *, rw rev_at_le (hn.trans (nat.le_add_right _ _)), - rw [tsub_le_iff_tsub_le, add_comm, nat.add_sub_cancel, ←mirror_nat_trailing_degree], + rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ←mirror_nat_trailing_degree], exact nat_trailing_degree_le_of_ne_zero hp }, { exact λ n₁ n₂ hn₁ hp₁ hn₂ hp₂ h, by rw [←@rev_at_invol _ n₁, h, rev_at_invol] }, { intros n hn hp, @@ -110,7 +110,7 @@ begin refine ⟨_, _, rev_at_invol.symm⟩, { rw finset.mem_range_succ_iff at *, rw rev_at_le (hn.trans (nat.le_add_right _ _)), - rw [tsub_le_iff_tsub_le, add_comm, nat.add_sub_cancel], + rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right], exact nat_trailing_degree_le_of_ne_zero hp }, { change p.mirror.coeff _ ≠ 0, rwa [coeff_mirror, rev_at_invol] } }, @@ -126,7 +126,7 @@ lemma mirror_eq_zero : p.mirror = 0 ↔ p = 0 := lemma mirror_trailing_coeff : p.mirror.trailing_coeff = p.leading_coeff := by rw [leading_coeff, trailing_coeff, mirror_nat_trailing_degree, coeff_mirror, - rev_at_le (nat.le_add_left _ _), nat.add_sub_cancel] + rev_at_le (nat.le_add_left _ _), add_tsub_cancel_right] lemma mirror_leading_coeff : p.mirror.leading_coeff = p.trailing_coeff := by rw [←p.mirror_mirror, mirror_trailing_coeff, p.mirror_mirror] diff --git a/src/data/polynomial/reverse.lean b/src/data/polynomial/reverse.lean index cc73c3bcc611a..da11277484ca5 100644 --- a/src/data/polynomial/reverse.lean +++ b/src/data/polynomial/reverse.lean @@ -34,7 +34,7 @@ lemma rev_at_fun_invol {N i : ℕ} : rev_at_fun N (rev_at_fun N i) = i := begin unfold rev_at_fun, split_ifs with h j, - { exact nat.sub_sub_self h, }, + { exact tsub_tsub_cancel_of_le h, }, { exfalso, apply j, exact nat.sub_le N i, }, @@ -71,7 +71,7 @@ begin rcases nat.le.dest ho with ⟨o', rfl⟩, repeat { rw rev_at_le (le_add_right rfl.le) }, rw [add_assoc, add_left_comm n' o, ← add_assoc, rev_at_le (le_add_right rfl.le)], - repeat {rw nat.add_sub_cancel_left}, + repeat {rw add_tsub_cancel_left}, end /-- `reflect N f` is the polynomial such that `(reflect N f).coeff i = f.coeff (rev_at N i)`. @@ -183,7 +183,7 @@ lemma coeff_reverse (f : polynomial R) (n : ℕ) : by rw [reverse, coeff_reflect] @[simp] lemma coeff_zero_reverse (f : polynomial R) : coeff (reverse f) 0 = leading_coeff f := -by rw [coeff_reverse, rev_at_le (zero_le f.nat_degree), nat.sub_zero, leading_coeff] +by rw [coeff_reverse, rev_at_le (zero_le f.nat_degree), tsub_zero, leading_coeff] @[simp] lemma reverse_zero : reverse (0 : polynomial R) = 0 := rfl @@ -217,7 +217,7 @@ end lemma reverse_nat_degree (f : polynomial R) : f.reverse.nat_degree = f.nat_degree - f.nat_trailing_degree := -by rw [f.nat_degree_eq_reverse_nat_degree_add_nat_trailing_degree, nat.add_sub_cancel] +by rw [f.nat_degree_eq_reverse_nat_degree_add_nat_trailing_degree, add_tsub_cancel_right] lemma reverse_leading_coeff (f : polynomial R) : f.reverse.leading_coeff = f.trailing_coeff := by rw [leading_coeff, reverse_nat_degree, ←rev_at_le f.nat_trailing_degree_le_nat_degree, diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean index fb7020baa627d..dd5b4ea9c1ac2 100644 --- a/src/data/polynomial/ring_division.lean +++ b/src/data/polynomial/ring_division.lean @@ -141,8 +141,9 @@ lemma nat_trailing_degree_mul (hp : p ≠ 0) (hq : q ≠ 0) : begin simp only [←tsub_eq_of_eq_add_rev (nat_degree_eq_reverse_nat_degree_add_nat_trailing_degree _)], rw [reverse_mul_of_domain, nat_degree_mul hp hq, nat_degree_mul (mt reverse_eq_zero.mp hp) - (mt reverse_eq_zero.mp hq), reverse_nat_degree, reverse_nat_degree, ←nat.sub_sub, nat.add_comm, - nat.add_sub_assoc (nat.sub_le _ _), add_comm, nat.add_sub_assoc (nat.sub_le _ _)], + (mt reverse_eq_zero.mp hq), reverse_nat_degree, reverse_nat_degree, tsub_add_eq_tsub_tsub, + nat.add_comm, add_tsub_assoc_of_le (nat.sub_le _ _), add_comm, + add_tsub_assoc_of_le (nat.sub_le _ _)], end end ring diff --git a/src/data/real/ennreal.lean b/src/data/real/ennreal.lean index d27b38b951e22..bcd44e617f11e 100644 --- a/src/data/real/ennreal.lean +++ b/src/data/real/ennreal.lean @@ -780,7 +780,7 @@ lemma sub_mul (h : 0 < b → b < a → c ≠ ∞) : (a - b) * c = a * c - b * c begin cases le_or_lt a b with hab hab, { simp [hab, mul_right_mono hab] }, rcases eq_or_lt_of_le (zero_le b) with rfl|hb, { simp }, - exact (cancel_of_ne $ mul_ne_top hab.ne_top (h hb hab)).sub_mul + exact (cancel_of_ne $ mul_ne_top hab.ne_top (h hb hab)).tsub_mul end lemma mul_sub (h : 0 < c → c < b → a ≠ ∞) : a * (b - c) = a * b - a * c := diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean index 628dd0015e4f1..05b1e4c4c86b1 100644 --- a/src/data/real/nnreal.lean +++ b/src/data/real/nnreal.lean @@ -490,7 +490,7 @@ section sub In this section we provide a few lemmas about subtraction that do not fit well into any other typeclass. For lemmas about subtraction and addition see lemmas -about `has_ordered_sub` in the file `algebra.order.sub`. See also `mul_sub'` and `sub_mul'`. -/ +about `has_ordered_sub` in the file `algebra.order.sub`. See also `mul_tsub` and `tsub_mul`. -/ lemma sub_def {r p : ℝ≥0} : r - p = real.to_nnreal (r - p) := rfl @@ -499,7 +499,7 @@ lemma coe_sub_def {r p : ℝ≥0} : ↑(r - p) = max (r - p : ℝ) 0 := rfl noncomputable example : has_ordered_sub ℝ≥0 := by apply_instance lemma sub_div (a b c : ℝ≥0) : (a - b) / c = a / c - b / c := -by simp only [div_eq_mul_inv, sub_mul'] +by simp only [div_eq_mul_inv, tsub_mul] end sub diff --git a/src/data/sym/card.lean b/src/data/sym/card.lean index 74e90fc017b50..d52f37ab7dfa5 100644 --- a/src/data/sym/card.lean +++ b/src/data/sym/card.lean @@ -81,7 +81,7 @@ This is because every element `⟦(x, y)⟧` of `sym2 α` not on the diagonal co pairs: `(x, y)` and `(y, x)`. -/ lemma card_image_off_diag (s : finset α) : (s.off_diag.image quotient.mk).card = s.card.choose 2 := -by rw [nat.choose_two_right, nat.mul_sub_left_distrib, mul_one, ←off_diag_card, +by rw [nat.choose_two_right, mul_tsub, mul_one, ←off_diag_card, nat.div_eq_of_eq_mul_right zero_lt_two (two_mul_card_image_off_diag s).symm] lemma card_subtype_diag [fintype α] : diff --git a/src/data/vector/basic.lean b/src/data/vector/basic.lean index 1bef6b9ece070..66bab293ae715 100644 --- a/src/data/vector/basic.lean +++ b/src/data/vector/basic.lean @@ -191,7 +191,7 @@ lemma last_def {v : vector α (n + 1)} : v.last = v.nth (fin.last n) := rfl lemma reverse_nth_zero {v : vector α (n + 1)} : v.reverse.head = v.last := begin have : 0 = v.to_list.length - 1 - n, - { simp only [nat.add_succ_sub_one, add_zero, to_list_length, nat.sub_self, + { simp only [nat.add_succ_sub_one, add_zero, to_list_length, tsub_self, list.length_reverse] }, rw [←nth_zero, last_def, nth_eq_nth_le, nth_eq_nth_le], simp_rw [to_list_reverse, fin.val_eq_coe, fin.coe_last, fin.coe_zero, this], diff --git a/src/data/zmod/basic.lean b/src/data/zmod/basic.lean index 5319a7dc90cbc..729ed89f853d4 100644 --- a/src/data/zmod/basic.lean +++ b/src/data/zmod/basic.lean @@ -651,9 +651,9 @@ begin ((lt_mul_iff_one_lt_left npos.1).2 dec_trivial), have hn2' : (n : ℕ) - n / 2 = n / 2 + 1, { conv {to_lhs, congr, rw [← nat.succ_sub_one n, nat.succ_sub npos.1]}, - rw [← nat.two_mul_odd_div_two hn.1, two_mul, ← nat.succ_add, nat.add_sub_cancel], }, + rw [← nat.two_mul_odd_div_two hn.1, two_mul, ← nat.succ_add, add_tsub_cancel_right], }, have hxn : (n : ℕ) - x.val < n, - { rw [tsub_lt_iff_tsub_lt x.val_le le_rfl, nat.sub_self], + { rw [tsub_lt_iff_tsub_lt x.val_le le_rfl, tsub_self], rw ← zmod.nat_cast_zmod_val x at hx0, exact nat.pos_of_ne_zero (λ h, by simpa [h] using hx0) }, by conv {to_rhs, rw [← nat.succ_le_iff, nat.succ_eq_add_one, ← hn2', ← zero_add (- x), @@ -690,12 +690,12 @@ by rw [val_nat_cast, nat.mod_eq_of_lt h] lemma neg_val' {n : ℕ} [fact (0 < n)] (a : zmod n) : (-a).val = (n - a.val) % n := calc (-a).val = val (-a) % n : by rw nat.mod_eq_of_lt ((-a).val_lt) ... = (n - val a) % n : nat.modeq.add_right_cancel' _ (by rw [nat.modeq, ←val_add, - add_left_neg, nat.sub_add_cancel a.val_le, nat.mod_self, val_zero]) + add_left_neg, tsub_add_cancel_of_le a.val_le, nat.mod_self, val_zero]) lemma neg_val {n : ℕ} [fact (0 < n)] (a : zmod n) : (-a).val = if a = 0 then 0 else n - a.val := begin rw neg_val', - by_cases h : a = 0, { rw [if_pos h, h, val_zero, nat.sub_zero, nat.mod_self] }, + by_cases h : a = 0, { rw [if_pos h, h, val_zero, tsub_zero, nat.mod_self] }, rw if_neg h, apply nat.mod_eq_of_lt, apply nat.sub_lt (fact.out (0 < n)), @@ -791,7 +791,7 @@ begin suffices : (((n+1 : ℕ) % 2) + 2 * ((n + 1) / 2)) - a.val ≤ (n+1) / 2 ↔ (n+1 : ℕ) / 2 < a.val, by rwa [nat.mod_add_div] at this, suffices : (n + 1) % 2 + (n + 1) / 2 ≤ val a ↔ (n + 1) / 2 < val a, - by rw [tsub_le_iff_tsub_le, two_mul, ← add_assoc, nat.add_sub_cancel, this], + by rw [tsub_le_iff_tsub_le, two_mul, ← add_assoc, add_tsub_cancel_right, this], cases (n + 1 : ℕ).mod_two_eq_zero_or_one with hn0 hn1, { split, { assume h, diff --git a/src/dynamics/ergodic/conservative.lean b/src/dynamics/ergodic/conservative.lean index 872bd55888864..d5c2d668fe050 100644 --- a/src/dynamics/ergodic/conservative.lean +++ b/src/dynamics/ergodic/conservative.lean @@ -192,9 +192,9 @@ begin exact (nat.modeq_iff_dvd' hkl.le).1 hn }, refine ⟨f^[k] x, hk, m, _, _⟩, { intro hm, - rw [hm, mul_zero, eq_comm, nat.sub_eq_zero_iff_le] at this, + rw [hm, mul_zero, eq_comm, tsub_eq_zero_iff_le] at this, exact this.not_lt hkl }, - { rwa [← iterate_mul, this, ← iterate_add_apply, nat.sub_add_cancel], + { rwa [← iterate_mul, this, ← iterate_add_apply, tsub_add_cancel_of_le], exact hkl.le } end diff --git a/src/dynamics/ergodic/measure_preserving.lean b/src/dynamics/ergodic/measure_preserving.lean index 9a17c314586d0..539792ee671da 100644 --- a/src/dynamics/ergodic/measure_preserving.lean +++ b/src/dynamics/ergodic/measure_preserving.lean @@ -129,8 +129,8 @@ begin -- without `tactic.skip` Lean closes the extra goal but it takes a long time; not sure why wlog hlt : i < j := hij.lt_or_lt using [i j, j i] tactic.skip, { simp only [set.mem_preimage, finset.mem_range] at hi hj hxi hxj, - refine ⟨f^[i] x, hxi, j - i, ⟨nat.sub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, _⟩, - rwa [← iterate_add_apply, nat.sub_add_cancel hlt.le] }, + refine ⟨f^[i] x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, _⟩, + rwa [← iterate_add_apply, tsub_add_cancel_of_le hlt.le] }, { exact λ hi hj hij hxi hxj, this hj hi hij.symm hxj hxi } end diff --git a/src/dynamics/periodic_pts.lean b/src/dynamics/periodic_pts.lean index 73a4c14faceb4..59292cbee574e 100644 --- a/src/dynamics/periodic_pts.lean +++ b/src/dynamics/periodic_pts.lean @@ -91,8 +91,8 @@ protected lemma sub (hm : is_periodic_pt f m x) (hn : is_periodic_pt f n x) : begin cases le_total n m with h h, { refine left_of_add _ hn, - rwa [nat.sub_add_cancel h] }, - { rw [nat.sub_eq_zero_of_le h], + rwa [tsub_add_cancel_of_le h] }, + { rw [tsub_eq_zero_iff_le.mpr h], apply is_periodic_pt_zero } end diff --git a/src/geometry/euclidean/monge_point.lean b/src/geometry/euclidean/monge_point.lean index 61fa66fb6e21d..9a2ba11034c7d 100644 --- a/src/geometry/euclidean/monge_point.lean +++ b/src/geometry/euclidean/monge_point.lean @@ -142,7 +142,7 @@ begin cases i; simp_rw [centroid_weights_with_circumcenter, circumcenter_weights_with_circumcenter, monge_point_weights_with_circumcenter]; - rw [nat.add_sub_assoc (dec_trivial : 1 ≤ 2), (dec_trivial : 2 - 1 = 1)], + rw [add_tsub_assoc_of_le (dec_trivial : 1 ≤ 2), (dec_trivial : 2 - 1 = 1)], { rw [if_pos (mem_univ _), sub_zero, add_zero, card_fin], have hn3 : (n + 2 + 1 : ℝ) ≠ 0, { exact_mod_cast nat.succ_ne_zero _ }, diff --git a/src/group_theory/nilpotent.lean b/src/group_theory/nilpotent.lean index 6b54140f4fa29..5fa802cd551fc 100644 --- a/src/group_theory/nilpotent.lean +++ b/src/group_theory/nilpotent.lean @@ -219,7 +219,7 @@ begin { refine ⟨hn, λ x m hx g, _⟩, dsimp at hx, by_cases hm : n ≤ m, - { have hnm : n - m = 0 := nat.sub_eq_zero_of_le hm, + { have hnm : n - m = 0 := tsub_eq_zero_iff_le.mpr hm, rw [hnm, h0, subgroup.mem_bot] at hx, subst hx, convert subgroup.one_mem _, @@ -228,16 +228,16 @@ begin apply hH, convert hx, rw nat.sub_succ, - exact nat.succ_pred_eq_of_pos (nat.sub_pos_of_lt hm) } }, + exact nat.succ_pred_eq_of_pos (tsub_pos_of_lt hm) } }, { use n, - rwa nat.sub_self } }, + rwa tsub_self } }, { rintro ⟨H, ⟨h0, hH⟩, n, hn⟩, use (λ m, H (n - m)), split, { refine ⟨hn, λ x m hx g, _⟩, dsimp only at hx, by_cases hm : n ≤ m, - { have hnm : n - m = 0 := nat.sub_eq_zero_of_le hm, + { have hnm : n - m = 0 := tsub_eq_zero_iff_le.mpr hm, dsimp only, rw [hnm, h0], exact mem_top _ }, @@ -245,9 +245,9 @@ begin dsimp only, convert hH x _ hx g, rw nat.sub_succ, - exact (nat.succ_pred_eq_of_pos (nat.sub_pos_of_lt hm)).symm } }, + exact (nat.succ_pred_eq_of_pos (tsub_pos_of_lt hm)).symm } }, { use n, - rwa nat.sub_self } }, + rwa tsub_self } }, end /-- The lower central series of a group `G` is a sequence `H n` of subgroups of `G`, defined diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean index 87a880f2b2497..c020e5426f43e 100644 --- a/src/group_theory/order_of_element.lean +++ b/src/group_theory/order_of_element.lean @@ -324,8 +324,8 @@ variables [add_left_cancel_monoid A] (a) lemma pow_injective_aux (h : n ≤ m) (hm : m < order_of x) (eq : x ^ n = x ^ m) : n = m := by_contradiction $ assume ne : n ≠ m, - have h₁ : m - n > 0, from nat.pos_of_ne_zero (by simp [nat.sub_eq_iff_eq_add h, ne.symm]), - have h₂ : m = n + (m - n) := (nat.add_sub_of_le h).symm, + have h₁ : m - n > 0, from nat.pos_of_ne_zero (by simp [tsub_eq_iff_eq_add_of_le h, ne.symm]), + have h₂ : m = n + (m - n) := (add_tsub_cancel_of_le h).symm, have h₃ : x ^ (m - n) = 1, by { rw [h₂, pow_add] at eq, apply mul_left_cancel, convert eq.symm, exact mul_one (x ^ n) }, have le : order_of x ≤ m - n, from order_of_le_of_pow_eq_one h₁ h₃, @@ -482,7 +482,7 @@ begin by simpa only [not_forall, exists_prop, injective] using (not_injective_infinite_fintype (λi:ℕ, x^i)), wlog h'' : j ≤ i, - refine ⟨i - j, nat.sub_pos_of_lt (lt_of_le_of_ne h'' ne.symm), mul_right_injective (x^j) _⟩, + refine ⟨i - j, tsub_pos_of_lt (lt_of_le_of_ne h'' ne.symm), mul_right_injective (x^j) _⟩, rw [mul_one, ← pow_add, ← a_eq, add_tsub_cancel_of_le h''], end @@ -910,7 +910,7 @@ have pow_mem : ∀ a : M, a ∈ S → ∀ n : ℕ, a ^ (n + 1) ∈ S := { carrier := S, one_mem' := by { obtain ⟨a, ha⟩ := hS1, - rw [←pow_order_of_eq_one a, ←nat.sub_add_cancel (order_of_pos a)], + rw [←pow_order_of_eq_one a, ← tsub_add_cancel_of_le (succ_le_of_lt (order_of_pos a))], exact pow_mem a ha (order_of a - 1) }, mul_mem' := λ a b ha hb, (congr_arg2 (∈) rfl hS2).mp (set.mul_mem_mul ha hb) } diff --git a/src/group_theory/perm/concrete_cycle.lean b/src/group_theory/perm/concrete_cycle.lean index fbba3da861e55..3aec95164d4c1 100644 --- a/src/group_theory/perm/concrete_cycle.lean +++ b/src/group_theory/perm/concrete_cycle.lean @@ -373,7 +373,7 @@ begin have hr : l ~r l.rotate k := ⟨k, rfl⟩, rw form_perm_eq_of_is_rotated hn hr, rw ←nth_le_rotate' l k k, - simp only [nat.mod_eq_of_lt hk, nat.sub_add_cancel hk.le, nat.mod_self], + simp only [nat.mod_eq_of_lt hk, tsub_add_cancel_of_le hk.le, nat.mod_self], rw [to_list_form_perm_nontrivial], { simp }, { simpa using hl }, diff --git a/src/group_theory/perm/cycle_type.lean b/src/group_theory/perm/cycle_type.lean index 24cffd99ef5d7..a8467566c273b 100644 --- a/src/group_theory/perm/cycle_type.lean +++ b/src/group_theory/perm/cycle_type.lean @@ -190,7 +190,7 @@ begin rw eq_repeat_of_mem (λ n hn, or_iff_not_imp_left.mp (hσ.2 n (dvd_of_mem_cycle_type hn)) (ne_of_gt (one_lt_of_mem_cycle_type hn))), use σ.cycle_type.card - 1, - rw nat.sub_add_cancel, + rw tsub_add_cancel_of_le, rw [nat.succ_le_iff, pos_iff_ne_zero, ne, card_cycle_type_eq_zero], rintro rfl, rw order_of_one at hσ, @@ -412,7 +412,7 @@ by deleting the last entry of `v`. -/ def equiv_vector : vectors_prod_eq_one G n ≃ vector G (n - 1) := ((vector_equiv G (n - 1)).trans (if hn : n = 0 then (show vectors_prod_eq_one G (n - 1 + 1) ≃ vectors_prod_eq_one G n, by { rw hn, exact equiv_of_unique_of_unique }) - else by rw nat.sub_add_cancel (nat.pos_of_ne_zero hn))).symm + else by rw tsub_add_cancel_of_le (nat.pos_of_ne_zero hn).nat_succ_le)).symm instance [fintype G] : fintype (vectors_prod_eq_one G n) := fintype.of_equiv (vector G (n - 1)) (equiv_vector G n).symm @@ -441,7 +441,7 @@ end vectors_prod_eq_one lemma exists_prime_order_of_dvd_card {G : Type*} [group G] [fintype G] (p : ℕ) [hp : fact p.prime] (hdvd : p ∣ fintype.card G) : ∃ x : G, order_of x = p := begin - have hp' : p - 1 ≠ 0 := mt nat.sub_eq_zero_iff_le.mp (not_le_of_lt hp.out.one_lt), + have hp' : p - 1 ≠ 0 := mt tsub_eq_zero_iff_le.mp (not_le_of_lt hp.out.one_lt), have Scard := calc p ∣ fintype.card G ^ (p - 1) : hdvd.trans (dvd_pow (dvd_refl _) hp') ... = fintype.card (vectors_prod_eq_one G p) : (vectors_prod_eq_one.card G p).symm, let f : ℕ → vectors_prod_eq_one G p → vectors_prod_eq_one G p := @@ -452,7 +452,7 @@ begin have hf3 : ∀ v, f p v = v := vectors_prod_eq_one.rotate_length, let σ := equiv.mk (f 1) (f (p - 1)) (λ s, by rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3]) - (λ s, by rw [hf2, nat.sub_add_cancel hp.out.pos, hf3]), + (λ s, by rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]), have hσ : ∀ k v, (σ ^ k) v = f k v := λ k v, nat.rec (hf1 v).symm (λ k hk, eq.trans (by exact congr_arg σ hk) (hf2 k 1 v)) k, replace hσ : σ ^ (p ^ 1) = 1 := perm.ext (λ v, by rw [pow_one, hσ, hf3, one_apply]), diff --git a/src/group_theory/perm/list.lean b/src/group_theory/perm/list.lean index 6935bf15d7c27..6f2ee0a5c8569 100644 --- a/src/group_theory/perm/list.lean +++ b/src/group_theory/perm/list.lean @@ -282,13 +282,13 @@ begin rw [length_reverse, ←nat.succ_le_iff, nat.succ_eq_add_one] at hk, cases hk.eq_or_lt with hk' hk', { simp [←hk'] }, - { rw [length_reverse, nat.mod_eq_of_lt hk', ←nat.sub_add_comm (nat.le_pred_of_lt hk'), + { rw [length_reverse, nat.mod_eq_of_lt hk', tsub_add_eq_add_tsub (nat.le_pred_of_lt hk'), nat.mod_eq_of_lt], { simp }, - { rw nat.sub_add_cancel, + { rw tsub_add_cancel_of_le, refine tsub_lt_self _ (nat.zero_lt_succ _), all_goals { simpa using (nat.zero_le _).trans_lt hk' } } } }, - all_goals { rw [nat.sub_sub, ←length_reverse], + all_goals { rw [← tsub_add_eq_tsub_tsub, ←length_reverse], refine tsub_lt_self _ (zero_lt_one.trans_le (le_add_right le_rfl)), exact k.zero_le.trans_lt hk } }, end diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean index 4b3ca49c72bac..d39e2ef52a224 100644 --- a/src/group_theory/sylow.lean +++ b/src/group_theory/sylow.lean @@ -376,9 +376,9 @@ theorem exists_subgroup_card_pow_prime_le [fintype G] (p : ℕ) : ∀ {n m : ℕ have hnm1 : n ≤ m - 1, from le_tsub_of_add_le_right hnm, let ⟨K, hK⟩ := @exists_subgroup_card_pow_prime_le n (m - 1) hp (nat.pow_dvd_of_le_of_pow_dvd tsub_le_self hdvd) H hH hnm1 in - have hdvd' : p ^ ((m - 1) + 1) ∣ card G, by rwa [nat.sub_add_cancel h0m], + have hdvd' : p ^ ((m - 1) + 1) ∣ card G, by rwa [tsub_add_cancel_of_le h0m.nat_succ_le], let ⟨K', hK'⟩ := @exists_subgroup_card_pow_succ _ _ _ _ _ hp hdvd' K hK.1 in - ⟨K', by rw [hK'.1, nat.sub_add_cancel h0m], le_trans hK.2 hK'.2⟩) + ⟨K', by rw [hK'.1, tsub_add_cancel_of_le h0m.nat_succ_le], le_trans hK.2 hK'.2⟩) (λ hnm : n = m, ⟨H, by simp [hH, hnm]⟩) /-- A generalisation of **Sylow's first theorem**. If `p ^ n` divides diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean index 1c29df62742e9..ea2a7adb2903a 100644 --- a/src/linear_algebra/basic.lean +++ b/src/linear_algebra/basic.lean @@ -256,7 +256,7 @@ end lemma pow_map_zero_of_le {f : module.End R M} {m : M} {k l : ℕ} (hk : k ≤ l) (hm : (f^k) m = 0) : (f^l) m = 0 := -by rw [← nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero] +by rw [← tsub_add_cancel_of_le hk, pow_add, mul_apply, hm, map_zero] lemma commute_pow_left_of_commute {f : M →ₛₗ[σ₁₂] M₂} {g : module.End R M} {g₂ : module.End R₂ M₂} diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean index 6cf9c01081cd0..28b78adb48481 100644 --- a/src/linear_algebra/finite_dimensional.lean +++ b/src/linear_algebra/finite_dimensional.lean @@ -1620,17 +1620,17 @@ begin ∃ k, k ≤ finrank K V ∧ linear_map.ker (f ^ k) = linear_map.ker (f ^ k.succ) := exists_ker_pow_eq_ker_pow_succ f, calc (f ^ m).ker = (f ^ (k + (m - k))).ker : - by rw nat.add_sub_of_le (h_k_le.trans hm) + by rw add_tsub_cancel_of_le (h_k_le.trans hm) ... = (f ^ k).ker : by rw ker_pow_constant hk _ ... = (f ^ (k + (finrank K V - k))).ker : ker_pow_constant hk (finrank K V - k) - ... = (f ^ finrank K V).ker : by rw nat.add_sub_of_le h_k_le + ... = (f ^ finrank K V).ker : by rw add_tsub_cancel_of_le h_k_le end lemma ker_pow_le_ker_pow_finrank [finite_dimensional K V] (f : End K V) (m : ℕ) : (f ^ m).ker ≤ (f ^ finrank K V).ker := begin by_cases h_cases: m < finrank K V, - { rw [←nat.add_sub_of_le (nat.le_of_lt h_cases), add_comm, pow_add], + { rw [←add_tsub_cancel_of_le (nat.le_of_lt h_cases), add_comm, pow_add], apply linear_map.ker_le_ker_comp }, { rw [ker_pow_eq_ker_pow_finrank_of_le (le_of_not_lt h_cases)], exact le_refl _ } diff --git a/src/linear_algebra/lagrange.lean b/src/linear_algebra/lagrange.lean index 8c6f35b50203c..1e8ebf42f34e3 100644 --- a/src/linear_algebra/lagrange.lean +++ b/src/linear_algebra/lagrange.lean @@ -61,7 +61,7 @@ by { split_ifs with H, { subst H, apply eval_basis_self }, { exact eval_basis_ne begin unfold basis, generalize hsx : s.erase x = sx, have : x ∉ sx := hsx ▸ finset.not_mem_erase x s, - rw [← finset.insert_erase hx, hsx, finset.card_insert_of_not_mem this, nat.add_sub_cancel], + rw [← finset.insert_erase hx, hsx, finset.card_insert_of_not_mem this, add_tsub_cancel_right], clear hx hsx s, revert this, apply sx.induction_on, { intros hx, rw [finset.prod_empty, nat_degree_one], refl }, { intros y s hys ih hx, rw [finset.mem_insert, not_or_distrib] at hx, diff --git a/src/linear_algebra/matrix/fpow.lean b/src/linear_algebra/matrix/fpow.lean index 1115f3140413b..5ecce7134a849 100644 --- a/src/linear_algebra/matrix/fpow.lean +++ b/src/linear_algebra/matrix/fpow.lean @@ -46,8 +46,8 @@ end theorem pow_sub' (A : M) {m n : ℕ} (ha : is_unit A.det) (h : n ≤ m) : A ^ (m - n) = A ^ m ⬝ (A ^ n)⁻¹ := begin - rw [←nat.sub_add_cancel h, pow_add, mul_eq_mul, matrix.mul_assoc, mul_nonsing_inv, - nat.sub_add_cancel h, matrix.mul_one], + rw [←tsub_add_cancel_of_le h, pow_add, mul_eq_mul, matrix.mul_assoc, mul_nonsing_inv, + tsub_add_cancel_of_le h, matrix.mul_one], simpa using ha.pow n end diff --git a/src/linear_algebra/matrix/nonsingular_inverse.lean b/src/linear_algebra/matrix/nonsingular_inverse.lean index 35e2883552364..bda544b2adf99 100644 --- a/src/linear_algebra/matrix/nonsingular_inverse.lean +++ b/src/linear_algebra/matrix/nonsingular_inverse.lean @@ -304,7 +304,7 @@ begin apply det_adjugate_of_cancel, intros b hb, calc b = a * (det A ^ (fintype.card n - 1 + 1)) : - by rw [←one_mul b, ←ha, mul_assoc, hb, nat.sub_add_cancel zero_lt_card] + by rw [←one_mul b, ←ha, mul_assoc, hb, tsub_add_cancel_of_le zero_lt_card.nat_succ_le] ... = a * det A * det A ^ (fintype.card n - 1) : by ring_exp ... = det A ^ (fintype.card n - 1) : by rw [ha, one_mul] end diff --git a/src/linear_algebra/vandermonde.lean b/src/linear_algebra/vandermonde.lean index 903364524c4ff..4e4575cfe459e 100644 --- a/src/linear_algebra/vandermonde.lean +++ b/src/linear_algebra/vandermonde.lean @@ -115,7 +115,7 @@ begin simp }, { intros i j, simp only [smul_eq_mul, pi.add_apply, fin.coe_succ, fin.coe_cast_succ, pi.smul_apply], - rw [finset.sum_range_succ, add_comm, nat.sub_self, pow_zero, mul_one, finset.mul_sum], + rw [finset.sum_range_succ, add_comm, tsub_self, pow_zero, mul_one, finset.mul_sum], congr' 1, refine finset.sum_congr rfl (λ i' hi', _), rw [mul_left_comm (v 0), nat.succ_sub, pow_succ], diff --git a/src/measure_theory/decomposition/signed_hahn.lean b/src/measure_theory/decomposition/signed_hahn.lean index 6425eaf899125..43422efb0b07f 100644 --- a/src/measure_theory/decomposition/signed_hahn.lean +++ b/src/measure_theory/decomposition/signed_hahn.lean @@ -342,7 +342,7 @@ begin refine find_exists_one_div_lt_min (hn' k) (buffer.lt_aux_2 hk₁) ⟨E, set.subset.trans hE₂ hA', hE₁, _⟩, convert hk₂, norm_cast, - exact nat.sub_add_cancel hk₁ + exact tsub_add_cancel_of_le hk₁ end end exists_subset_restrict_nonpos diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index b2713e8fafebd..a72cd198b885e 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -401,7 +401,7 @@ begin (ennreal.tendsto_sum_nat_add (μ ∘ t) ht) (λ n, measure_Union_le _), intros n m hnm x, simp only [set.mem_Union], - exact λ ⟨i, hi⟩, ⟨i + (m - n), by simpa only [add_assoc, nat.sub_add_cancel hnm] using hi⟩ + exact λ ⟨i, hi⟩, ⟨i + (m - n), by simpa only [add_assoc, tsub_add_cancel_of_le hnm] using hi⟩ end lemma measure_if {x : β} {t : set β} {s : set α} : diff --git a/src/measure_theory/measure/outer_measure.lean b/src/measure_theory/measure/outer_measure.lean index 5b95a52965198..f3fe71156e5e6 100644 --- a/src/measure_theory/measure/outer_measure.lean +++ b/src/measure_theory/measure/outer_measure.lean @@ -131,7 +131,7 @@ begin rcases nat.find_x ⟨i, hx⟩ with ⟨j, hj, hlt⟩, clear hx i, cases 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, nat.sub_add_cancel hnj], + by rw [add_assoc, tsub_add_cancel_of_le hnj.nat_succ_le], refine or.inr (mem_Union.2 ⟨j - (n + 1), _, hlt _ _⟩), { rwa this }, { rw [← nat.succ_le_iff, nat.succ_eq_add_one, this] } diff --git a/src/number_theory/bernoulli.lean b/src/number_theory/bernoulli.lean index 8dba7da43dfb9..a7d637fb0507a 100644 --- a/src/number_theory/bernoulli.lean +++ b/src/number_theory/bernoulli.lean @@ -74,7 +74,7 @@ by { rw [bernoulli'_def', ← fin.sum_univ_eq_sum_range], refl } lemma bernoulli'_spec (n : ℕ) : ∑ k in range n.succ, (n.choose (n - k) : ℚ) / (n - k + 1) * bernoulli' k = 1 := begin - rw [sum_range_succ_comm, bernoulli'_def n, nat.sub_self], + rw [sum_range_succ_comm, bernoulli'_def n, tsub_self], conv in (n.choose (_ - _)) { rw choose_symm (mem_range.1 H).le }, simp only [one_mul, cast_one, sub_self, sub_add_cancel, choose_zero_right, zero_add, div_one], end @@ -286,7 +286,7 @@ begin rw [choose_eq_factorial_div_factorial h.le, eq_comm, div_eq_iff (hne q.succ), succ_eq_add_one, mul_assoc _ _ ↑q.succ!, mul_comm _ ↑q.succ!, ← mul_assoc, div_mul_eq_mul_div, mul_comm (↑n ^ (q - m + 1)), ← mul_assoc _ _ (↑n ^ (q - m + 1)), ← one_div, mul_one_div, - div_div_eq_div_mul, ← nat.sub_add_comm (le_of_lt_succ h), cast_dvd, cast_mul], + div_div_eq_div_mul, tsub_add_eq_add_tsub (le_of_lt_succ h), cast_dvd, cast_mul], { ring }, { exact factorial_mul_factorial_dvd_factorial h.le }, { simp [hne] } }, @@ -336,7 +336,7 @@ begin have h1 : ∀ r : ℚ, r * (p + 1 + 1) * n ^ p.succ / (p + 1 + 1 : ℚ) = r * n ^ p.succ := λ r, by rw [mul_div_right_comm, mul_div_cancel _ hne], have h2 : f 1 + n ^ p.succ = 1 / 2 * n ^ p.succ, - { simp_rw [f, bernoulli_one, choose_one_right, succ_sub_succ_eq_sub, cast_succ, nat.sub_zero, h1], + { simp_rw [f, bernoulli_one, choose_one_right, succ_sub_succ_eq_sub, cast_succ, tsub_zero, h1], ring }, have : ∑ i in range p, bernoulli (i + 2) * (p + 2).choose (i + 2) * n ^ (p - i) / ↑(p + 2) = ∑ i in range p, bernoulli' (i + 2) * (p + 2).choose (i + 2) * n ^ (p - i) / ↑(p + 2) := diff --git a/src/number_theory/bernoulli_polynomials.lean b/src/number_theory/bernoulli_polynomials.lean index a9e43686399d0..e62d2e227dc13 100644 --- a/src/number_theory/bernoulli_polynomials.lean +++ b/src/number_theory/bernoulli_polynomials.lean @@ -52,7 +52,7 @@ begin rw [←sum_range_reflect, add_succ_sub_one, add_zero, bernoulli_poly], apply sum_congr rfl, rintros x hx, - rw mem_range_succ_iff at hx, rw [choose_symm hx, nat.sub_sub_self hx], + rw mem_range_succ_iff at hx, rw [choose_symm hx, tsub_tsub_cancel_of_le hx], end namespace bernoulli_poly @@ -71,7 +71,7 @@ begin rw [bernoulli_poly, polynomial.eval_finset_sum, sum_range_succ], have : ∑ (x : ℕ) in range n, bernoulli x * (n.choose x) * 0 ^ (n - x) = 0, { apply sum_eq_zero (λ x hx, _), - have h : 0 < n - x := nat.sub_pos_of_lt (mem_range.1 hx), + have h : 0 < n - x := tsub_pos_of_lt (mem_range.1 hx), simp [h] }, simp [this], end @@ -96,16 +96,16 @@ end examples begin simp_rw [bernoulli_poly_def, finset.smul_sum, finset.range_eq_Ico, ←finset.sum_Ico_Ico_comm, finset.sum_Ico_eq_sum_range], - simp only [cast_succ, nat.add_sub_cancel_left, nat.sub_zero, zero_add, linear_map.map_add], + simp only [cast_succ, add_tsub_cancel_left, tsub_zero, zero_add, linear_map.map_add], simp_rw [polynomial.smul_monomial, mul_comm (bernoulli _) _, smul_eq_mul, ←mul_assoc], conv_lhs { apply_congr, skip, conv { apply_congr, skip, rw [← nat.cast_mul, choose_mul ((le_tsub_iff_left $ mem_range_le H).1 - $ mem_range_le H_1) (le.intro rfl), nat.cast_mul, add_comm x x_1, nat.add_sub_cancel, + $ mem_range_le H_1) (le.intro rfl), nat.cast_mul, add_comm x x_1, add_tsub_cancel_right, mul_assoc, mul_comm, ←smul_eq_mul, ←polynomial.smul_monomial] }, rw [←sum_smul], }, rw [sum_range_succ_comm], - simp only [add_right_eq_self, cast_succ, mul_one, cast_one, cast_add, nat.add_sub_cancel_left, + simp only [add_right_eq_self, cast_succ, mul_one, cast_one, cast_add, add_tsub_cancel_left, choose_succ_self_right, one_smul, bernoulli_zero, sum_singleton, zero_add, linear_map.map_add, range_one], apply sum_eq_zero (λ x hx, _), @@ -141,7 +141,7 @@ begin rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, coeff_mul, nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ], -- last term is zero so kill with `add_zero` - simp only [ring_hom.map_sub, nat.sub_self, constant_coeff_one, constant_coeff_exp, + simp only [ring_hom.map_sub, tsub_self, constant_coeff_one, constant_coeff_exp, coeff_zero_eq_constant_coeff, mul_zero, sub_self, add_zero], -- Let's multiply both sides by (n+1)! (OK because it's a unit) set u : units ℚ := ⟨(n+1)!, (n+1)!⁻¹, diff --git a/src/number_theory/class_number/admissible_card_pow_degree.lean b/src/number_theory/class_number/admissible_card_pow_degree.lean index 8bff71f953a21..c056f5e20432a 100644 --- a/src/number_theory/class_number/admissible_card_pow_degree.lean +++ b/src/number_theory/class_number/admissible_card_pow_degree.lean @@ -89,7 +89,7 @@ begin have := lt_of_le_of_lt hj (nat.lt_succ_self j), rwa [tsub_lt_iff_tsub_lt hd hbj] at this } }, have : j = b.nat_degree - (nat_degree b - j.succ).succ, - { rw [← nat.succ_sub hbj, nat.succ_sub_succ, nat.sub_sub_self hbj.le] }, + { rw [← nat.succ_sub hbj, nat.succ_sub_succ, tsub_tsub_cancel_of_le hbj.le] }, convert congr_fun i_eq.symm ⟨nat_degree b - j.succ, hj⟩ end diff --git a/src/number_theory/dioph.lean b/src/number_theory/dioph.lean index f8d90b51e7840..5d7a1451ffebe 100644 --- a/src/number_theory/dioph.lean +++ b/src/number_theory/dioph.lean @@ -511,13 +511,13 @@ ext (D&1 D= D&0 D+ D&2 D∨ D&1 D≤ D&2 D∧ D&0 D= D.0) $ (vector_all_iff_fora show (y = x + z ∨ y ≤ z ∧ x = 0) ↔ y - z = x, from ⟨λo, begin rcases o with ae | ⟨yz, x0⟩, - { rw [ae, nat.add_sub_cancel] }, - { rw [x0, nat.sub_eq_zero_of_le yz] } + { rw [ae, add_tsub_cancel_right] }, + { rw [x0, tsub_eq_zero_iff_le.mpr yz] } end, λh, begin subst x, cases le_total y z with yz zy, - { exact or.inr ⟨yz, nat.sub_eq_zero_of_le yz⟩ }, - { exact or.inl (nat.sub_add_cancel zy).symm }, + { exact or.inr ⟨yz, tsub_eq_zero_iff_le.mpr yz⟩ }, + { exact or.inl (tsub_add_cancel_of_le zy).symm }, end⟩ localized "infix ` D- `:80 := dioph.sub_dioph" in dioph diff --git a/src/number_theory/liouville/liouville_constant.lean b/src/number_theory/liouville/liouville_constant.lean index 32bafe6a54c0a..f641942477311 100644 --- a/src/number_theory/liouville/liouville_constant.lean +++ b/src/number_theory/liouville/liouville_constant.lean @@ -158,7 +158,7 @@ begin rw [sum_range_succ, h_k, div_add_div, div_eq_div_iff, add_mul], { norm_cast, rw [add_mul, one_mul, nat.factorial_succ, - show k.succ * k! - k! = (k.succ - 1) * k!, by rw [nat.mul_sub_right_distrib, one_mul], + show k.succ * k! - k! = (k.succ - 1) * k!, by rw [tsub_mul, one_mul], nat.succ_sub_one, add_mul, one_mul, pow_add], simp [mul_assoc] }, refine mul_ne_zero_iff.mpr ⟨_, _⟩, diff --git a/src/number_theory/lucas_lehmer.lean b/src/number_theory/lucas_lehmer.lean index ea98bc19bdf0d..3d46db2c374ba 100644 --- a/src/number_theory/lucas_lehmer.lean +++ b/src/number_theory/lucas_lehmer.lean @@ -50,7 +50,7 @@ end @[simp] lemma succ_mersenne (k : ℕ) : mersenne k + 1 = 2 ^ k := begin - rw [mersenne, nat.sub_add_cancel], + rw [mersenne, tsub_add_cancel_of_le], exact one_le_pow_of_one_le (by norm_num) k end @@ -425,7 +425,7 @@ open lucas_lehmer theorem lucas_lehmer_sufficiency (p : ℕ) (w : 1 < p) : lucas_lehmer_test p → (mersenne p).prime := begin let p' := p - 2, - have z : p = p' + 2 := (nat.sub_eq_iff_eq_add w).mp rfl, + have z : p = p' + 2 := (tsub_eq_iff_eq_add_of_le w.nat_succ_le).mp rfl, have w : 1 < p' + 2 := (nat.lt_of_sub_eq_succ rfl), contrapose, intros a t, diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean index a246da8a64cbf..2b213f6745bbc 100644 --- a/src/number_theory/padics/padic_norm.lean +++ b/src/number_theory/padics/padic_norm.lean @@ -469,7 +469,7 @@ begin cc }, { rw [←h, padic_val_nat.div], { have: 1 ≤ padic_val_nat p n := one_le_padic_val_nat_of_dvd (by linarith) p_dvd_n, - exact (nat.sub_eq_iff_eq_add this).mp rfl, }, + exact (tsub_eq_iff_eq_add_of_le this).mp rfl, }, { exact p_dvd_n, }, }, { suffices : p.coprime q, { rw [padic_val_nat.div' this (min_fac_dvd n), add_zero], }, diff --git a/src/number_theory/padics/ring_homs.lean b/src/number_theory/padics/ring_homs.lean index 6d6c8a536fd10..564f06fb34e54 100644 --- a/src/number_theory/padics/ring_homs.lean +++ b/src/number_theory/padics/ring_homs.lean @@ -316,7 +316,7 @@ begin apply nat.mul_le_mul_left, apply le_pred_of_lt, apply zmod.val_lt }, - { rw [nat.mul_sub_left_distrib, mul_one, ← pow_succ'], + { rw [mul_tsub, mul_one, ← pow_succ'], apply add_tsub_cancel_of_le (le_of_lt hp) } } end @@ -334,12 +334,12 @@ lemma dvd_appr_sub_appr (x : ℤ_[p]) (m n : ℕ) (h : m ≤ n) : begin obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le h, clear h, induction k with k ih, - { simp only [add_zero, nat.sub_self, dvd_zero], }, + { simp only [add_zero, tsub_self, dvd_zero], }, rw [nat.succ_eq_add_one, ← add_assoc], dsimp [appr], split_ifs with h, { exact ih }, - rw [add_comm, nat.add_sub_assoc (appr_mono _ (nat.le_add_right m k))], + rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (nat.le_add_right m k))], apply dvd_add _ ih, apply dvd_mul_of_dvd_left, apply pow_dvd_pow _ (nat.le_add_right m k), diff --git a/src/number_theory/pell.lean b/src/number_theory/pell.lean index 1fee2ef79f7f9..fc009cf1fa311 100644 --- a/src/number_theory/pell.lean +++ b/src/number_theory/pell.lean @@ -59,7 +59,7 @@ include a1 private def d := a*a - 1 @[simp] theorem d_pos : 0 < d := -nat.sub_pos_of_lt (mul_lt_mul a1 (le_of_lt a1) dec_trivial dec_trivial : 1*1 n, k ≤ 2*n → (↑(xn k % xn n) : ℤ) = xn n - xn (2 * n - k), from λk kn k2n, let k2nl := lt_of_add_lt_add_right $ show 2*n-k+k < n+k, by - {rw nat.sub_add_cancel, rw two_mul; exact (add_lt_add_left kn n), exact k2n } in + {rw tsub_add_cancel_of_le, rw two_mul; exact (add_lt_add_left kn n), exact k2n } in have xle : xn (2 * n - k) ≤ xn n, from le_of_lt $ strict_mono_x k2nl, suffices xn k % xn n = xn n - xn (2 * n - k), by rw [this, int.coe_nat_sub xle], by { rw ← nat.mod_eq_of_lt (nat.sub_lt (x_pos a1 n) (x_pos a1 (2 * n - k))), apply modeq.add_right_cancel' (xn a1 (2 * n - k)), - rw [nat.sub_add_cancel xle], + rw [tsub_add_cancel_of_le xle], have t := xn_modeq_x2n_sub_lem a1 k2nl.le, - rw nat.sub_sub_self k2n at t, + rw tsub_tsub_cancel_of_le k2n at t, exact t.trans dvd_rfl.zero_modeq_nat }, (lt_trichotomy j n).elim (λ (jn : j < n), eq_of_xn_modeq_lem1 ij (lt_of_le_of_ne jn jnn)) $ λ o, o.elim @@ -493,13 +493,13 @@ theorem eq_of_xn_modeq_lem3 {i n} (npos : 0 < n) : cases jn, apply int.lt_of_coe_nat_lt_coe_nat, rw [lem2 (n+1) (nat.lt_succ_self _) j2n, - show 2 * n - (n + 1) = n - 1, by rw[two_mul, ← nat.sub_sub, nat.add_sub_cancel]], + show 2 * n - (n + 1) = n - 1, by rw[two_mul, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]], refine lt_sub_left_of_add_lt (int.coe_nat_lt_coe_nat_of_lt _), cases (lt_or_eq_of_le $ nat.le_of_succ_le_succ ij) with lin ein, { rw nat.mod_eq_of_lt (strict_mono_x _ lin), have ll : xn a1 (n-1) + xn a1 (n-1) ≤ xn a1 n, { rw [← two_mul, mul_comm, show xn a1 n = xn a1 (n-1+1), - by rw [nat.sub_add_cancel npos], xn_succ], + by rw [tsub_add_cancel_of_le (succ_le_of_lt npos)], xn_succ], exact le_trans (nat.mul_le_mul_left _ a1) (nat.le_add_right _ _) }, have npm : (n-1).succ = n := nat.succ_pred_eq_of_pos npos, have il : i ≤ n - 1, { apply nat.le_of_succ_le_succ, rw npm, exact lin }, @@ -509,11 +509,12 @@ theorem eq_of_xn_modeq_lem3 {i n} (npos : 0 < n) : apply lt_of_le_of_ne ll, rw ← two_mul, exact λe, ntriv $ - let ⟨a2, s1⟩ := @eq_of_xn_modeq_lem2 _ a1 (n-1) (by rwa [nat.sub_add_cancel npos]) in - have n1 : n = 1, from le_antisymm (nat.le_of_sub_eq_zero s1) npos, + let ⟨a2, s1⟩ := @eq_of_xn_modeq_lem2 _ a1 (n-1) + (by rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)]) in + have n1 : n = 1, from le_antisymm (tsub_eq_zero_iff_le.mp s1) npos, by rw [ile, a2, n1]; exact ⟨rfl, rfl, rfl, rfl⟩ } }, { rw [ein, nat.mod_self, add_zero], - exact strict_mono_x _ (nat.pred_lt $ ne_of_gt npos) } }) + exact strict_mono_x _ (nat.pred_lt npos.ne') } }) (λ (jn : j > n), have lem1 : j ≠ n → xn j % xn n < xn (j + 1) % xn n → xn i % xn n < xn (j + 1) % xn n, from λjn s, @@ -525,7 +526,7 @@ theorem eq_of_xn_modeq_lem3 {i n} (npos : 0 < n) : rw [lem2 j jn (le_of_lt j2n), lem2 (j+1) (nat.le_succ_of_le jn) j2n], refine sub_lt_sub_left (int.coe_nat_lt_coe_nat_of_lt $ strict_mono_x _ _) _, rw [nat.sub_succ], - exact nat.pred_lt (ne_of_gt $ nat.sub_pos_of_lt j2n) }) + exact nat.pred_lt (ne_of_gt $ tsub_pos_of_lt j2n) }) theorem eq_of_xn_modeq_le {i j n} (npos : 0 < n) (ij : i ≤ j) (j2n : j ≤ 2 * n) (h : xn i ≡ xn j [MOD xn n]) (ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)) : i = j := @@ -557,12 +558,12 @@ have npos : 0 < n, from lt_of_lt_of_le ipos hin, (λj2n : j ≤ 2 * n, eq_of_xn_modeq npos j2n i2n h $ λa2 n1, ⟨λj0 i2, by rw [n1, i2] at hin; exact absurd hin dec_trivial, λj2 i0, ne_of_gt ipos i0⟩) - (λj2n : 2 * n < j, suffices i = 4*n - j, by rw [this, nat.add_sub_of_le j4n], + (λj2n : 2 * n < j, suffices i = 4*n - j, by rw [this, add_tsub_cancel_of_le j4n], have j42n : 4*n - j ≤ 2*n, from @nat.le_of_add_le_add_right j _ _ $ - by rw [nat.sub_add_cancel j4n, show 4*n = 2*n + 2*n, from right_distrib 2 2 n]; + by rw [tsub_add_cancel_of_le j4n, show 4*n = 2*n + 2*n, from right_distrib 2 2 n]; exact nat.add_le_add_left (le_of_lt j2n) _, eq_of_xn_modeq npos i2n j42n - (h.symm.trans $ let t := xn_modeq_x4n_sub j42n in by rwa [nat.sub_sub_self j4n] at t) + (h.symm.trans $ let t := xn_modeq_x4n_sub j42n in by rwa [tsub_tsub_cancel_of_le j4n] at t) (λa2 n1, ⟨λi0, absurd i0 (ne_of_gt ipos), λi2, by { rw [n1, i2] at hin, exact absurd hin dec_trivial }⟩)) diff --git a/src/number_theory/primorial.lean b/src/number_theory/primorial.lean index 0a8783bf19990..005aeef384730 100644 --- a/src/number_theory/primorial.lean +++ b/src/number_theory/primorial.lean @@ -37,7 +37,7 @@ begin { exfalso, rw ←not_even_iff at n_even r, have e : even (n + 1 - n) := (even_sub (lt_add_one n).le).2 (iff_of_false n_even r), - simp only [nat.add_sub_cancel_left, not_even_one] at e, + simp only [add_tsub_cancel_left, not_even_one] at e, exact e, }, }, apply finset.prod_congr, { rw [@range_succ (n + 1), filter_insert, if_neg not_prime], }, @@ -60,7 +60,7 @@ begin have t : ¬(p ∣ (2 * m + 1 - (m + 1))!), { intros p_div_fact, have p_small : p ≤ 2 * m + 1 - (m + 1) := (prime.dvd_factorial is_prime).mp p_div_fact, - have t : 2 * m + 1 - (m + 1) = m, by { norm_num, rw two_mul m, exact nat.add_sub_cancel m m, }, + have t : 2 * m + 1 - (m + 1) = m, { norm_num, rw two_mul m, exact add_tsub_cancel_right m m, }, rw t at p_small, obtain p_lt_m | rfl | m_lt_p : _ := lt_trichotomy p m, { have r : m < m + 1 := lt_add_one m, linarith, }, diff --git a/src/number_theory/quadratic_reciprocity.lean b/src/number_theory/quadratic_reciprocity.lean index 6588716c217f4..b3debc4dec428 100644 --- a/src/number_theory/quadratic_reciprocity.lean +++ b/src/number_theory/quadratic_reciprocity.lean @@ -341,7 +341,7 @@ begin simp only [mem_union, mem_filter, mem_Ico, mem_product]; tauto), rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_disjoint_union hdisj, hunion, card_product], - simp only [card_Ico, nat.sub_zero, succ_sub_succ_eq_sub] + simp only [card_Ico, tsub_zero, succ_sub_succ_eq_sub] end variables (p q : ℕ) [fact p.prime] [fact q.prime] diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean index 345303362bd03..b9127d6a93dc2 100644 --- a/src/order/complete_lattice.lean +++ b/src/order/complete_lattice.lean @@ -5,6 +5,7 @@ Authors: Johannes Hölzl -/ import order.bounds import data.set.bool +import data.nat.basic /-! # Theory of complete lattices @@ -1068,7 +1069,7 @@ lemma supr_ge_eq_supr_nat_add {u : ℕ → α} (n : ℕ) : (⨆ i ≥ n, u i) = begin apply le_antisymm; simp only [supr_le_iff], - { exact λ i hi, le_Sup ⟨i - n, by { dsimp only, rw nat.sub_add_cancel hi }⟩ }, + { exact λ i hi, le_Sup ⟨i - n, by { dsimp only, rw tsub_add_cancel_of_le hi }⟩ }, { exact λ i, le_Sup ⟨i + n, supr_pos (nat.le_add_left _ _)⟩ } end diff --git a/src/order/filter/at_top_bot.lean b/src/order/filter/at_top_bot.lean index 540e8397783d4..c0e5d56edb4e2 100644 --- a/src/order/filter/at_top_bot.lean +++ b/src/order/filter/at_top_bot.lean @@ -1090,13 +1090,13 @@ lemma map_add_at_top_eq_nat (k : ℕ) : map (λa, a + k) at_top = at_top := map_at_top_eq_of_gc (λa, a - k) k (assume a b h, add_le_add_right h k) (assume a b h, (le_tsub_iff_right h).symm) - (assume a h, by rw [nat.sub_add_cancel h]) + (assume a h, by rw [tsub_add_cancel_of_le h]) lemma map_sub_at_top_eq_nat (k : ℕ) : map (λa, a - k) at_top = at_top := map_at_top_eq_of_gc (λa, a + k) 0 - (assume a b h, nat.sub_le_sub_right h _) + (assume a b h, tsub_le_tsub_right h _) (assume a b _, tsub_le_iff_right) - (assume b _, by rw [nat.add_sub_cancel]) + (assume b _, by rw [add_tsub_cancel_right]) lemma tendsto_add_at_top_nat (k : ℕ) : tendsto (λa, a + k) at_top at_top := le_of_eq (map_add_at_top_eq_nat k) @@ -1120,7 +1120,7 @@ map_at_top_eq_of_gc (λb, b * k + (k - 1)) 1 cases k, exact (lt_irrefl _ hk).elim, rw [add_mul, one_mul, nat.succ_sub_succ_eq_sub, - nat.sub_zero, nat.add_succ, nat.lt_succ_iff], + tsub_zero, nat.add_succ, nat.lt_succ_iff], end) (assume b _, calc b = (b * k) / k : by rw [nat.mul_div_cancel b hk] diff --git a/src/order/jordan_holder.lean b/src/order/jordan_holder.lean index 537c20b6bda72..1240f93f63840 100644 --- a/src/order/jordan_holder.lean +++ b/src/order/jordan_holder.lean @@ -265,7 +265,7 @@ def of_list (l : list X) (hl : l ≠ []) (hc : list.chain' is_maximal l) : composition_series X := { length := l.length - 1, series := λ i, l.nth_le i begin - conv_rhs { rw ← nat.sub_add_cancel (list.length_pos_of_ne_nil hl) }, + conv_rhs { rw ← tsub_add_cancel_of_le (nat.succ_le_of_lt (list.length_pos_of_ne_nil hl)) }, exact i.2 end, step' := λ ⟨i, hi⟩, list.chain'_iff_nth_le.1 hc i hi } @@ -291,8 +291,8 @@ of_list_to_list s to_list (of_list l hl hc) = l := begin refine list.ext_le _ _, - { rw [length_to_list, length_of_list, nat.sub_add_cancel - (list.length_pos_of_ne_nil hl)] }, + { rw [length_to_list, length_of_list, + tsub_add_cancel_of_le (nat.succ_le_of_lt $ list.length_pos_of_ne_nil hl)] }, { assume i hi hi', dsimp [of_list, to_list], rw [list.nth_le_of_fn'], @@ -451,7 +451,7 @@ lemma append_nat_add_aux begin cases i, simp only [fin.append, nat.not_lt_zero, fin.nat_add_mk, add_lt_iff_neg_left, - nat.add_sub_cancel_left, dif_neg, fin.cast_succ_mk, not_false_iff, fin.coe_mk] + add_tsub_cancel_left, dif_neg, fin.cast_succ_mk, not_false_iff, fin.coe_mk] end lemma append_succ_nat_add_aux @@ -462,7 +462,7 @@ lemma append_succ_nat_add_aux begin cases i with i hi, simp only [fin.append, add_assoc, nat.not_lt_zero, fin.nat_add_mk, add_lt_iff_neg_left, - nat.add_sub_cancel_left, fin.succ_mk, dif_neg, not_false_iff, fin.coe_mk] + add_tsub_cancel_left, fin.succ_mk, dif_neg, not_false_iff, fin.coe_mk] end /-- Append two composition series `s₁` and `s₂` such that diff --git a/src/order/well_founded_set.lean b/src/order/well_founded_set.lean index 025cf25395493..fce6a9a517d09 100644 --- a/src/order/well_founded_set.lean +++ b/src/order/well_founded_set.lean @@ -619,7 +619,7 @@ begin exact λ n, hf1.1 (set.mem_range_self n) _ (list.head_mem_self (hnil n)) }, have hf' := hf2 (g 0) (λ n, if n < g 0 then f n else list.tail (f (g (n - g 0)))) (λ m hm, (if_pos hm).symm) _, - swap, { simp only [if_neg (lt_irrefl (g 0)), nat.sub_self], + swap, { simp only [if_neg (lt_irrefl (g 0)), tsub_self], rw [list.length_tail, ← nat.pred_eq_sub_one], exact nat.pred_lt (λ con, hnil _ (list.length_eq_zero.1 con)) }, rw [is_bad_seq] at hf', @@ -634,7 +634,7 @@ begin { apply hf1.2 m n mn, rwa [if_pos hn, if_pos (mn.trans hn)] at hmn }, { obtain ⟨n', rfl⟩ := le_iff_exists_add.1 (not_lt.1 hn), - rw [if_neg hn, add_comm (g 0) n', nat.add_sub_cancel] at hmn, + rw [if_neg hn, add_comm (g 0) n', add_tsub_cancel_right] at hmn, split_ifs at hmn with hm hm, { apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le)), exact trans hmn (list.tail_sublist_forall₂_self _) }, diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean index 7ab352e3193b3..1fb417aad7041 100644 --- a/src/ring_theory/ideal/operations.lean +++ b/src/ring_theory/ideal/operations.lean @@ -397,7 +397,7 @@ def radical (I : ideal R) : ideal R := x ^ c * y ^ (m + n - c) * (nat.choose (m + n) c) ∈ I, from λ c hc, or.cases_on (le_total c m) (λ hcm, I.mul_mem_right _ $ I.mul_mem_left _ $ nat.add_comm n m ▸ - (nat.add_sub_assoc hcm n).symm ▸ + (add_tsub_assoc_of_le hcm n).symm ▸ (pow_add y n (m-c)).symm ▸ I.mul_mem_right _ hyni) (λ hmc, I.mul_mem_right _ $ I.mul_mem_right _ $ add_tsub_cancel_of_le hmc ▸ (pow_add x m (c-m)).symm ▸ I.mul_mem_right _ hxmi)⟩, diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean index 3807b4ddd7297..2cd4d7d1cb19a 100644 --- a/src/ring_theory/integral_closure.lean +++ b/src/ring_theory/integral_closure.lean @@ -696,18 +696,18 @@ begin rw [ring_hom.map_mul, mul_assoc], congr, have : a_inv ^ p.nat_degree = a_inv ^ (p.nat_degree - i) * a_inv ^ i, - { rw [← pow_add a_inv, nat.sub_add_cancel (nat.le_of_lt_succ (finset.mem_range.mp hi))] }, + { rw [← pow_add a_inv, tsub_add_cancel_of_le (nat.le_of_lt_succ (finset.mem_range.mp hi))] }, rw [ring_hom.map_pow, this, ← mul_assoc, ← mul_pow, ha_inv, one_pow, one_mul] }, -- Since `q(a) = 0` and `q(a) = q'(a) * a + 1`, we have `a * -q'(a) = 1`. -- TODO: we could use a lemma for `polynomial.div_X` here. - rw [finset.sum_range_succ_comm, p_monic.coeff_nat_degree, one_mul, nat.sub_self, pow_zero, + rw [finset.sum_range_succ_comm, p_monic.coeff_nat_degree, one_mul, tsub_self, pow_zero, add_eq_zero_iff_eq_neg, eq_comm] at hq, rw [mul_comm, ← neg_mul_eq_neg_mul, finset.sum_mul], convert hq using 2, refine finset.sum_congr rfl (λ i hi, _), have : 1 ≤ p.nat_degree - i := le_tsub_of_add_le_left (finset.mem_range.mp hi), - rw [mul_assoc, ← pow_succ', nat.sub_add_cancel this] + rw [mul_assoc, ← pow_succ', tsub_add_cancel_of_le this] end end algebra diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean index cc7e8db958335..49f7cf6a0b4f2 100644 --- a/src/ring_theory/multiplicity.lean +++ b/src/ring_theory/multiplicity.lean @@ -313,11 +313,11 @@ lemma finite_mul_aux {p : α} (hp : prime p) : ∀ {n m : ℕ} {a b : α}, have wf : (n - 1) < n, from tsub_lt_self hn0 dec_trivial, have hpx : ¬ p ^ (n - 1 + 1) ∣ x, from λ ⟨y, hy⟩, ha (hx.symm ▸ ⟨y, mul_right_cancel₀ hp.1 - $ by rw [nat.sub_add_cancel hn0] at hy; + $ by rw [tsub_add_cancel_of_le (succ_le_of_lt hn0)] at hy; simp [hy, pow_add, mul_comm, mul_assoc, mul_left_comm]⟩), have 1 ≤ n + m, from le_trans hn0 (nat.le_add_right n m), finite_mul_aux hpx hb ⟨s, mul_right_cancel₀ hp.1 begin - rw [← nat.sub_add_comm hn0, nat.sub_add_cancel this], + rw [tsub_add_eq_add_tsub (succ_le_of_lt hn0), tsub_add_cancel_of_le this], clear _fun_match _fun_match finite_mul_aux, simp [*, mul_comm, mul_assoc, mul_left_comm, pow_add] at * end⟩) @@ -326,10 +326,10 @@ lemma finite_mul_aux {p : α} (hp : prime p) : ∀ {n m : ℕ} {a b : α}, have wf : (m - 1) < m, from tsub_lt_self hm0 dec_trivial, have hpx : ¬ p ^ (m - 1 + 1) ∣ x, from λ ⟨y, hy⟩, hb (hx.symm ▸ ⟨y, mul_right_cancel₀ hp.1 - $ by rw [nat.sub_add_cancel hm0] at hy; + $ by rw [tsub_add_cancel_of_le (succ_le_of_lt hm0)] at hy; simp [hy, pow_add, mul_comm, mul_assoc, mul_left_comm]⟩), finite_mul_aux ha hpx ⟨s, mul_right_cancel₀ hp.1 begin - rw [add_assoc, nat.sub_add_cancel hm0], + rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)], clear _fun_match _fun_match finite_mul_aux, simp [*, mul_comm, mul_assoc, mul_left_comm, pow_add] at * end⟩) diff --git a/src/ring_theory/perfection.lean b/src/ring_theory/perfection.lean index 91323758ad2a9..6b35acc55bc5a 100644 --- a/src/ring_theory/perfection.lean +++ b/src/ring_theory/perfection.lean @@ -129,7 +129,7 @@ nat.rec_on m rfl $ λ m ih, by erw [function.iterate_succ_apply', coeff_frobeniu lemma coeff_iterate_frobenius' (f : ring.perfection R p) (n m : ℕ) (hmn : m ≤ n) : coeff R p n (frobenius _ p ^[m] f) = coeff R p (n - m) f := -eq.symm $ (coeff_iterate_frobenius _ _ m).symm.trans $ (nat.sub_add_cancel hmn).symm ▸ rfl +eq.symm $ (coeff_iterate_frobenius _ _ m).symm.trans $ (tsub_add_cancel_of_le hmn).symm ▸ rfl lemma pth_root_frobenius : (pth_root R p).comp (frobenius _ p) = ring_hom.id _ := ring_hom.ext $ λ x, ext $ λ n, diff --git a/src/ring_theory/polynomial/bernstein.lean b/src/ring_theory/polynomial/bernstein.lean index 91c20f1c9f419..ab3e862098dce 100644 --- a/src/ring_theory/polynomial/bernstein.lean +++ b/src/ring_theory/polynomial/bernstein.lean @@ -94,7 +94,7 @@ begin split_ifs, { subst h, simp, }, { 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 [nat.choose_eq_zero_of_lt ((tsub_eq_zero_iff_le.mp w).lt_of_ne (ne.symm h))] }, { simp [zero_pow w] } }, end. @@ -116,7 +116,7 @@ begin refine congr (congr_arg (*) (congr (congr_arg (*) _) rfl)) rfl, -- Now it's just about binomial coefficients exact_mod_cast congr_arg (λ m : ℕ, (m : polynomial R)) (nat.succ_mul_choose_eq n ν).symm, }, - { rw nat.sub_sub, rw [←mul_assoc,←mul_assoc], congr' 1, + { rw [← tsub_add_eq_tsub_tsub, ← mul_assoc, ← mul_assoc], congr' 1, rw mul_comm , rw [←mul_assoc,←mul_assoc], congr' 1, norm_cast, congr' 1, @@ -178,7 +178,7 @@ begin { simp [eval_at_0], }, { have h' : ν ≤ n-1 := le_tsub_of_add_le_right h, simp only [derivative_succ, ih (n-1) h', iterate_derivative_succ_at_0_eq_zero, - nat.succ_sub_succ_eq_sub, nat.sub_zero, sub_zero, + nat.succ_sub_succ_eq_sub, tsub_zero, sub_zero, 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], @@ -186,11 +186,11 @@ begin { 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 [← tsub_add_eq_tsub_tsub, add_comm, tsub_add_cancel_of_le h''] }, rw [this, pochhammer_eval_succ], - rw_mod_cast nat.sub_add_cancel (h'.trans n.pred_le) } } }, + rw_mod_cast tsub_add_cancel_of_le (h'.trans n.pred_le) } } }, { simp only [not_le] at h, - rw [nat.sub_eq_zero_of_le (nat.le_pred_of_lt h), eq_zero_of_lt R h], + rw [tsub_eq_zero_iff_le.mpr (nat.le_pred_of_lt h), eq_zero_of_lt R h], simp [pos_iff_ne_zero.mp (pos_of_gt h)] }, end @@ -205,7 +205,7 @@ begin 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)) } + exact pochhammer_pos _ _ (tsub_pos_of_lt (nat.lt_of_succ_le h)) } end /-! @@ -231,7 +231,7 @@ begin { simp, }, { congr, norm_cast, - rw [nat.sub_sub, nat.sub_sub_self (nat.succ_le_iff.mpr h')] }, + rw [← tsub_add_eq_tsub_tsub, tsub_tsub_cancel_of_le (nat.succ_le_iff.mpr h')] }, end lemma iterate_derivative_at_1_ne_zero [char_zero R] (n ν : ℕ) (h : ν ≤ n) : diff --git a/src/ring_theory/polynomial/content.lean b/src/ring_theory/polynomial/content.lean index 38f0da31f920b..7b0fb45508cae 100644 --- a/src/ring_theory/polynomial/content.lean +++ b/src/ring_theory/polynomial/content.lean @@ -409,7 +409,7 @@ begin refine ⟨_, rfl, ⟨dvd_cancel_leads_of_dvd_of_dvd pr ps, dvd_cancel_leads_of_dvd_of_dvd qr qs⟩, λ rcs, rs _⟩, rw ← rprim.dvd_prim_part_iff_dvd s0, - rw [cancel_leads, nat.sub_eq_zero_of_le hs, pow_zero, mul_one] at rcs, + rw [cancel_leads, tsub_eq_zero_iff_le.mpr hs, pow_zero, mul_one] at rcs, have h := dvd_add rcs (dvd.intro_left _ rfl), have hC0 := rprim.ne_zero, rw [ne.def, ← leading_coeff_eq_zero, ← C_eq_zero] at hC0, diff --git a/src/ring_theory/polynomial/pochhammer.lean b/src/ring_theory/polynomial/pochhammer.lean index 44f91fc803fff..52e1d675835e0 100644 --- a/src/ring_theory/polynomial/pochhammer.lean +++ b/src/ring_theory/polynomial/pochhammer.lean @@ -117,7 +117,7 @@ lemma pochhammer_nat_eq_desc_factorial (a b : ℕ) : begin cases b, { rw [nat.desc_factorial_zero, pochhammer_zero, polynomial.eval_one] }, - rw [nat.add_succ, nat.succ_sub_succ, nat.sub_zero], + rw [nat.add_succ, nat.succ_sub_succ, tsub_zero], cases a, { rw [pochhammer_ne_zero_eval_zero _ b.succ_ne_zero, zero_add, nat.desc_factorial_of_lt b.lt_succ_self] }, diff --git a/src/ring_theory/polynomial/rational_root.lean b/src/ring_theory/polynomial/rational_root.lean index 40273257e2ec3..8da6b38c335cf 100644 --- a/src/ring_theory/polynomial/rational_root.lean +++ b/src/ring_theory/polynomial/rational_root.lean @@ -67,7 +67,7 @@ theorem num_dvd_of_is_root {p : polynomial A} {r : K} (hr : aeval r p = 0) : num A r ∣ p.coeff 0 := begin suffices : num A r ∣ (scale_roots p (denom A r)).coeff 0, - { simp only [coeff_scale_roots, nat.sub_zero] at this, + { simp only [coeff_scale_roots, tsub_zero] at this, haveI := classical.prop_decidable, by_cases hr : num A r = 0, { obtain ⟨u, hu⟩ := (is_unit_denom_of_num_eq_zero hr).pow p.nat_degree, diff --git a/src/ring_theory/polynomial/scale_roots.lean b/src/ring_theory/polynomial/scale_roots.lean index c795577757d6e..8b74c8e1e0e32 100644 --- a/src/ring_theory/polynomial/scale_roots.lean +++ b/src/ring_theory/polynomial/scale_roots.lean @@ -32,7 +32,7 @@ by simp [scale_roots, coeff_monomial] {contextual := tt} lemma coeff_scale_roots_nat_degree (p : polynomial R) (s : R) : (scale_roots p s).coeff p.nat_degree = p.leading_coeff := -by rw [leading_coeff, coeff_scale_roots, nat.sub_self, pow_zero, mul_one] +by rw [leading_coeff, coeff_scale_roots, tsub_self, pow_zero, mul_one] @[simp] lemma zero_scale_roots (s : R) : scale_roots 0 s = 0 := by { ext, simp } @@ -99,7 +99,7 @@ calc eval₂ f (f s * r) (scale_roots p s) = (λ i hi, by simp_rw [f.map_mul, f.map_pow, pow_add, mul_pow, mul_assoc]) ... = p.support.sum (λ (i : ℕ), f s ^ p.nat_degree * (f (p.coeff i) * r ^ i)) : finset.sum_congr rfl - (λ i hi, by { rw [mul_assoc, mul_left_comm, nat.sub_add_cancel], + (λ i hi, by { rw [mul_assoc, mul_left_comm, tsub_add_cancel_of_le], exact le_nat_degree_of_ne_zero (polynomial.mem_support_iff.mp hi) }) ... = f s ^ p.nat_degree * p.support.sum (λ (i : ℕ), (f (p.coeff i) * r ^ i)) : finset.mul_sum.symm ... = f s ^ p.nat_degree * eval₂ f r p : by { simp [eval₂_eq_sum, sum_def] } diff --git a/src/ring_theory/polynomial/vieta.lean b/src/ring_theory/polynomial/vieta.lean index 9651940d1495e..133254a914028 100644 --- a/src/ring_theory/polynomial/vieta.lean +++ b/src/ring_theory/polynomial/vieta.lean @@ -86,16 +86,16 @@ begin begin refine finset.ext (λ a, ⟨λ ha, _, λ ha, _ ⟩), rw mem_singleton, - have hσ := (nat.sub_eq_iff_eq_add (mem_range_succ_iff.mp + have hσ := (tsub_eq_iff_eq_add_of_le (mem_range_succ_iff.mp (mem_filter.mp ha).1)).mp ((mem_filter.mp ha).2).symm, symmetry, - rwa [(nat.sub_eq_iff_eq_add h), add_comm], + rwa [(tsub_eq_iff_eq_add_of_le h), add_comm], rw mem_filter, have haσ : a ∈ range (card σ + 1) := by { rw mem_singleton.mp ha, exact mem_range_succ_iff.mpr (@tsub_le_self _ _ _ _ _ k) }, refine ⟨haσ, eq.symm _⟩, - rw nat.sub_eq_iff_eq_add (mem_range_succ_iff.mp haσ), - have hσ := (nat.sub_eq_iff_eq_add h).mp (mem_singleton.mp ha).symm, + rw tsub_eq_iff_eq_add_of_le (mem_range_succ_iff.mp haσ), + have hσ := (tsub_eq_iff_eq_add_of_le h).mp (mem_singleton.mp ha).symm, rwa add_comm, end, simp only [prod_X_add_C_eval, ← esymm_to_sum, finset_sum_coeff, coeff_C_mul_X, sum_ite, hk, diff --git a/src/ring_theory/power_series/basic.lean b/src/ring_theory/power_series/basic.lean index 30c6008322dcf..2aaf4c4e504f9 100644 --- a/src/ring_theory/power_series/basic.lean +++ b/src/ring_theory/power_series/basic.lean @@ -541,7 +541,7 @@ begin { rintros ⟨i,j⟩ hij hne, rw finsupp.mem_antidiagonal at hij, rw coeff_X_pow, split_ifs with hi, { exfalso, apply hne, rw [← hij, ← hi, prod.mk.inj_iff], refine ⟨rfl, _⟩, - ext t, simp only [nat.add_sub_cancel_left, finsupp.add_apply, finsupp.tsub_apply] }, + ext t, simp only [add_tsub_cancel_left, finsupp.add_apply, finsupp.tsub_apply] }, { exact zero_mul _ } }, { intro hni, exfalso, apply hni, rwa [finsupp.mem_antidiagonal, add_comm] } }, { rw [h, coeff_mul, finset.sum_eq_zero], @@ -552,7 +552,7 @@ begin { exact zero_mul _ } }, { classical, contrapose! H, ext t, by_cases hst : s = t, - { subst t, simpa using nat.sub_add_cancel H }, + { subst t, simpa using tsub_add_cancel_of_le H }, { simp [finsupp.single_apply, hst] } } } } end diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean index aec50dc0dd9a9..666bec8ac669a 100644 --- a/src/ring_theory/roots_of_unity.lean +++ b/src/ring_theory/roots_of_unity.lean @@ -166,7 +166,7 @@ begin all_goals { rcases x with ⟨x, hx⟩, rw [mem_nth_roots k.pos] at hx, simp only [subtype.coe_mk, ← pow_succ, ← pow_succ', hx, - nat.sub_add_cancel (show 1 ≤ (k : ℕ), from k.one_le)] }, + tsub_add_cancel_of_le (show 1 ≤ (k : ℕ), from k.one_le)] }, { show (_ : units R) ^ (k : ℕ) = 1, simp only [units.ext_iff, hx, units.coe_mk, units.coe_one, subtype.coe_mk, units.coe_pow] } end @@ -269,7 +269,7 @@ by { rintro ⟨i, rfl⟩, simp only [pow_mul, h.pow_eq_one, one_pow, pnat.mul_co lemma is_unit (h : is_primitive_root ζ k) (h0 : 0 < k) : is_unit ζ := begin apply is_unit_of_mul_eq_one ζ (ζ ^ (k - 1)), - rw [← pow_succ, nat.sub_add_cancel h0, h.pow_eq_one] + rw [← pow_succ, tsub_add_cancel_of_le h0.nat_succ_le, h.pow_eq_one] end lemma pow_ne_one_of_pos_of_lt (h0 : 0 < l) (hl : l < k) : ζ ^ l ≠ 1 := @@ -280,11 +280,11 @@ lemma pow_inj (h : is_primitive_root ζ k) ⦃i j : ℕ⦄ (hi : i < k) (hj : j begin wlog hij : i ≤ j, apply le_antisymm hij, - rw ← nat.sub_eq_zero_iff_le, + rw ← tsub_eq_zero_iff_le, apply nat.eq_zero_of_dvd_of_lt _ (lt_of_le_of_lt tsub_le_self hj), apply h.dvd_of_pow_eq_one, rw [← ((h.is_unit (lt_of_le_of_lt (nat.zero_le _) hi)).pow i).mul_left_inj, - ← pow_add, nat.sub_add_cancel hij, H, one_mul] + ← pow_add, tsub_add_cancel_of_le hij, H, one_mul] end lemma one : is_primitive_root (1 : M) 1 := diff --git a/src/ring_theory/witt_vector/defs.lean b/src/ring_theory/witt_vector/defs.lean index 519296c39f2a7..8c8bf30c8d265 100644 --- a/src/ring_theory/witt_vector/defs.lean +++ b/src/ring_theory/witt_vector/defs.lean @@ -200,7 +200,7 @@ begin bind₁_X_right, bind₁_C_right], rw [sub_mul, one_mul], rw [finset.sum_eq_single 0], - { simp only [inv_of_eq_inv, one_mul, inv_pow₀, nat.sub_zero, ring_hom.map_one, pow_zero], + { simp only [inv_of_eq_inv, one_mul, inv_pow₀, tsub_zero, ring_hom.map_one, pow_zero], simp only [one_pow, one_mul, X_in_terms_of_W_zero, sub_self, bind₁_X_right] }, { intros i hin hi0, rw [finset.mem_range] at hin, diff --git a/src/ring_theory/witt_vector/frobenius.lean b/src/ring_theory/witt_vector/frobenius.lean index cd5b5a9c4efa1..757e03c45f4e5 100644 --- a/src/ring_theory/witt_vector/frobenius.lean +++ b/src/ring_theory/witt_vector/frobenius.lean @@ -134,9 +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, - { 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 (le_tsub_of_add_le_right - ((le_tsub_iff_left hi.le).mp this.1))] }, + { rw [tsub_add_eq_add_tsub this.2, add_comm i j, + add_tsub_assoc_of_le (this.1.trans (nat.sub_le n i)), add_assoc, tsub_right_comm, add_comm i, + tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left 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], @@ -162,7 +162,7 @@ begin simp only [alg_hom.map_sum, alg_hom.map_sub, alg_hom.map_mul, alg_hom.map_pow, bind₁_C_right], have h1 : (↑p ^ n) * (⅟ (↑p : ℚ) ^ n) = 1 := by rw [←mul_pow, mul_inv_of_self, one_pow], rw [bind₁_X_right, function.comp_app, witt_polynomial_eq_sum_C_mul_X_pow, sum_range_succ, - sum_range_succ, nat.sub_self, nat.add_sub_cancel_left, pow_zero, pow_one, pow_one, sub_mul, + sum_range_succ, tsub_self, add_tsub_cancel_left, pow_zero, pow_one, pow_one, sub_mul, add_mul, add_mul, mul_right_comm, mul_right_comm (C (↑p ^ (n + 1))), ←C_mul, ←C_mul, pow_succ, mul_assoc ↑p (↑p ^ n), h1, mul_one, C_1, one_mul, add_comm _ (X n ^ p), add_assoc, ←add_sub, add_right_inj, frobenius_poly_aux_eq, ring_hom.map_sub, map_X, mul_sub, sub_eq_add_neg, @@ -173,7 +173,7 @@ begin rw mem_range at hi, rw [← IH i hi], clear IH, - rw [add_comm (X i ^ p), add_pow, sum_range_succ', pow_zero, nat.sub_zero, nat.choose_zero_right, + rw [add_comm (X i ^ p), add_pow, sum_range_succ', pow_zero, tsub_zero, nat.choose_zero_right, one_mul, nat.cast_one, mul_one, mul_add, add_mul, nat.succ_sub (le_of_lt hi), nat.succ_eq_add_one (n - i), pow_succ, pow_mul, add_sub_cancel, mul_sum, sum_mul], apply sum_congr rfl, diff --git a/src/ring_theory/witt_vector/is_poly.lean b/src/ring_theory/witt_vector/is_poly.lean index bdbcb46fe28d8..f4e53d386b559 100644 --- a/src/ring_theory/witt_vector/is_poly.lean +++ b/src/ring_theory/witt_vector/is_poly.lean @@ -617,7 +617,7 @@ attribute [ghost_simps] ring_hom.map_zero ring_hom.map_one ring_hom.map_mul ring_hom.map_add ring_hom.map_sub ring_hom.map_neg ring_hom.id_apply ring_hom.map_nat_cast mul_add add_mul add_zero zero_add mul_one one_mul mul_zero zero_mul - nat.succ_ne_zero nat.add_sub_cancel nat.succ_eq_add_one + nat.succ_ne_zero add_tsub_cancel_right nat.succ_eq_add_one if_true eq_self_iff_true if_false forall_true_iff forall_2_true_iff forall_3_true_iff end witt_vector diff --git a/src/ring_theory/witt_vector/structure_polynomial.lean b/src/ring_theory/witt_vector/structure_polynomial.lean index 7f1bd9976425b..8230c601f14c8 100644 --- a/src/ring_theory/witt_vector/structure_polynomial.lean +++ b/src/ring_theory/witt_vector/structure_polynomial.lean @@ -245,11 +245,11 @@ begin 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, ←add_assoc], congr' 2, rw [add_comm, ←nat.sub_eq_iff_eq_add hk] }, + { rw [← pow_add, ←add_assoc], congr' 2, rw [add_comm, ←tsub_eq_iff_eq_add_of_le 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, nat.sub_add_comm hk] }, + { rw [← pow_succ, ← tsub_add_eq_add_tsub hk] }, rw [pow_mul], -- the machine! apply dvd_sub_pow_of_dvd_sub, diff --git a/src/ring_theory/witt_vector/teichmuller.lean b/src/ring_theory/witt_vector/teichmuller.lean index 4e4092ca97324..81e9289af99cf 100644 --- a/src/ring_theory/witt_vector/teichmuller.lean +++ b/src/ring_theory/witt_vector/teichmuller.lean @@ -59,7 +59,7 @@ private lemma ghost_component_teichmuller_fun (r : R) (n : ℕ) : ghost_component n (teichmuller_fun p r) = r ^ p ^ n := begin rw [ghost_component_apply, aeval_witt_polynomial, finset.sum_eq_single 0, - pow_zero, one_mul, nat.sub_zero], + pow_zero, one_mul, tsub_zero], { refl }, { intros i hi h0, convert mul_zero _, convert zero_pow _, diff --git a/src/ring_theory/witt_vector/verschiebung.lean b/src/ring_theory/witt_vector/verschiebung.lean index b688b8271410b..d4062f4d140d2 100644 --- a/src/ring_theory/witt_vector/verschiebung.lean +++ b/src/ring_theory/witt_vector/verschiebung.lean @@ -62,7 +62,7 @@ begin mul_zero, add_zero, finset.mul_sum, finset.sum_congr rfl], rintro i -, simp only [pow_succ, mul_assoc, verschiebung_fun_coeff, if_neg (nat.succ_ne_zero i), - nat.succ_sub_succ, nat.sub_zero] + nat.succ_sub_succ, tsub_zero] end omit hp @@ -83,7 +83,7 @@ begin cases n, { simp only [verschiebung_poly, verschiebung_fun_coeff_zero, if_pos rfl, alg_hom.map_zero] }, { rw [verschiebung_poly, verschiebung_fun_coeff_succ, if_neg (n.succ_ne_zero), - aeval_X, nat.succ_eq_add_one, nat.add_sub_cancel] } + aeval_X, nat.succ_eq_add_one, add_tsub_cancel_right] } end variable (p) @@ -158,7 +158,7 @@ begin split_ifs with hn, { simp only [hn, verschiebung_poly_zero, witt_polynomial_zero, bind₁_X_right] }, { obtain ⟨n, rfl⟩ := nat.exists_eq_succ_of_ne_zero hn, - rw [nat.succ_eq_add_one, nat.add_sub_cancel, ring_hom.map_mul, + rw [nat.succ_eq_add_one, add_tsub_cancel_right, ring_hom.map_mul, ring_hom.map_nat_cast, hom_bind₁], calc _ = ghost_component (n + 1) (verschiebung $ mk p x) : _ diff --git a/src/ring_theory/witt_vector/witt_polynomial.lean b/src/ring_theory/witt_vector/witt_polynomial.lean index 58175b208c9c2..eb165aea79189 100644 --- a/src/ring_theory/witt_vector/witt_polynomial.lean +++ b/src/ring_theory/witt_vector/witt_polynomial.lean @@ -146,7 +146,7 @@ begin rw [alg_hom.map_mul, alg_hom.map_pow, expand_X, alg_hom_C, ← pow_mul, ← pow_succ], congr, rw mem_range at hk, - rw [add_comm, nat.add_sub_assoc (nat.lt_succ_iff.mp hk), ← add_comm], + rw [add_comm, add_tsub_assoc_of_le (nat.lt_succ_iff.mp hk), ← add_comm], end section p_prime @@ -277,7 +277,7 @@ by rw [X_in_terms_of_W_eq, mul_assoc, ← C_mul, ← mul_pow, inv_of_mul_self, o begin rw [witt_polynomial_eq_sum_C_mul_X_pow, alg_hom.map_sum], simp only [alg_hom.map_pow, C_pow, alg_hom.map_mul, alg_hom_C], - rw [sum_range_succ_comm, nat.sub_self, pow_zero, pow_one, bind₁_X_right, + rw [sum_range_succ_comm, tsub_self, pow_zero, pow_one, bind₁_X_right, mul_comm, ← C_pow, X_in_terms_of_W_aux], simp only [C_pow, bind₁_X_right, sub_add_cancel], end @@ -290,7 +290,7 @@ begin rw [X_in_terms_of_W_eq, alg_hom.map_mul, alg_hom.map_sub, bind₁_X_right, alg_hom_C, alg_hom.map_sum], have : W_ R n - ∑ i in range n, C (p ^ i : R) * (X i) ^ p ^ (n - i) = C (p ^ n : R) * X n, - by simp only [witt_polynomial_eq_sum_C_mul_X_pow, nat.sub_self, sum_range_succ_comm, + by simp only [witt_polynomial_eq_sum_C_mul_X_pow, tsub_self, sum_range_succ_comm, pow_one, add_sub_cancel, pow_zero], rw [sum_congr rfl, this], { -- this is really slow for some reason diff --git a/src/set_theory/game/domineering.lean b/src/set_theory/game/domineering.lean index bf6c59e05a9c5..7244547795e37 100644 --- a/src/set_theory/game/domineering.lean +++ b/src/set_theory/game/domineering.lean @@ -97,7 +97,7 @@ begin dsimp [move_left], rw finset.card_erase_of_mem, { rw finset.card_erase_of_mem, - { exact nat.sub_add_cancel (card_of_mem_left h), }, + { exact tsub_add_cancel_of_le (card_of_mem_left h), }, { exact finset.mem_of_mem_inter_left h, } }, { apply finset.mem_erase_of_ne_of_mem, { exact λ w, pred_ne_self m.2 (congr_arg prod.snd w), }, @@ -115,7 +115,7 @@ begin dsimp [move_right], rw finset.card_erase_of_mem, { rw finset.card_erase_of_mem, - { exact nat.sub_add_cancel (card_of_mem_right h), }, + { exact tsub_add_cancel_of_le (card_of_mem_right h), }, { exact finset.mem_of_mem_inter_left h, } }, { apply finset.mem_erase_of_ne_of_mem, { exact λ w, pred_ne_self m.1 (congr_arg prod.fst w), }, diff --git a/src/set_theory/ordinal_arithmetic.lean b/src/set_theory/ordinal_arithmetic.lean index 6170659ca512f..ab6ad7df3f5b4 100644 --- a/src/set_theory/ordinal_arithmetic.lean +++ b/src/set_theory/ordinal_arithmetic.lean @@ -1332,7 +1332,7 @@ not_congr nat_cast_eq_zero @[simp] theorem nat_cast_sub {m n : ℕ} : ((m - n : ℕ) : ordinal) = m - n := (_root_.le_total m n).elim - (λ h, by rw [nat.sub_eq_zero_iff_le.2 h, ordinal.sub_eq_zero_iff_le.2 (nat_cast_le.2 h)]; refl) + (λ h, by rw [tsub_eq_zero_iff_le.2 h, ordinal.sub_eq_zero_iff_le.2 (nat_cast_le.2 h)]; refl) (λ h, (add_left_cancel n).1 $ by rw [← nat.cast_add, add_tsub_cancel_of_le h, ordinal.add_sub_cancel_of_le (nat_cast_le.2 h)]) diff --git a/src/set_theory/ordinal_notation.lean b/src/set_theory/ordinal_notation.lean index 768fc2d372d69..f166883105283 100644 --- a/src/set_theory/ordinal_notation.lean +++ b/src/set_theory/ordinal_notation.lean @@ -431,9 +431,9 @@ instance sub_NF (o₁ o₂) : ∀ [NF o₁] [NF o₂], NF (o₁ - o₂) { simp [en], rwa [add_sub_add_cancel] }, { simp [en, -repr], exact (ordinal.sub_eq_zero_iff_le.2 $ le_of_lt $ oadd_lt_oadd_2 h₁ $ - lt_of_le_of_ne (nat.sub_eq_zero_iff_le.1 mn) (mt pnat.eq en)).symm } }, + lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt pnat.eq en)).symm } }, { simp [nat.succ_pnat, -nat.cast_succ], - rw [(nat.sub_eq_iff_eq_add $ le_of_lt $ nat.lt_of_sub_eq_succ mn).1 mn, + rw [(tsub_eq_iff_eq_add_of_le $ le_of_lt $ nat.lt_of_sub_eq_succ mn).1 mn, add_comm, nat.cast_add, ordinal.mul_add, add_assoc, add_sub_add_cancel], refine (ordinal.sub_eq_of_add_eq $ add_absorp h₂.snd'.repr_lt $ le_trans _ (le_add_right _ _)).symm, diff --git a/src/tactic/group.lean b/src/tactic/group.lean index 61fb38f9fba9a..bc74780c84d5a 100644 --- a/src/tactic/group.lean +++ b/src/tactic/group.lean @@ -54,7 +54,7 @@ meta def aux_group₁ (locat : loc) : tactic unit := expr ``(add_neg_self), expr ``(neg_add_self), expr ``(neg_neg), - expr ``(nat.sub_self), + expr ``(tsub_self), expr ``(int.coe_nat_add), expr ``(int.coe_nat_mul), expr ``(int.coe_nat_zero), diff --git a/src/tactic/monotonicity/lemmas.lean b/src/tactic/monotonicity/lemmas.lean index f66d40ea4a0fb..5902c2db98b67 100644 --- a/src/tactic/monotonicity/lemmas.lean +++ b/src/tactic/monotonicity/lemmas.lean @@ -48,7 +48,7 @@ begin have : z ≤ y, { transitivity, assumption, apply le_of_lt h, }, apply @nat.lt_of_add_lt_add_left z, - rw [nat.add_sub_of_le,nat.add_sub_of_le]; + rw [add_tsub_cancel_of_le,add_tsub_cancel_of_le]; solve_by_elim end @@ -61,9 +61,9 @@ begin have h'' : y ≤ z, { transitivity, apply le_of_lt h, assumption }, apply @nat.lt_of_add_lt_add_right _ x, - rw [nat.sub_add_cancel h'], + rw [tsub_add_cancel_of_le h'], apply @lt_of_le_of_lt _ _ _ (z - y + y), - rw [nat.sub_add_cancel h''], + rw [tsub_add_cancel_of_le h''], apply nat.add_lt_add_left h end diff --git a/src/tactic/norm_num.lean b/src/tactic/norm_num.lean index fd3bf7b82b1ab..4e570f106fce3 100644 --- a/src/tactic/norm_num.lean +++ b/src/tactic/norm_num.lean @@ -955,9 +955,9 @@ match match_sign b with end theorem sub_nat_pos (a b c : ℕ) (h : b + c = a) : a - b = c := -h ▸ nat.add_sub_cancel_left _ _ +h ▸ add_tsub_cancel_left _ _ theorem sub_nat_neg (a b c : ℕ) (h : a + c = b) : a - b = 0 := -nat.sub_eq_zero_of_le $ h ▸ nat.le_add_right _ _ +tsub_eq_zero_iff_le.mpr $ h ▸ nat.le_add_right _ _ /-- Given `a : nat`,`b : nat` natural numerals, returns `(c, ⊢ a - b = c)`. -/ meta def prove_sub_nat (ic : instance_cache) (a b : expr) : tactic (expr × expr) := diff --git a/src/tactic/omega/coeffs.lean b/src/tactic/omega/coeffs.lean index a0f988a14db2e..d4a5f10aab454 100644 --- a/src/tactic/omega/coeffs.lean +++ b/src/tactic/omega/coeffs.lean @@ -44,12 +44,11 @@ val_between v as 0 as.length lemma val_between_eq_of_le {as : list int} {l : nat} : ∀ m, as.length ≤ l + m → val_between v as l m = val_between v as l (as.length - l) -| 0 h1 := - begin rw (nat.sub_eq_zero_iff_le.elim_right _), apply h1 end +| 0 h1 := by { rw add_zero at h1, rw tsub_eq_zero_iff_le.mpr h1 } | (m+1) h1 := begin rw le_iff_eq_or_lt at h1, cases h1, - { rw [h1, add_comm l, nat.add_sub_cancel] }, + { rw [h1, add_comm l, add_tsub_cancel_right] }, have h2 : list.length as ≤ l + m, { rw ← nat.lt_succ_iff, apply h1 }, simpa [ get_eq_default_of_le _ h2, zero_mul, add_zero, @@ -229,19 +228,17 @@ lemma val_except_add_eq (n : nat) {as : list int} : (val_except n v as) + ((get n as) * (v n)) = val v as := begin unfold val_except, unfold val, - by_cases h1 : n + 1 ≤ as.length, + cases le_total (n + 1) as.length with h1 h1, { have h4 := @val_between_add_val_between v as 0 (n+1) (as.length - (n+1)), have h5 : n + 1 + (as.length - (n + 1)) = as.length, - { rw [add_comm, nat.sub_add_cancel h1] }, + { rw [add_comm, tsub_add_cancel_of_le h1] }, rw h5 at h4, apply eq.trans _ h4, simp only [val_between, zero_add], ring }, - have h2 : (list.length as - (n + 1)) = 0, - { apply nat.sub_eq_zero_of_le - (le_trans (not_lt.1 h1) (nat.le_add_right _ _)) }, + have h2 : list.length as - (n + 1) = 0, + { exact tsub_eq_zero_iff_le.mpr h1 }, have h3 : val_between v as 0 (list.length as) = val_between v as 0 (n + 1), - { simpa only [val] using @val_eq_of_le v as (n+1) - (le_trans (not_lt.1 h1) (nat.le_add_right _ _)) }, + { simpa only [val] using @val_eq_of_le v as (n+1) h1 }, simp only [add_zero, val_between, zero_add, h2, h3] end diff --git a/src/tactic/omega/nat/sub_elim.lean b/src/tactic/omega/nat/sub_elim.lean index 6922491a6d38c..5d0569eb711c7 100644 --- a/src/tactic/omega/nat/sub_elim.lean +++ b/src/tactic/omega/nat/sub_elim.lean @@ -97,11 +97,10 @@ begin intro h1, simp only [preform.holds, is_diff, if_pos (eq.refl 1), preterm.val_add, preterm.val_var, preterm.val_const], - by_cases h2 : t.val v ≤ s.val v, - { right, refine ⟨h2,_⟩, - rw [h1, one_mul, nat.sub_eq_zero_iff_le], exact h2 }, - { left, rw [h1, one_mul, add_comm, nat.sub_add_cancel _], - rw not_le at h2, apply le_of_lt h2 } + cases le_total (t.val v) (s.val v) with h2 h2, + { right, refine ⟨h2, _⟩, + rw [h1, one_mul, tsub_eq_zero_iff_le], exact h2 }, + { left, rw [h1, one_mul, add_comm, tsub_add_cancel_of_le h2] } end /-- Helper function for sub_elim -/ diff --git a/src/tactic/suggest.lean b/src/tactic/suggest.lean index e7ca4264eabad..4ac72a6d1b73d 100644 --- a/src/tactic/suggest.lean +++ b/src/tactic/suggest.lean @@ -457,7 +457,7 @@ of `library_search`. Typical usage is: ```lean example (n m k : ℕ) : n * (m - k) = n * m - n * k := -by library_search -- Try this: exact nat.mul_sub_left_distrib n m k +by library_search -- Try this: exact mul_tsub n m k ``` `library_search using h₁ h₂` will only show solutions diff --git a/src/testing/slim_check/sampleable.lean b/src/testing/slim_check/sampleable.lean index 8439bf673176b..80495ac90cdc9 100644 --- a/src/testing/slim_check/sampleable.lean +++ b/src/testing/slim_check/sampleable.lean @@ -292,7 +292,7 @@ sampleable.lift ℕ fin.of_nat subtype.val $ instance pnat.sampleable : sampleable ℕ+ := sampleable.lift ℕ nat.succ_pnat pnat.nat_pred $ λ a, -by unfold_wf; simp only [pnat.nat_pred, succ_pnat, pnat.mk_coe, nat.sub_zero, succ_sub_succ_eq_sub] +by unfold_wf; simp only [pnat.nat_pred, succ_pnat, pnat.mk_coe, tsub_zero, succ_sub_succ_eq_sub] /-- Redefine `sizeof` for `int` to make it easier to use with `nat` -/ def int.has_sizeof : has_sizeof ℤ := ⟨ int.nat_abs ⟩ @@ -374,7 +374,7 @@ begin { rw [← int.coe_nat_le, ← int.abs_eq_nat_abs, ← int.abs_eq_nat_abs], apply int.abs_div_le_abs }, { change _ - 1 ≤ y-1, - apply nat.sub_le_sub_right, + apply tsub_le_tsub_right, apply nat.div_le_of_le_mul, suffices : 1 * y ≤ x.nat_abs.gcd y * y, { simpa }, apply nat.mul_le_mul_right, diff --git a/test/library_search/basic.lean b/test/library_search/basic.lean index 4f5e915a2d7d1..1086e7a991ba3 100644 --- a/test/library_search/basic.lean +++ b/test/library_search/basic.lean @@ -44,10 +44,10 @@ example (a b : ℕ) : a + b = b + a := by library_search -- says: `exact add_comm a b` example (n m k : ℕ) : n * (m - k) = n * m - n * k := -by library_search -- says: `exact nat.mul_sub_left_distrib n m k` +by library_search -- says: `exact mul_tsub n m k` example (n m k : ℕ) : n * m - n * k = n * (m - k) := -by library_search -- says: `exact eq.symm (nat.mul_sub_left_distrib n m k)` +by library_search -- says: `exact eq.symm (mul_tsub n m k)` example {α : Type} (x y : α) : x = y ↔ y = x := by library_search -- says: `exact eq_comm`