refactor(data/nat/basic): remove sub lemmas (#9544)

* Remove the nat sub lemmas that are special cases of lemmas in `algebra/order/sub`
* This PR does 90% of the work, some lemmas require a bit more work (which will be done in a future PR)
* Protect `ordinal.add_sub_cancel_of_le`
* Most fixes in other files were abuses of the definitional equality of `n < m` and `nat.succ n \le m`.
* [This](https://github.com/leanprover-community/mathlib/blob/7a5d15a955a92a90e1d398b2281916b9c41270b2/src/data/nat/basic.lean#L498-L611) gives the list of renamings.
* The regex to find 90+% of the occurrences of removed lemmas. Some lemmas were not protected, so might not be found this way.
```
nat.(le_sub_add|add_sub_cancel'|sub_add_sub_cancel|sub_cancel|sub_sub_sub_cancel_right|sub_add_eq_add_sub|sub_sub_assoc|lt_of_sub_pos|lt_of_sub_lt_sub_right|lt_of_sub_lt_sub_left|sub_lt_self|le_sub_right_of_add_le|le_sub_left_of_add_le|lt_sub_right_of_add_lt|lt_sub_left_of_add_lt|add_lt_of_lt_sub_right|add_lt_of_lt_sub_left|le_add_of_sub_le_right|le_add_of_sub_le_left|lt_add_of_sub_lt_right|lt_add_of_sub_lt_left|sub_le_left_of_le_add|sub_le_right_of_le_add|sub_lt_left_iff_lt_add|le_sub_left_iff_add_le|le_sub_right_iff_add_le|lt_sub_left_iff_add_lt|lt_sub_right_iff_add_lt|sub_lt_right_iff_lt_add|sub_le_sub_left_iff|sub_lt_sub_right_iff|sub_lt_sub_left_iff|sub_le_iff|sub_lt_iff)[^_]
```



Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>

archive/100-theorems-list/73_ascending_descending_sequences.lean

@@ -150,10 +150,10 @@ begin
     refine ⟨_, _⟩,
     -- Need to get `a_i ≤ r`, here phrased as: there is some `a < r` with `a+1 = a_i`.
     { refine ⟨(ab i).1 - 1, _, nat.succ_pred_eq_of_pos z.1⟩,
-      rw nat.sub_lt_right_iff_lt_add z.1,
+      rw sub_lt_iff_right z.1,
       apply nat.lt_succ_of_le q.1 },
     { refine ⟨(ab i).2 - 1, _, nat.succ_pred_eq_of_pos z.2⟩,
-      rw nat.sub_lt_right_iff_lt_add z.2,
+      rw sub_lt_iff_right z.2,
       apply nat.lt_succ_of_le q.2 } },
   -- To get our contradiction, it suffices to prove `n ≤ r * s`
   apply not_le_of_lt hn,

archive/imo/imo1977_q6.lean

@@ -24,7 +24,7 @@ begin
     { intros, exact nat.zero_le _ },
     { intros n hk,
       apply nat.succ_le_of_lt,
-      calc k ≤ f (f (n - 1)) : h_ind _ (h_ind (n - 1) (nat.le_sub_right_of_add_le hk))
+      calc k ≤ f (f (n - 1)) : h_ind _ (h_ind (n - 1) (le_sub_of_add_le_right' hk))
          ... < f n           : nat.sub_add_cancel
         (le_trans (nat.succ_le_succ (nat.zero_le _)) hk) ▸ h _ } },
   have hf : ∀ n, n ≤ f n := λ n, h' n n rfl.le,

archive/imo/imo1998_q2.lean

@@ -174,7 +174,7 @@ begin
     { suffices : p.judge₁ = p.judge₂, { simp [this], }, finish, }, },
   have hst' : (s \ t).card = 2*z + 1, { rw [hst, finset.diag_card, ← hJ], refl, },
   rw [finset.filter_and, ← finset.sdiff_sdiff_self_left s t, finset.card_sdiff],
-  { rw hst', rw add_assoc at hs, apply nat.le_sub_right_of_add_le hs, },
+  { rw hst', rw add_assoc at hs, apply le_sub_of_add_le_right' hs, },
   { apply finset.sdiff_subset, },
 end
 

archive/oxford_invariants/2021summer/week3_p1.lean

@@ -119,7 +119,7 @@ begin
           norm_cast,
           rw nat.cast_sub (nat.div_le_of_le_mul _),
           rw [←mul_assoc, nat.mul_div_cancel' ha, add_mul],
-          exact (nat.sub_le_self _ _).trans (nat.le_add_right _ _),
+          exact sub_le_self'.trans (nat.le_add_right _ _),
         end
     ... = a (n + 2) / a (n + 1) * b + (a 0 * a (n + 2)) / (a (n + 1) * a (n + 2))
         : by rw [add_div, add_mul, sub_div, mul_div_right_comm, add_sub_sub_cancel,

counterexamples/canonically_ordered_comm_semiring_two_mul.lean

@@ -233,7 +233,7 @@ begin
       { rw [ne.def, prod.mk.inj_iff, not_and_distrib],
         exact or.inl (ne_of_gt (nat.sub_pos_of_lt h)) },
       { congr,
-        { exact (nat.add_sub_cancel' h.le).symm },
+        { exact (add_sub_cancel_of_le h.le).symm },
         { change b2 = a2 + (b2 + a2),
           rw [add_comm b2, ← add_assoc, add_self_zmod_2, zero_add] } } } },
   { rcases h with ⟨⟨⟨c, c2⟩, hc⟩, abc⟩,

src/algebra/big_operators/basic.lean

@@ -932,7 +932,7 @@ begin
   refine sum_range_induction _ _ (nat.sub_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₂, nat.add_sub_cancel' h₁],
+  rw [←nat.sub_add_comm h₂, add_sub_cancel_of_le h₁],
 end
 
 @[simp] lemma prod_const (b : β) : (∏ x in s, b) = b ^ s.card :=

src/algebra/big_operators/intervals.lean

@@ -146,7 +146,7 @@ lemma sum_range_id_mul_two (n : ℕ) :
 calc (∑ i in range n, i) * 2 = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i)) :
   by rw [sum_range_reflect (λ i, i) n, mul_two]
 ... = ∑ i in range n, (i + (n - 1 - i)) : sum_add_distrib.symm
-... = ∑ i in range n, (n - 1) : sum_congr rfl $ λ i hi, nat.add_sub_cancel' $
+... = ∑ i in range n, (n - 1) : sum_congr rfl $ λ i hi, add_sub_cancel_of_le $
   nat.le_pred_of_lt $ mem_range.1 hi
 ... = n * (n - 1) : by rw [sum_const, card_range, nat.nsmul_eq_mul]
 

src/algebra/geom_sum.lean

@@ -82,7 +82,7 @@ begin
   rw [mem_range, nat.lt_iff_add_one_le] at j_in,
   congr,
   apply nat.sub_sub_self,
-  exact nat.le_sub_right_of_add_le j_in
+  exact le_sub_of_add_le_right' j_in
 end
 
 @[simp] theorem geom_sum₂_with_one [semiring α] (x : α) (n : ℕ) :
@@ -123,7 +123,7 @@ theorem geom_sum₂_self {α : Type*} [comm_ring α] (x : α) (n : ℕ) :
 calc  ∑ i in finset.range n, x ^ i * x ^ (n - 1 - i)
     = ∑ i in finset.range n, x ^ (i + (n - 1 - i)) : by simp_rw [← pow_add]
 ... = ∑ i in finset.range n, x ^ (n - 1) : finset.sum_congr rfl
-  (λ i hi, congr_arg _ $ nat.add_sub_cancel' $ nat.le_pred_of_lt $ finset.mem_range.1 hi)
+  (λ i hi, congr_arg _ $ add_sub_cancel_of_le $ nat.le_pred_of_lt $ finset.mem_range.1 hi)
 ... = (finset.range n).card • (x ^ (n - 1)) : finset.sum_const _
 ... = n * x ^ (n - 1) : by rw [finset.card_range, nsmul_eq_mul]
 
@@ -219,7 +219,7 @@ begin
       rw ← pow_add,
       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) := nat.sub_add_sub_cancel hmn j_in,
+      have h' : n - m + (m - (1 + j)) = n - (1 + j) := sub_add_sub_cancel'' hmn j_in,
       rw [nat.sub_sub m, h', nat.sub_sub] },
   rw this,
   simp_rw pow_mul_comm y (n-m) _,
@@ -239,7 +239,7 @@ begin
   suffices : n - 1 - i + 1 = n - i, { rw this },
   cases n,
   { exact absurd (list.mem_range.mp hi) i.not_lt_zero },
-  { rw [nat.sub_add_eq_add_sub (nat.le_pred_of_lt (list.mem_range.mp hi)),
+  { rw [sub_add_eq_add_sub' (nat.le_pred_of_lt (list.mem_range.mp hi)),
         nat.sub_add_cancel (nat.succ_le_iff.mpr n.succ_pos)] },
 end
 
@@ -346,7 +346,7 @@ begin
   { rw [sum_range_zero, zero_mul],
     exact nat.zero_le _ },
   rw mul_comm,
-  exact (nat.pred_mul_geom_sum_le a b n).trans (nat.sub_le_self _ _),
+  exact (nat.pred_mul_geom_sum_le a b n).trans sub_le_self',
 end
 
 lemma nat.geom_sum_Ico_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
@@ -365,7 +365,7 @@ begin
         end
     ... ≤ a * b/(b - 1) : nat.geom_sum_le hb a _
     ... = (a * 1 + a * (b - 1))/(b - 1)
-        : by rw [←mul_add, nat.add_sub_cancel' (one_le_two.trans hb)]
+        : by rw [←mul_add, add_sub_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]
 end

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), nat.sub_lt_left_iff_lt_add],
+      rw [add_comm, ← nat.add_sub_assoc (not_lt.mp h), sub_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] }
@@ -93,7 +93,7 @@ lemma eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : fin E.order → α}
     congr' with k,
     exact have wf : n - E.order + k < n :=
       begin
-        rw [add_comm, ← nat.add_sub_assoc (not_lt.mp h'), nat.sub_lt_left_iff_lt_add],
+        rw [add_comm, ← nat.add_sub_assoc (not_lt.mp h'), sub_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] }

src/algebra/pointwise.lean

@@ -818,7 +818,7 @@ begin
     replace key : ∀ k : ℕ, f (n + k) = f (n + k + 1) ∧ f (n + k) = f n :=
     λ k, nat.rec ⟨hn2, rfl⟩ (λ k ih, ⟨h3 _ ih.1, ih.1.symm.trans ih.2⟩) k,
     replace key : ∀ k : ℕ, n ≤ k → f k = f n :=
-    λ k hk, (congr_arg f (nat.add_sub_cancel' hk)).symm.trans (key (k - n)).2,
+    λ k hk, (congr_arg f (add_sub_cancel_of_le hk)).symm.trans (key (k - n)).2,
     exact λ k hk, (key k (hn1.trans hk)).trans (key B hn1).symm },
 end
 

src/analysis/asymptotics/asymptotics.lean

@@ -1302,7 +1302,7 @@ theorem is_o_pow_pow {m n : ℕ} (h : m < n) :
   is_o (λ(x : 𝕜), x^n) (λx, x^m) (𝓝 0) :=
 begin
   let p := n - m,
-  have nmp : n = m + p := (nat.add_sub_cancel' (le_of_lt h)).symm,
+  have nmp : n = m + p := (add_sub_cancel_of_le (le_of_lt h)).symm,
   have : (λ(x : 𝕜), x^m) = (λx, x^m * 1), by simp only [mul_one],
   simp only [this, pow_add, nmp],
   refine is_O.mul_is_o (is_O_refl _ _) ((is_o_one_iff _).2 _),

src/combinatorics/composition.lean

@@ -302,7 +302,7 @@ end
 def inv_embedding (j : fin n) : fin (c.blocks_fun (c.index j)) :=
 ⟨j - c.size_up_to (c.index j),
 begin
-  rw [nat.sub_lt_right_iff_lt_add, add_comm, ← size_up_to_succ'],
+  rw [sub_lt_iff_right, add_comm, ← size_up_to_succ'],
   { exact lt_size_up_to_index_succ _ _ },
   { exact size_up_to_index_le _ _ }
 end⟩
@@ -314,7 +314,7 @@ lemma embedding_comp_inv (j : fin n) :
   c.embedding (c.index j) (c.inv_embedding j) = j :=
 begin
   rw fin.ext_iff,
-  apply nat.add_sub_cancel' (c.size_up_to_index_le j),
+  apply add_sub_cancel_of_le (c.size_up_to_index_le j),
 end
 
 lemma mem_range_embedding_iff {j : fin n} {i : fin c.length} :
@@ -331,11 +331,11 @@ begin
   { assume h,
     apply set.mem_range.2,
     refine ⟨⟨j - c.size_up_to i, _⟩, _⟩,
-    { rw [nat.sub_lt_left_iff_lt_add, ← size_up_to_succ'],
+    { rw [sub_lt_iff_left, ← size_up_to_succ'],
       { exact h.2 },
       { exact h.1 } },
     { rw fin.ext_iff,
-      exact nat.add_sub_cancel' h.1 } }
+      exact add_sub_cancel_of_le h.1 } }
 end
 
 /-- The embeddings of different blocks of a composition are disjoint. -/
@@ -599,7 +599,7 @@ begin
   induction ns with n ns IH; intros l h; simp at h ⊢,
   have := le_trans (nat.le_add_right _ _) h,
   rw IH, {simp [this]},
-  rwa [length_drop, nat.le_sub_left_iff_add_le this]
+  rwa [length_drop, le_sub_iff_left this]
 end
 
 /-- When one splits a list along a composition `c`, the lengths of the sublists thus created are
@@ -755,7 +755,7 @@ lemma length_lt_card_boundaries : c.length < c.boundaries.card :=
 by { rw c.card_boundaries_eq_succ_length, exact lt_add_one _ }
 
 lemma lt_length (i : fin c.length) : (i : ℕ) + 1 < c.boundaries.card :=
-nat.add_lt_of_lt_sub_right i.2
+lt_sub_iff_right.mp i.2
 
 lemma lt_length' (i : fin c.length) : (i : ℕ) < c.boundaries.card :=
 lt_of_le_of_lt (nat.le_succ i) (c.lt_length i)
@@ -783,7 +783,7 @@ lemma blocks_fun_pos (i : fin c.length) : 0 < c.blocks_fun i :=
 begin
   have : (⟨i, c.lt_length' i⟩ : fin c.boundaries.card) < ⟨i + 1, c.lt_length i⟩ :=
     nat.lt_succ_self _,
-  exact nat.lt_sub_left_of_add_lt ((c.boundaries.order_emb_of_fin rfl).strict_mono this)
+  exact lt_sub_iff_left.mpr ((c.boundaries.order_emb_of_fin rfl).strict_mono this)
 end
 
 /-- List of the sizes of the blocks in a `composition_as_set`. -/
@@ -803,7 +803,7 @@ begin
   have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length, nat.sub_le]),
   rw [sum_take_succ _ _ A, IH B],
   simp only [blocks, blocks_fun, nth_le_of_fn'],
-  apply nat.add_sub_cancel',
+  apply add_sub_cancel_of_le,
   simp
 end
 

src/combinatorics/derangements/exponential.lean

@@ -44,7 +44,7 @@ begin
   refine finset.sum_congr (refl _) _,
   intros k hk,
   have h_le : k ≤ n := finset.mem_range_succ_iff.mp hk,
-  rw [nat.asc_factorial_eq_div, nat.add_sub_cancel' h_le],
+  rw [nat.asc_factorial_eq_div, add_sub_cancel_of_le h_le],
   push_cast [nat.factorial_dvd_factorial h_le],
   field_simp [nat.factorial_ne_zero],
   ring,

src/combinatorics/derangements/finite.lean

@@ -109,6 +109,6 @@ begin
   -- show that (n + 1) * (-1)^x * asc_fac x (n - x) = (-1)^x * asc_fac x (n.succ - x)
   intros x hx,
   have h_le : x ≤ n := finset.mem_range_succ_iff.mp hx,
-  rw [nat.succ_sub h_le, nat.asc_factorial_succ, nat.add_sub_cancel' h_le,
+  rw [nat.succ_sub h_le, nat.asc_factorial_succ, add_sub_cancel_of_le h_le,
     int.coe_nat_mul, int.coe_nat_succ, mul_left_comm],
 end

src/computability/DFA.lean

@@ -70,7 +70,7 @@ begin
   { rw [list.take_append_drop, list.take_append_drop] },
 
   { simp only [list.length_drop, list.length_take],
-    rw [min_eq_left (hm.le.trans hlen), min_eq_left hle, nat.add_sub_cancel' hle],
+    rw [min_eq_left (hm.le.trans hlen), min_eq_left hle, add_sub_cancel_of_le hle],
     exact hm.le },
 
   { intro h,

src/computability/turing_machine.lean

@@ -79,7 +79,7 @@ theorem blank_extends.below_of_le {Γ} [inhabited Γ] {l l₁ l₂ : list Γ} :
 begin
   rintro ⟨i, rfl⟩ ⟨j, rfl⟩ h, use j - i,
   simp only [list.length_append, add_le_add_iff_left, list.length_repeat] at h,
-  simp only [← list.repeat_add, nat.add_sub_cancel' h, list.append_assoc],
+  simp only [← list.repeat_add, add_sub_cancel_of_le h, list.append_assoc],
 end
 
 /-- Any two extensions by blank `l₁,l₂` of `l` have a common join (which can be taken to be the

src/data/complex/exponential.lean

@@ -178,7 +178,7 @@ by rw [sum_sigma', sum_sigma']; exact sum_bij
 (λ a ha, have h₁ : a.1 < n := mem_range.1 (mem_sigma.1 ha).1,
   have h₂ : a.2 < nat.succ a.1 := mem_range.1 (mem_sigma.1 ha).2,
     mem_sigma.2 ⟨mem_range.2 (lt_of_lt_of_le h₂ h₁),
-    mem_range.2 ((nat.sub_lt_sub_right_iff (nat.le_of_lt_succ h₂)).2 h₁)⟩)
+    mem_range.2 ((sub_lt_sub_iff_right' (nat.le_of_lt_succ h₂)).2 h₁)⟩)
 (λ _ _, rfl)
 (λ ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ha hb h,
   have ha : a₁ < n ∧ a₂ ≤ a₁ :=
@@ -193,7 +193,7 @@ by rw [sum_sigma', sum_sigma']; exact sum_bij
 (λ ⟨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 (nat.lt_sub_right_iff_add_lt.1 ha.2),
+  ⟨⟨a₂ + a₁, a₁⟩, ⟨mem_sigma.2 ⟨mem_range.2 (lt_sub_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⟩⟩⟩)
 
@@ -266,7 +266,7 @@ have hsumlesum : ∑ i in range (max N M + 1), abv (a i) *
     ∑ i in range (max N M + 1), abv (a i) * (ε / (2 * P)),
   from sum_le_sum (λ m hmJ, mul_le_mul_of_nonneg_left
     (le_of_lt (hN (K - m) K
-      (nat.le_sub_left_of_add_le (le_trans
+      (le_sub_of_add_le_left' (le_trans
         (by rw two_mul; exact add_le_add (le_of_lt (mem_range.1 hmJ))
           (le_trans (le_max_left _ _) (le_of_lt (lt_add_one _)))) hK))
       (le_of_lt hKN))) (abv_nonneg abv _)),
@@ -1202,15 +1202,15 @@ lemma sum_div_factorial_le {α : Type*} [linear_ordered_field α] (n j : ℕ) (h
 calc ∑ m in filter (λ k, n ≤ k) (range j), (1 / m! : α)
     = ∑ m in range (j - n), 1 / (m + n)! :
   sum_bij (λ m _, m - n)
-    (λ m hm, mem_range.2 $ (nat.sub_lt_sub_right_iff (by simp at hm; tauto)).2
+    (λ m hm, mem_range.2 $ (sub_lt_sub_iff_right' (by simp at hm; tauto)).2
       (by simp at hm; tauto))
     (λ m hm, by rw nat.sub_add_cancel; 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,
               add_left_inj, eq_comm] at h;
         simp at *; tauto)
     (λ b hb, ⟨b + n,
-      mem_filter.2 ⟨mem_range.2 $ nat.add_lt_of_lt_sub_right (mem_range.1 hb), nat.le_add_left _ _⟩,
+      mem_filter.2 ⟨mem_range.2 $ lt_sub_iff_right.mp (mem_range.1 hb), nat.le_add_left _ _⟩,
       by rw nat.add_sub_cancel⟩)
 ... ≤ ∑ m in range (j - n), (n! * n.succ ^ m)⁻¹ :
   begin
@@ -1259,7 +1259,7 @@ begin
     begin
       refine congr_arg abs (sum_congr rfl (λ m hm, _)),
       rw [mem_filter, mem_range] at hm,
-      rw [← mul_div_assoc, ← pow_add, nat.add_sub_cancel' hm.2]
+      rw [← mul_div_assoc, ← pow_add, add_sub_cancel_of_le hm.2]
     end
   ... ≤ ∑ m in filter (λ k, n ≤ k) (range j), abs (x ^ n * (_ / m!)) : abv_sum_le_sum_abv _ _
   ... ≤ ∑ m in filter (λ k, n ≤ k) (range j), abs x ^ n * (1 / m!) :

src/data/equiv/denumerable.lean

@@ -162,7 +162,7 @@ lemma exists_succ (x : s) : ∃ n, x.1 + n + 1 ∈ s :=
 classical.by_contradiction $ λ h,
 have ∀ (a : ℕ) (ha : a ∈ s), a < x.val.succ,
   from λ a ha, lt_of_not_ge (λ hax, h ⟨a - (x.1 + 1),
-    by rwa [add_right_comm, nat.add_sub_cancel' hax]⟩),
+    by rwa [add_right_comm, add_sub_cancel_of_le hax]⟩),
 fintype.false
   ⟨(((multiset.range x.1.succ).filter (∈ s)).pmap
       (λ (y : ℕ) (hy : y ∈ s), subtype.mk y hy)

src/data/equiv/fin.lean

@@ -238,7 +238,7 @@ by convert fin_add_flip_apply_cast_add ⟨k, h⟩ n
   fin_add_flip (⟨k, h₂⟩ : fin (m + n)) = ⟨k - m, sub_le_self'.trans_lt $ add_comm m n ▸ h₂⟩ :=
 begin
   convert fin_add_flip_apply_nat_add ⟨k - m, (sub_lt_iff_right h₁).2 _⟩ m,
-  { simp [nat.add_sub_cancel' h₁] },
+  { simp [add_sub_cancel_of_le h₁] },
   { rwa add_comm }
 end
 

src/data/fin.lean

@@ -790,7 +790,7 @@ by simp only [ext_iff, coe_pred, coe_mk, nat.add_sub_cancel]
 -- 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) :
   fin.pred ⟨i, h⟩ w =
-  ⟨i - 1, by rwa nat.sub_lt_right_iff_lt_add (nat.pos_of_ne_zero (fin.vne_of_ne w))⟩ :=
+  ⟨i - 1, by rwa sub_lt_iff_right (nat.succ_le_of_lt $ nat.pos_of_ne_zero (fin.vne_of_ne w))⟩ :=
 rfl
 
 @[simp] lemma pred_le_pred_iff {n : ℕ} {a b : fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
@@ -818,7 +818,7 @@ end
 
 /-- `sub_nat i h` subtracts `m` from `i`, generalizes `fin.pred`. -/
 def sub_nat (m) (i : fin (n + m)) (h : m ≤ (i : ℕ)) : fin n :=
-⟨(i : ℕ) - m, by { rw [nat.sub_lt_right_iff_lt_add h], exact i.is_lt }⟩
+⟨(i : ℕ) - m, by { rw [sub_lt_iff_right h], exact i.is_lt }⟩
 
 @[simp] lemma coe_sub_nat (i : fin (n + m)) (h : m ≤ i) : (i.sub_nat m h : ℕ) = i - m :=
 rfl
@@ -968,7 +968,7 @@ else
   let j : fin n := ⟨i, lt_of_le_of_ne (nat.le_of_lt_succ i.2) (λ h, hi (fin.ext h))⟩ in
   have wf : n + 1 - j.succ < n + 1 - i, begin
     cases i,
-    rw [nat.sub_lt_sub_left_iff];
+    rw [sub_lt_sub_iff_left_of_le];
     simp [*, nat.succ_le_iff],
   end,
   have hi : i = fin.cast_succ j, from fin.ext rfl,
@@ -1586,7 +1586,7 @@ for the vector length. -/
 def append {α : Type*} {o : ℕ} (ho : o = m + n) (u : fin m → α) (v : fin n → α) : fin o → α :=
 λ i, if h : (i : ℕ) < m
   then u ⟨i, h⟩
-  else v ⟨(i : ℕ) - m, (nat.sub_lt_left_iff_lt_add (le_of_not_lt h)).2 (ho ▸ i.property)⟩
+  else v ⟨(i : ℕ) - m, (sub_lt_iff_left (le_of_not_lt h)).2 (ho ▸ i.property)⟩
 
 @[simp] lemma fin_append_apply_zero {α : Type*} {o : ℕ} (ho : (o + 1) = (m + 1) + n)
   (u : fin (m + 1) → α) (v : fin n → α) :

src/data/finset/basic.lean

@@ -2460,7 +2460,7 @@ def strong_downward_induction {p : finset α → Sort*} {n : ℕ} (H : ∀ t₁,
   t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) :
   ∀ (s : finset α), s.card ≤ n → p s
 | s := H s (λ t ht h, have n - card t < n - card s,
-     from (nat.sub_lt_sub_left_iff ht).2 (finset.card_lt_card h),
+     from (sub_lt_sub_iff_left_of_le ht).2 (finset.card_lt_card h),
   strong_downward_induction t ht)
 using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ (t : finset α), n - t.card)⟩]}
 

src/data/finset/intervals.lean

@@ -175,14 +175,14 @@ begin
   split,
   { rintros ⟨j, ⟨hjk, hjm⟩, rfl⟩,
     split,
-    { simp only [← nat.add_sub_add_right n 1 j, nat.sub_le_sub_left, hjm] },
+    { simp only [← add_sub_add_right_eq_sub' n 1 j, nat.sub_le_sub_left, hjm] },
     { exact nat.sub_le_sub_left _ hjk } },
   { rintros ⟨hm, hk⟩,
-    have hj : j ≤ n := le_trans hk (nat.sub_le_self _ _),
+    have hj : j ≤ n := le_trans hk sub_le_self',
     refine ⟨n - j, ⟨_, _⟩, _⟩,
-    { apply nat.le_sub_right_of_add_le,
-      rwa nat.le_sub_left_iff_add_le hkn at hk },
-    { rwa [← nat.sub_add_comm hj, nat.sub_le_iff] },
+    { apply le_sub_of_add_le_right',
+      rwa le_sub_iff_left hkn at hk },
+    { rwa [← nat.sub_add_comm hj, sub_le_iff_sub_le] },
     { exact nat.sub_sub_self hj } }
 end