refactor(data/multiset/basic): remove sub lemmas (#9578)

* Remove the multiset sub lemmas that are special cases of lemmas in `algebra/order/sub`
* [This](https://github.com/leanprover-community/mathlib/blob/14c3324143beef6e538f63da9c48d45f4a949604/src/data/multiset/basic.lean#L1513-L1538) gives the list of renamings.
* Use `derive` in `pnat.factors`.



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

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 [multiset.add_sub_of_le h] at this },
+  suffices : p.prod ≤ (p + (q - p)).prod, { rwa [add_sub_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/data/finset/basic.lean

@@ -1052,7 +1052,8 @@ lemma erase_inj_on (s : finset α) : set.inj_on s.erase s :=
 /-! ### sdiff -/
 
 /-- `s \ t` is the set consisting of the elements of `s` that are not in `t`. -/
-instance : has_sdiff (finset α) := ⟨λs₁ s₂, ⟨s₁.1 - s₂.1, nodup_of_le (sub_le_self _ _) s₁.2⟩⟩
+instance : has_sdiff (finset α) :=
+⟨λs₁ s₂, ⟨s₁.1 - s₂.1, nodup_of_le sub_le_self' s₁.2⟩⟩
 
 @[simp] lemma sdiff_val (s₁ s₂ : finset α) : (s₁ \ s₂).val = s₁.val - s₂.val := rfl
 

src/data/list/perm.lean

@@ -704,7 +704,7 @@ end⟩
 lemma subperm.cons_right {α : Type*} {l l' : list α} (x : α) (h : l <+~ l') : l <+~ x :: l' :=
 h.trans (sublist_cons x l').subperm
 
-/-- The list version of `multiset.add_sub_of_le`. -/
+/-- The list version of `add_sub_cancel_of_le` for multisets. -/
 lemma subperm_append_diff_self_of_count_le {l₁ l₂ : list α}
   (h : ∀ x ∈ l₁, count x l₁ ≤ count x l₂) : l₁ ++ l₂.diff l₁ ~ l₂ :=
 begin

src/data/multiset/antidiagonal.lean

@@ -40,7 +40,8 @@ quotient.induction_on s $ λ l, begin
   haveI := classical.dec_eq α,
   simp [revzip_powerset_aux_lemma l revzip_powerset_aux, h.symm],
   cases x with x₁ x₂,
-  exact ⟨_, le_add_right _ _, by rw add_sub_cancel_left _ _⟩
+  dsimp only,
+  exact ⟨x₁, le_add_right _ _, by rw add_sub_cancel_left x₁ x₂⟩
 end
 
 @[simp] theorem antidiagonal_map_fst (s : multiset α) :

src/data/multiset/basic.lean

@@ -1513,35 +1513,8 @@ quotient.induction_on₂ s t $ λ l₁ l₂,
 show ↑(l₁.diff l₂) = foldl erase erase_comm ↑l₁ ↑l₂,
 by { rw diff_eq_foldl l₁ l₂, symmetry, exact foldl_hom _ _ _ _ _ (λ x y, rfl) }
 
-theorem add_sub_of_le (h : s ≤ t) : s + (t - s) = t :=
-add_sub_cancel_of_le h
-
-theorem sub_add' : s - (t + u) = s - t - u :=
-sub_add_eq_sub_sub'
-
-theorem sub_add_cancel (h : t ≤ s) : s - t + t = s :=
-sub_add_cancel_of_le h
-
-@[simp] theorem add_sub_cancel_left (s : multiset α) : ∀ t, s + t - s = t :=
-add_sub_cancel_left s
-
-@[simp] theorem add_sub_cancel (s t : multiset α) : s + t - t = s :=
-add_sub_cancel_right s t
-
-theorem sub_le_sub_right (h : s ≤ t) (u) : s - u ≤ t - u :=
-sub_le_sub_right' h u
-
-theorem sub_le_sub_left (h : s ≤ t) : ∀ u, u - t ≤ u - s :=
-sub_le_sub_left' h
-
-theorem le_sub_add (s t : multiset α) : s ≤ s - t + t :=
-le_sub_add -- implicit args
-
-theorem sub_le_self (s t : multiset α) : s - t ≤ s :=
-sub_le_self' -- implicit args
-
 @[simp] theorem card_sub {s t : multiset α} (h : t ≤ s) : card (s - t) = card s - card t :=
-(nat.sub_eq_of_eq_add $ by rw [add_comm, ← card_add, sub_add_cancel h]).symm
+(nat.sub_eq_of_eq_add $ by rw [add_comm, ← card_add, sub_add_cancel_of_le h]).symm
 
 /-! ### Union -/
 
@@ -1554,20 +1527,20 @@ instance : has_union (multiset α) := ⟨union⟩
 
 theorem union_def (s t : multiset α) : s ∪ t = s - t + t := rfl
 
-theorem le_union_left (s t : multiset α) : s ≤ s ∪ t := le_sub_add _ _
+theorem le_union_left (s t : multiset α) : s ≤ s ∪ t := le_sub_add
 
 theorem le_union_right (s t : multiset α) : t ≤ s ∪ t := le_add_left _ _
 
-theorem eq_union_left : t ≤ s → s ∪ t = s := sub_add_cancel
+theorem eq_union_left : t ≤ s → s ∪ t = s := sub_add_cancel_of_le
 
 theorem union_le_union_right (h : s ≤ t) (u) : s ∪ u ≤ t ∪ u :=
-add_le_add_right (sub_le_sub_right h _) u
+add_le_add_right (sub_le_sub_right' h _) u
 
 theorem union_le (h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u :=
 by rw ← eq_union_left h₂; exact union_le_union_right h₁ t
 
 @[simp] theorem mem_union : a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t :=
-⟨λ h, (mem_add.1 h).imp_left (mem_of_le $ sub_le_self _ _),
+⟨λ h, (mem_add.1 h).imp_left (mem_of_le sub_le_self'),
  or.rec (mem_of_le $ le_union_left _ _) (mem_of_le $ le_union_right _ _)⟩
 
 @[simp] theorem map_union [decidable_eq β] {f : α → β} (finj : function.injective f)
@@ -1662,7 +1635,7 @@ union_le (le_add_right _ _) (le_add_left _ _)
 
 theorem union_add_distrib (s t u : multiset α) : (s ∪ t) + u = (s + u) ∪ (t + u) :=
 by simpa [(∪), union, eq_comm, add_assoc] using show s + u - (t + u) = s - t,
-by rw [add_comm t, sub_add', add_sub_cancel]
+by rw [add_comm t, sub_add_eq_sub_sub', add_sub_cancel_right]
 
 theorem add_union_distrib (s t u : multiset α) : s + (t ∪ u) = (s + t) ∪ (s + u) :=
 by rw [add_comm, union_add_distrib, add_comm s, add_comm s]
@@ -1709,8 +1682,7 @@ begin
 end
 
 theorem sub_inter (s t : multiset α) : s - (s ∩ t) = s - t :=
-add_right_cancel $
-by rw [sub_add_inter s t, sub_add_cancel (inter_le_left _ _)]
+add_right_cancel $ by rw [sub_add_inter s t, sub_add_cancel_of_le (inter_le_left s t)]
 
 end
 

src/data/multiset/nodup.lean

@@ -191,10 +191,10 @@ 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 (sub_le_self _ _) h, λ h',
+⟨λ h, ⟨mem_of_le sub_le_self' h, λ h',
   by refine count_eq_zero.1 _ h; rw [count_sub a s t, nat.sub_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_sub_add _ _) h₁) h₂⟩
+ λ ⟨h₁, h₂⟩, or.resolve_right (mem_add.1 $ mem_of_le le_sub_add h₁) h₂⟩
 
 lemma map_eq_map_of_bij_of_nodup (f : α → γ) (g : β → γ) {s : multiset α} {t : multiset β}
   (hs : s.nodup) (ht : t.nodup) (i : Πa∈s, β)

src/data/pnat/factors.lean

@@ -23,31 +23,12 @@ the multiplicity of `p` in this factors multiset being the p-adic valuation of `
 /-- The type of multisets of prime numbers.  Unique factorization
  gives an equivalence between this set and ℕ+, as we will formalize
  below. -/
+ @[derive [inhabited, has_repr, canonically_ordered_add_monoid, distrib_lattice,
+  semilattice_sup_bot, has_sub, has_ordered_sub]]
 def prime_multiset := multiset nat.primes
 
 namespace prime_multiset
 
-instance : inhabited prime_multiset :=
-by unfold prime_multiset; apply_instance
-
-instance : has_repr prime_multiset :=
-by { dsimp [prime_multiset], apply_instance }
-
-instance : canonically_ordered_add_monoid prime_multiset :=
-by { dsimp [prime_multiset], apply_instance }
-
-instance : distrib_lattice prime_multiset :=
-by { dsimp [prime_multiset], apply_instance }
-
-instance : semilattice_sup_bot prime_multiset :=
-by { dsimp [prime_multiset], apply_instance }
-
-instance : has_sub prime_multiset :=
-by { dsimp [prime_multiset], apply_instance }
-
-theorem add_sub_of_le {u v : prime_multiset} : u ≤ v → u + (v - u) = v :=
-multiset.add_sub_of_le
-
 /-- The multiset consisting of a single prime -/
 def of_prime (p : nat.primes) : prime_multiset := ({p} : multiset nat.primes)
 
@@ -303,7 +284,7 @@ begin
     rw [← prod_factor_multiset m, ← prod_factor_multiset m],
     apply dvd.intro (n.factor_multiset - m.factor_multiset).prod,
     rw [← prime_multiset.prod_add, prime_multiset.factor_multiset_prod,
-        prime_multiset.add_sub_of_le h, prod_factor_multiset] },
+        add_sub_cancel_of_le h, prod_factor_multiset] },
   { intro  h,
     rw [← mul_div_exact h, factor_multiset_mul],
     exact le_self_add }

src/group_theory/perm/cycle_type.lean

@@ -221,10 +221,10 @@ lemma cycle_type_mul_mem_cycle_factors_finset_eq_sub {f g : perm α}
   (g * f⁻¹).cycle_type = g.cycle_type - f.cycle_type :=
 begin
   suffices : (g * f⁻¹).cycle_type + f.cycle_type = g.cycle_type - f.cycle_type + f.cycle_type,
-  { rw multiset.sub_add_cancel (cycle_type_le_of_mem_cycle_factors_finset hf) at this,
+  { rw sub_add_cancel_of_le (cycle_type_le_of_mem_cycle_factors_finset hf) at this,
     simp [←this] },
   simp [←(disjoint_mul_inv_of_mem_cycle_factors_finset hf).cycle_type,
-    multiset.sub_add_cancel (cycle_type_le_of_mem_cycle_factors_finset hf)]
+    sub_add_cancel_of_le (cycle_type_le_of_mem_cycle_factors_finset hf)]
 end
 
 theorem is_conj_of_cycle_type_eq {σ τ : perm α} (h : cycle_type σ = cycle_type τ) : is_conj σ τ :=
@@ -256,7 +256,7 @@ begin
         rw [hσ.cycle_type, ←hσ', hσ'l.left.cycle_type] },
       refine hστ.is_conj_mul (h1 hs) (h2 _) _,
       { rw [cycle_type_mul_mem_cycle_factors_finset_eq_sub, ←hπ, add_comm, hs,
-            multiset.add_sub_cancel],
+            add_sub_cancel_right],
         rwa finset.mem_def },
       { exact (disjoint_mul_inv_of_mem_cycle_factors_finset hσ'l).symm } } }
 end