refactor(algebra/order/sub): rename sub -> tsub (#9793)

* Renames lemmas in the file `algebra/order/sub` to use `tsub` instead of `sub` in the name
* Remove primes from lemma names where possible
* [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mul_lt_mul'''')
* Remove `sub_mul_ge`, `mul_sub_ge` and `lt_sub_iff_lt_sub`. They were special cases of `le_sub_mul`, `le_mul_sub` and `lt_sub_comm`, respectively.

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 sub_lt_iff_right z.1,
+      rw tsub_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 sub_lt_iff_right z.2,
+      rw tsub_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) (le_sub_of_add_le_right' hk))
+      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
         (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 le_sub_of_add_le_right' hs, },
+  { rw hst', rw add_assoc at hs, apply le_tsub_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 sub_le_self'.trans (nat.le_add_right _ _),
+          exact tsub_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,
@@ -133,6 +133,6 @@ begin
         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_sub_sub_cancel' ha₀, nat.add_sub_cancel],
+      nat.mul_div_cancel' han, add_tsub_tsub_cancel ha₀, nat.add_sub_cancel],
     exact dvd_mul_right _ _ }
 end

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 (add_sub_cancel_of_le h.le).symm },
+        { exact (add_tsub_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/associated.lean

@@ -554,7 +554,7 @@ theorem prod_le_prod {p q : multiset (associates α)} (h : p ≤ q) : p.prod ≤
 begin
   haveI := classical.dec_eq (associates α),
   haveI := classical.dec_eq α,
-  suffices : p.prod ≤ (p + (q - p)).prod, { rwa [add_sub_cancel_of_le h] at this },
+  suffices : p.prod ≤ (p + (q - p)).prod, { rwa [add_tsub_cancel_of_le h] at this },
   suffices : p.prod * 1 ≤ p.prod * (q - p).prod, { simpa },
   exact mul_mono (le_refl p.prod) one_le
 end

src/algebra/big_operators/basic.lean

@@ -930,7 +930,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₂, add_sub_cancel_of_le h₁],
+  rw [←nat.sub_add_comm h₂, add_tsub_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, add_sub_cancel_of_le $
+... = ∑ i in range n, (n - 1) : sum_congr rfl $ λ i hi, add_tsub_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 le_sub_of_add_le_right' j_in
+  exact le_tsub_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 _ $ add_sub_cancel_of_le $ nat.le_pred_of_lt $ finset.mem_range.1 hi)
+  (λ i hi, congr_arg _ $ add_tsub_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) := sub_add_sub_cancel'' hmn 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 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 [sub_add_eq_add_sub' (nat.le_pred_of_lt (list.mem_range.mp hi)),
+  { 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)] },
 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 sub_le_self',
+  exact (nat.pred_mul_geom_sum_le a b n).trans tsub_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, add_sub_cancel_of_le (one_le_two.trans hb)]
+        : 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]
 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), sub_lt_iff_left],
+      rw [add_comm, ← nat.add_sub_assoc (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] }
@@ -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'), sub_lt_iff_left],
+        rw [add_comm, ← nat.add_sub_assoc (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] }

src/algebra/order/ring.lean

@@ -1414,21 +1414,15 @@ section sub
 variables [canonically_ordered_comm_semiring α] {a b c : α}
 variables [has_sub α] [has_ordered_sub α]
 
-lemma sub_mul_ge : a * c - b * c ≤ (a - b) * c :=
-by { rw [sub_le_iff_right, ← add_mul], exact mul_le_mul_right' le_sub_add c }
-
-lemma mul_sub_ge : a * b - a * c ≤ a * (b - c) :=
-by simp only [mul_comm a, sub_mul_ge]
-
 variables [is_total α (≤)]
 
 namespace add_le_cancellable
 protected lemma mul_sub (h : add_le_cancellable (a * c)) :
   a * (b - c) = a * b - a * c :=
 begin
   cases total_of (≤) b c with hbc hcb,
-  { rw [sub_eq_zero_iff_le.2 hbc, mul_zero, sub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)] },
-  { apply h.eq_sub_of_add_eq, rw [← mul_add, sub_add_cancel_of_le hcb] }
+  { rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)] },
+  { 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 :=