feat(data/multiset/erase_dup): Alias for multiset.erase_dup_eq_self (…

…#9587)

The new `multiset.nodup.erase_dup` allows dot notation.

src/algebra/squarefree.lean

@@ -164,8 +164,8 @@ begin
       rcases an with ⟨b, rfl⟩,
       rw mul_ne_zero_iff at h0,
       rw unique_factorization_monoid.squarefree_iff_nodup_normalized_factors h0.1 at hsq,
-      rw [multiset.to_finset_subset, multiset.to_finset_val, multiset.erase_dup_eq_self.2 hsq,
-        ← associated_iff_eq, normalized_factors_mul h0.1 h0.2],
+      rw [multiset.to_finset_subset, multiset.to_finset_val, hsq.erase_dup, ← associated_iff_eq,
+        normalized_factors_mul h0.1 h0.2],
       exact ⟨multiset.subset_of_le (multiset.le_add_right _ _), normalized_factors_prod h0.1⟩ },
     { rintro ⟨s, hs, rfl⟩,
       rw [finset.mem_powerset, ← finset.val_le_iff, multiset.to_finset_val] at hs,

src/data/finset/basic.lean

@@ -151,7 +151,7 @@ theorem eq_of_veq : ∀ {s t : finset α}, s.1 = t.1 → s = t
 ⟨eq_of_veq, congr_arg _⟩
 
 @[simp] theorem erase_dup_eq_self [decidable_eq α] (s : finset α) : erase_dup s.1 = s.1 :=
-erase_dup_eq_self.2 s.2
+s.2.erase_dup
 
 instance has_decidable_eq [decidable_eq α] : decidable_eq (finset α)
 | s₁ s₂ := decidable_of_iff _ val_inj
@@ -1676,7 +1676,7 @@ def to_finset (s : multiset α) : finset α := ⟨_, nodup_erase_dup s⟩
 @[simp] theorem to_finset_val (s : multiset α) : s.to_finset.1 = s.erase_dup := rfl
 
 theorem to_finset_eq {s : multiset α} (n : nodup s) : finset.mk s n = s.to_finset :=
-finset.val_inj.1 (erase_dup_eq_self.2 n).symm
+finset.val_inj.1 n.erase_dup.symm
 
 lemma nodup.to_finset_inj {l l' : multiset α} (hl : nodup l) (hl' : nodup l')
   (h : l.to_finset = l'.to_finset) : l = l' :=
@@ -1963,7 +1963,7 @@ theorem image_to_finset [decidable_eq α] {s : multiset α} :
 ext $ λ _, by simp only [mem_image, multiset.mem_to_finset, exists_prop, multiset.mem_map]
 
 theorem image_val_of_inj_on (H : set.inj_on f s) : (image f s).1 = s.1.map f :=
-multiset.erase_dup_eq_self.2 (nodup_map_on H s.2)
+(nodup_map_on H s.2).erase_dup
 
 @[simp]
 theorem image_id [decidable_eq α] : s.image id = s :=
@@ -2060,7 +2060,7 @@ ext $ λ ⟨x, hx⟩, ⟨or.cases_on (mem_insert.1 hx)
 λ _, finset.mem_attach _ _⟩
 
 theorem map_eq_image (f : α ↪ β) (s : finset α) : s.map f = s.image f :=
-eq_of_veq $ (multiset.erase_dup_eq_self.2 (s.map f).2).symm
+eq_of_veq (s.map f).2.erase_dup.symm
 
 lemma image_const {s : finset α} (h : s.nonempty) (b : β) : s.image (λa, b) = singleton b :=
 ext $ assume b', by simp only [mem_image, exists_prop, exists_and_distrib_right,

src/data/finset/pi.lean

@@ -73,14 +73,14 @@ assume e₁ e₂ eq,
   pi (insert a s) t = (t a).bUnion (λb, (pi s t).image (pi.cons s a b)) :=
 begin
   apply eq_of_veq,
-  rw ← multiset.erase_dup_eq_self.2 (pi (insert a s) t).2,
+  rw ← (pi (insert a s) t).2.erase_dup,
   refine (λ s' (h : s' = a ::ₘ s.1), (_ : erase_dup (multiset.pi s' (λ a, (t a).1)) =
     erase_dup ((t a).1.bind $ λ b,
     erase_dup $ (multiset.pi s.1 (λ (a : α), (t a).val)).map $
       λ f a' h', multiset.pi.cons s.1 a b f a' (h ▸ h')))) _ (insert_val_of_not_mem ha),
   subst s', rw pi_cons,
   congr, funext b,
-  rw multiset.erase_dup_eq_self.2,
+  rw multiset.nodup.erase_dup,
   exact multiset.nodup_map (multiset.pi_cons_injective ha) (pi s t).2,
 end
 

src/data/multiset/erase_dup.lean

@@ -56,14 +56,16 @@ quot.induction_on s nodup_erase_dup
 
 theorem erase_dup_eq_self {s : multiset α} : erase_dup s = s ↔ nodup s :=
 ⟨λ e, e ▸ nodup_erase_dup s,
- quot.induction_on s $ λ l h, congr_arg coe $ erase_dup_eq_self.2 h⟩
+ quot.induction_on s $ λ l h, congr_arg coe h.erase_dup⟩
+
+alias erase_dup_eq_self ↔ _ multiset.nodup.erase_dup
 
 theorem erase_dup_eq_zero {s : multiset α} : erase_dup s = 0 ↔ s = 0 :=
 ⟨λ h, eq_zero_of_subset_zero $ h ▸ subset_erase_dup _,
  λ h, h.symm ▸ erase_dup_zero⟩
 
 @[simp] theorem erase_dup_singleton {a : α} : erase_dup ({a} : multiset α) = {a} :=
-erase_dup_eq_self.2 $ nodup_singleton _
+(nodup_singleton _).erase_dup
 
 theorem le_erase_dup {s t : multiset α} : s ≤ erase_dup t ↔ s ≤ t ∧ nodup s :=
 ⟨λ h, ⟨le_trans h (erase_dup_le _), nodup_of_le h (nodup_erase_dup _)⟩,

src/number_theory/arithmetic_function.lean

@@ -686,7 +686,7 @@ begin
   split; intro h,
   { rw ← list.eq_of_sublist_of_length_eq n.factors.erase_dup_sublist h,
     apply list.nodup_erase_dup },
-  { rw list.erase_dup_eq_self.2 h,
+  { rw h.erase_dup,
     refl }
 end