refactor(data/finsupp/basic): remove sub lemmas (#9603)

* Remove the finsupp sub lemmas that are special cases of lemmas in `algebra/order/sub`, namely:
  * `finsupp.nat_zero_sub`
  * `finsupp.nat_sub_self`
  * `finsupp.nat_add_sub_of_le`
  * `finsupp.nat_sub_add_cancel`
  * `finsupp.nat_add_sub_cancel`
  * `finsupp.nat_add_sub_cancel_left`
  * `finsupp.nat_add_sub_assoc`
* Rename the remaining lemmas to use `tsub`:
  * `finsupp.coe_nat_sub` → `finsupp.coe_tsub`
  * `finsupp.nat_sub_apply` → `finsupp.tsub_apply`

  Lemmas in `algebra/order/sub` will soon also use `tsub` (see [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mul_lt_mul''''))

src/data/finsupp/antidiagonal.lean

@@ -51,8 +51,8 @@ begin
   suffices : a = g → (a + b = f ↔ g ≤ f ∧ b = f - g),
   { simpa [apply_ite ((∈) (a, b)), ← and.assoc, @and.right_comm _ (a = _), and.congr_left_iff] },
   unfreezingI {rintro rfl}, split,
-  { rintro rfl, exact ⟨le_add_right le_rfl, (nat_add_sub_cancel_left _ _).symm⟩ },
-  { rintro ⟨h, rfl⟩, exact nat_add_sub_of_le h }
+  { rintro rfl, exact ⟨le_add_right le_rfl, (add_sub_cancel_left _ _).symm⟩ },
+  { rintro ⟨h, rfl⟩, exact add_sub_cancel_of_le h }
 end
 
 lemma antidiagonal_filter_snd_eq (f g : α →₀ ℕ)
@@ -63,8 +63,8 @@ begin
   suffices : b = g → (a + b = f ↔ g ≤ f ∧ a = f - g),
   { simpa [apply_ite ((∈) (a, b)), ← and.assoc, and.congr_left_iff] },
   unfreezingI {rintro rfl}, split,
-  { rintro rfl, exact ⟨le_add_left le_rfl, (nat_add_sub_cancel _ _).symm⟩ },
-  { rintro ⟨h, rfl⟩, exact nat_sub_add_cancel h }
+  { rintro rfl, exact ⟨le_add_left le_rfl, (add_sub_cancel_right _ _).symm⟩ },
+  { rintro ⟨h, rfl⟩, exact sub_add_cancel_of_le h }
 end
 
 @[simp] lemma antidiagonal_zero : antidiagonal (0 : α →₀ ℕ) = singleton (0,0) :=

src/data/finsupp/basic.lean

@@ -2678,21 +2678,22 @@ subrelation.wf (sum_id_lt_of_lt) $ inv_image.wf _ nat.lt_wf
 
 variable {α}
 
-/-! Declarations about subtraction on `finsupp`.
+/-! Declarations about subtraction on `finsupp` with codomain a `canonically_ordered_add_monoid`.
 
 Some of these lemmas are used to develop the partial derivative on `mv_polynomial`. -/
 section nat_sub
 section canonically_ordered_monoid
 
 variables [canonically_ordered_add_monoid M] [has_sub M] [has_ordered_sub M]
 
-/-- Todo: rename. It is defined more generally for `canonically_ordered_add_monoid` -/
-instance nat_sub : has_sub (α →₀ M) :=
+/-- This is called `tsub` for truncated subtraction, to distinguish it with subtraction in an
+additive group. -/
+instance tsub : has_sub (α →₀ M) :=
 ⟨zip_with (λ m n, m - n) (sub_self' 0)⟩
 
-@[simp] lemma coe_nat_sub (g₁ g₂ : α →₀ M) : ⇑(g₁ - g₂) = g₁ - g₂ := rfl
+@[simp] lemma coe_tsub (g₁ g₂ : α →₀ M) : ⇑(g₁ - g₂) = g₁ - g₂ := rfl
 
-lemma nat_sub_apply (g₁ g₂ : α →₀ M) (a : α) : (g₁ - g₂) a = g₁ a - g₂ a := rfl
+lemma tsub_apply (g₁ g₂ : α →₀ M) (a : α) : (g₁ - g₂) a = g₁ a - g₂ a := rfl
 
 instance : canonically_ordered_add_monoid (α →₀ M) :=
 { bot := 0,
@@ -2705,47 +2706,17 @@ instance : canonically_ordered_add_monoid (α →₀ M) :=
     end,
  ..(by apply_instance : ordered_add_comm_monoid (α →₀ M)) }
 
-protected theorem sub_le_iff_right {f g h : α →₀ M} : f - g ≤ h ↔ f ≤ h + g :=
-begin
-  apply forall_congr, intro x,
-  simp only [finsupp.coe_nat_sub, pi.add_apply, sub_le_iff_right, finsupp.coe_add, pi.sub_apply]
-end
-
 instance : has_ordered_sub (α →₀ M) :=
-⟨λ n m k, finsupp.sub_le_iff_right⟩
+⟨λ n m k, forall_congr $ λ x, sub_le_iff_right⟩
 
-@[simp] lemma single_nat_sub {a : α} {n₁ n₂ : M} : single a (n₁ - n₂) = single a n₁ - single a n₂ :=
+@[simp] lemma single_tsub {a : α} {n₁ n₂ : M} : single a (n₁ - n₂) = single a n₁ - single a n₂ :=
 begin
   ext f,
   by_cases h : (a = f),
-  { rw [h, nat_sub_apply, single_eq_same, single_eq_same, single_eq_same] },
-  rw [nat_sub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, sub_self']
+  { rw [h, tsub_apply, single_eq_same, single_eq_same, single_eq_same] },
+  rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, sub_self']
 end
 
-lemma nat_zero_sub (f : α →₀ M) : 0 - f = 0 :=
-zero_sub' f
-
-lemma nat_sub_self (f : α →₀ M) : f - f = 0 :=
-sub_self' f
-
-lemma nat_add_sub_of_le {f g : α →₀ M} (h : f ≤ g) : f + (g - f) = g :=
-add_sub_cancel_of_le h
-
-lemma nat_sub_add_cancel {f g : α →₀ M} (h : f ≤ g) : g - f + f = g :=
-sub_add_cancel_of_le h
-
-variables [contravariant_class M M (+) (≤)]
-
-lemma nat_add_sub_cancel (f g : α →₀ M) : f + g - g = f :=
-add_sub_cancel_right f g
-
-lemma nat_add_sub_cancel_left (f g : α →₀ M) : f + g - f = g :=
-add_sub_cancel_left f g
-
-lemma nat_add_sub_assoc {f₁ f₂ : α →₀ M} (h : f₁ ≤ f₂) (f₃ : α →₀ M) :
-  f₃ + f₂ - f₁ = f₃ + (f₂ - f₁) :=
-add_sub_assoc_of_le h f₃
-
 end canonically_ordered_monoid
 
 /-! Some lemmas specifically about `ℕ`. -/

src/data/mv_polynomial/basic.lean

@@ -455,7 +455,7 @@ begin
   { conv_rhs {rw ← coeff_mul_X _ s},
     congr' with  t,
     by_cases hj : s = t,
-    { subst t, simp only [nat_sub_apply, add_apply, single_eq_same],
+    { 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 },
     { simp [single_eq_of_ne hj] } },
   { rw ← not_mem_support_iff, intro hm, apply h,

src/ring_theory/power_series/basic.lean

@@ -192,14 +192,14 @@ end
 lemma coeff_add_monomial_mul (a : R) :
   coeff R (m + n) (monomial R m a * φ) = a * coeff R n φ :=
 begin
-  rw [coeff_monomial_mul, if_pos, nat_add_sub_cancel_left],
+  rw [coeff_monomial_mul, if_pos, add_sub_cancel_left],
   exact le_add_right le_rfl
 end
 
 lemma coeff_add_mul_monomial (a : R) :
   coeff R (m + n) (φ * monomial R n a) = coeff R m φ * a :=
 begin
-  rw [coeff_mul_monomial, if_pos, nat_add_sub_cancel],
+  rw [coeff_mul_monomial, if_pos, add_sub_cancel_right],
   exact le_add_left le_rfl
 end
 
@@ -271,8 +271,8 @@ begin
   ext k,
   simp only [coeff_mul_monomial, coeff_monomial],
   split_ifs with h₁ h₂ h₃ h₃ h₂; try { refl },
-  { rw [← h₂, nat_sub_add_cancel h₁] at h₃, exact (h₃ rfl).elim },
-  { rw [h₃, nat_add_sub_cancel] at h₂, exact (h₂ rfl).elim },
+  { rw [← h₂, sub_add_cancel_of_le h₁] at h₃, exact (h₃ rfl).elim },
+  { rw [h₃, add_sub_cancel_right] at h₂, exact (h₂ rfl).elim },
   { exact zero_mul b },
   { rw h₂ at h₁, exact (h₁ $ le_add_left le_rfl).elim }
 end
@@ -542,14 +542,14 @@ 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.nat_sub_apply] },
+          ext t, simp only [nat.add_sub_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],
       { rintros ⟨i,j⟩ hij, rw finsupp.mem_antidiagonal at hij,
         rw coeff_X_pow, split_ifs with hi,
         { exfalso, apply H, rw [← hij, hi], ext,
-          rw [coe_add, coe_add, pi.add_apply, pi.add_apply, nat_add_sub_cancel_left, add_comm], },
+          rw [coe_add, coe_add, pi.add_apply, pi.add_apply, add_sub_cancel_left, add_comm], },
         { exact zero_mul _ } },
       { classical, contrapose! H, ext t,
         by_cases hst : s = t,