chore(*): rename erase_dup to dedup (#12057)

Author: ericrbg

src/algebra/big_operators/basic.lean

@@ -1565,7 +1565,7 @@ lemma to_finset_prod_dvd_prod [comm_monoid α] (S : multiset α) : S.to_finset.p
 begin
   rw finset.prod_eq_multiset_prod,
   refine multiset.prod_dvd_prod_of_le _,
-  simp [multiset.erase_dup_le S],
+  simp [multiset.dedup_le S],
 end
 
 @[to_additive]

src/algebra/gcd_monoid/multiset.lean

@@ -67,7 +67,7 @@ end
 
 variables [decidable_eq α]
 
-@[simp] lemma lcm_erase_dup (s : multiset α) : (erase_dup s).lcm = s.lcm :=
+@[simp] lemma lcm_dedup (s : multiset α) : (dedup s).lcm = s.lcm :=
 multiset.induction_on s (by simp) $ λ a s IH, begin
   by_cases a ∈ s; simp [IH, h],
   unfold lcm,
@@ -77,15 +77,15 @@ end
 
 @[simp] lemma lcm_ndunion (s₁ s₂ : multiset α) :
   (ndunion s₁ s₂).lcm = gcd_monoid.lcm s₁.lcm s₂.lcm :=
-by { rw [← lcm_erase_dup, erase_dup_ext.2, lcm_erase_dup, lcm_add], simp }
+by { rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add], simp }
 
 @[simp] lemma lcm_union (s₁ s₂ : multiset α) :
   (s₁ ∪ s₂).lcm = gcd_monoid.lcm s₁.lcm s₂.lcm :=
-by { rw [← lcm_erase_dup, erase_dup_ext.2, lcm_erase_dup, lcm_add], simp }
+by { rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add], simp }
 
 @[simp] lemma lcm_ndinsert (a : α) (s : multiset α) :
   (ndinsert a s).lcm = gcd_monoid.lcm a s.lcm :=
-by { rw [← lcm_erase_dup, erase_dup_ext.2, lcm_erase_dup, lcm_cons], simp }
+by { rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_cons], simp }
 
 end lcm
 
@@ -136,7 +136,7 @@ end
 
 variables [decidable_eq α]
 
-@[simp] lemma gcd_erase_dup (s : multiset α) : (erase_dup s).gcd = s.gcd :=
+@[simp] lemma gcd_dedup (s : multiset α) : (dedup s).gcd = s.gcd :=
 multiset.induction_on s (by simp) $ λ a s IH, begin
   by_cases a ∈ s; simp [IH, h],
   unfold gcd,
@@ -146,15 +146,15 @@ end
 
 @[simp] lemma gcd_ndunion (s₁ s₂ : multiset α) :
   (ndunion s₁ s₂).gcd = gcd_monoid.gcd s₁.gcd s₂.gcd :=
-by { rw [← gcd_erase_dup, erase_dup_ext.2, gcd_erase_dup, gcd_add], simp }
+by { rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add], simp }
 
 @[simp] lemma gcd_union (s₁ s₂ : multiset α) :
   (s₁ ∪ s₂).gcd = gcd_monoid.gcd s₁.gcd s₂.gcd :=
-by { rw [← gcd_erase_dup, erase_dup_ext.2, gcd_erase_dup, gcd_add], simp }
+by { rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add], simp }
 
 @[simp] lemma gcd_ndinsert (a : α) (s : multiset α) :
   (ndinsert a s).gcd = gcd_monoid.gcd a s.gcd :=
-by { rw [← gcd_erase_dup, erase_dup_ext.2, gcd_erase_dup, gcd_cons], simp }
+by { rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_cons], simp }
 
 end gcd
 

src/algebra/squarefree.lean

@@ -332,7 +332,7 @@ 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, hsq.erase_dup, ← associated_iff_eq,
+      rw [multiset.to_finset_subset, multiset.to_finset_val, hsq.dedup, ← 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⟩,
@@ -342,12 +342,12 @@ begin
         simp only [exists_prop, id.def, exists_eq_right],
         intro con,
         apply not_irreducible_zero (irreducible_of_normalized_factor 0
-            (multiset.mem_erase_dup.1 (multiset.mem_of_le hs con))) },
+            (multiset.mem_dedup.1 (multiset.mem_of_le hs con))) },
       rw (normalized_factors_prod h0).symm.dvd_iff_dvd_right,
-      refine ⟨⟨multiset.prod_dvd_prod_of_le (le_trans hs (multiset.erase_dup_le _)), h0⟩, _⟩,
+      refine ⟨⟨multiset.prod_dvd_prod_of_le (le_trans hs (multiset.dedup_le _)), h0⟩, _⟩,
       have h := unique_factorization_monoid.factors_unique irreducible_of_normalized_factor
         (λ x hx, irreducible_of_normalized_factor x (multiset.mem_of_le
-          (le_trans hs (multiset.erase_dup_le _)) hx)) (normalized_factors_prod hs0),
+          (le_trans hs (multiset.dedup_le _)) hx)) (normalized_factors_prod hs0),
       rw [associated_eq_eq, multiset.rel_eq] at h,
       rw [unique_factorization_monoid.squarefree_iff_nodup_normalized_factors hs0, h],
       apply s.nodup } },

src/data/fin_enum.lean

@@ -43,11 +43,11 @@ def of_nodup_list [decidable_eq α] (xs : list α) (h : ∀ x : α, x ∈ xs) (h
            λ ⟨i,h⟩, xs.nth_le _ h,
            λ x, by simp [of_nodup_list._match_1],
            λ ⟨i,h⟩, by simp [of_nodup_list._match_1,*]; rw list.nth_le_index_of;
-             apply list.nodup_erase_dup ⟩ }
+             apply list.nodup_dedup ⟩ }
 
 /-- create a `fin_enum` instance from an exhaustive list; duplicates are removed -/
 def of_list [decidable_eq α] (xs : list α) (h : ∀ x : α, x ∈ xs) : fin_enum α :=
-of_nodup_list xs.erase_dup (by simp *) (list.nodup_erase_dup _)
+of_nodup_list xs.dedup (by simp *) (list.nodup_dedup _)
 
 /-- create an exhaustive list of the values of a given type -/
 def to_list (α) [fin_enum α] : list α :=

src/data/finset/basic.lean

@@ -149,8 +149,8 @@ theorem eq_of_veq : ∀ {s t : finset α}, s.1 = t.1 → s = t
 @[simp] theorem val_inj {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 :=
-s.2.erase_dup
+@[simp] theorem dedup_eq_self [decidable_eq α] (s : finset α) : dedup s.1 = s.1 :=
+s.2.dedup
 
 instance has_decidable_eq [decidable_eq α] : decidable_eq (finset α)
 | s₁ s₂ := decidable_of_iff _ val_inj
@@ -550,8 +550,8 @@ theorem insert_def (a : α) (s : finset α) : insert a s = ⟨_, nodup_ndinsert
 
 @[simp] theorem insert_val (a : α) (s : finset α) : (insert a s).1 = ndinsert a s.1 := rfl
 
-theorem insert_val' (a : α) (s : finset α) : (insert a s).1 = erase_dup (a ::ₘ s.1) :=
-by rw [erase_dup_cons, erase_dup_eq_self]; refl
+theorem insert_val' (a : α) (s : finset α) : (insert a s).1 = dedup (a ::ₘ s.1) :=
+by rw [dedup_cons, dedup_eq_self]; refl
 
 theorem insert_val_of_not_mem {a : α} {s : finset α} (h : a ∉ s) : (insert a s).1 = a ::ₘ s.1 :=
 by rw [insert_val, ndinsert_of_not_mem h]
@@ -1658,30 +1658,30 @@ def not_mem_range_equiv (k : ℕ) : {n // n ∉ range k} ≃ ℕ :=
 @[simp] lemma coe_not_mem_range_equiv_symm (k : ℕ) :
   ((not_mem_range_equiv k).symm : ℕ → {n // n ∉ range k}) = λ j, ⟨j + k, by simp⟩ := rfl
 
-/-! ### erase_dup on list and multiset -/
+/-! ### dedup on list and multiset -/
 
 namespace multiset
 variable [decidable_eq α]
 
 /-- `to_finset s` removes duplicates from the multiset `s` to produce a finset. -/
-def to_finset (s : multiset α) : finset α := ⟨_, nodup_erase_dup s⟩
+def to_finset (s : multiset α) : finset α := ⟨_, nodup_dedup s⟩
 
-@[simp] theorem to_finset_val (s : multiset α) : s.to_finset.1 = s.erase_dup := rfl
+@[simp] theorem to_finset_val (s : multiset α) : s.to_finset.1 = s.dedup := rfl
 
 theorem to_finset_eq {s : multiset α} (n : nodup s) : finset.mk s n = s.to_finset :=
-finset.val_inj.1 n.erase_dup.symm
+finset.val_inj.1 n.dedup.symm
 
 lemma nodup.to_finset_inj {l l' : multiset α} (hl : nodup l) (hl' : nodup l')
   (h : l.to_finset = l'.to_finset) : l = l' :=
 by simpa [←to_finset_eq hl, ←to_finset_eq hl'] using h
 
-@[simp] lemma mem_to_finset {a : α} {s : multiset α} : a ∈ s.to_finset ↔ a ∈ s := mem_erase_dup
+@[simp] lemma mem_to_finset {a : α} {s : multiset α} : a ∈ s.to_finset ↔ a ∈ s := mem_dedup
 
 @[simp] lemma to_finset_zero : to_finset (0 : multiset α) = ∅ := rfl
 
 @[simp] lemma to_finset_cons (a : α) (s : multiset α) :
   to_finset (a ::ₘ s) = insert a (to_finset s) :=
-finset.eq_of_veq erase_dup_cons
+finset.eq_of_veq dedup_cons
 
 @[simp] lemma to_finset_singleton (a : α) : to_finset ({a} : multiset α) = {a} :=
 by rw [singleton_eq_cons, to_finset_cons, to_finset_zero, is_lawful_singleton.insert_emptyc_eq]
@@ -1706,7 +1706,7 @@ finset.ext $ by simp
 by ext; simp
 
 theorem to_finset_eq_empty {m : multiset α} : m.to_finset = ∅ ↔ m = 0 :=
-finset.val_inj.symm.trans multiset.erase_dup_eq_zero
+finset.val_inj.symm.trans multiset.dedup_eq_zero
 
 @[simp] lemma to_finset_subset (s t : multiset α) : s.to_finset ⊆ t.to_finset ↔ s ⊆ t :=
 by simp only [finset.subset_iff, multiset.subset_iff, multiset.mem_to_finset]
@@ -1729,32 +1729,32 @@ variables [decidable_eq α] {l l' : list α} {a : α}
 /-- `to_finset l` removes duplicates from the list `l` to produce a finset. -/
 def to_finset (l : list α) : finset α := multiset.to_finset l
 
-@[simp] theorem to_finset_val (l : list α) : l.to_finset.1 = (l.erase_dup : multiset α) := rfl
+@[simp] theorem to_finset_val (l : list α) : l.to_finset.1 = (l.dedup : multiset α) := rfl
 
 lemma to_finset_eq (n : nodup l) : @finset.mk α l n = l.to_finset := multiset.to_finset_eq n
 
-@[simp] lemma mem_to_finset : a ∈ l.to_finset ↔ a ∈ l := mem_erase_dup
+@[simp] lemma mem_to_finset : a ∈ l.to_finset ↔ a ∈ l := mem_dedup
 @[simp] lemma to_finset_nil : to_finset (@nil α) = ∅ := rfl
 
 @[simp] lemma to_finset_cons : to_finset (a :: l) = insert a (to_finset l) :=
-finset.eq_of_veq $ by by_cases h : a ∈ l; simp [finset.insert_val', multiset.erase_dup_cons, h]
+finset.eq_of_veq $ by by_cases h : a ∈ l; simp [finset.insert_val', multiset.dedup_cons, h]
 
 lemma to_finset_surj_on : set.surj_on to_finset {l : list α | l.nodup} set.univ :=
 by { rintro ⟨⟨l⟩, hl⟩ _, exact ⟨l, hl, (to_finset_eq hl).symm⟩ }
 
 theorem to_finset_surjective : surjective (to_finset : list α → finset α) :=
 λ s, let ⟨l, _, hls⟩ := to_finset_surj_on (set.mem_univ s) in ⟨l, hls⟩
 
-lemma to_finset_eq_iff_perm_erase_dup : l.to_finset = l'.to_finset ↔ l.erase_dup ~ l'.erase_dup :=
-by simp [finset.ext_iff, perm_ext (nodup_erase_dup _) (nodup_erase_dup _)]
+lemma to_finset_eq_iff_perm_dedup : l.to_finset = l'.to_finset ↔ l.dedup ~ l'.dedup :=
+by simp [finset.ext_iff, perm_ext (nodup_dedup _) (nodup_dedup _)]
 
 lemma to_finset.ext_iff {a b : list α} : a.to_finset = b.to_finset ↔ ∀ x, x ∈ a ↔ x ∈ b :=
 by simp only [finset.ext_iff, mem_to_finset]
 
 lemma to_finset.ext : (∀ x, x ∈ l ↔ x ∈ l') → l.to_finset = l'.to_finset := to_finset.ext_iff.mpr
 
 lemma to_finset_eq_of_perm (l l' : list α) (h : l ~ l') : l.to_finset = l'.to_finset :=
-to_finset_eq_iff_perm_erase_dup.mpr h.erase_dup
+to_finset_eq_iff_perm_dedup.mpr h.dedup
 
 lemma perm_of_nodup_nodup_to_finset_eq (hl : nodup l) (hl' : nodup l')
   (h : l.to_finset = l'.to_finset) : l ~ l' :=
@@ -1907,14 +1907,14 @@ variables [decidable_eq β]
 /-- `image f s` is the forward image of `s` under `f`. -/
 def image (f : α → β) (s : finset α) : finset β := (s.1.map f).to_finset
 
-@[simp] theorem image_val (f : α → β) (s : finset α) : (image f s).1 = (s.1.map f).erase_dup := rfl
+@[simp] theorem image_val (f : α → β) (s : finset α) : (image f s).1 = (s.1.map f).dedup := rfl
 
 @[simp] theorem image_empty (f : α → β) : (∅ : finset α).image f = ∅ := rfl
 
 variables {f g : α → β} {s : finset α} {t : finset β} {a : α} {b c : β}
 
 @[simp] lemma mem_image : b ∈ s.image f ↔ ∃ a ∈ s, f a = b :=
-by simp only [mem_def, image_val, mem_erase_dup, multiset.mem_map, exists_prop]
+by simp only [mem_def, image_val, mem_dedup, multiset.mem_map, exists_prop]
 
 lemma mem_image_of_mem (f : α → β) {a} (h : a ∈ s) : f a ∈ s.image f := mem_image.2 ⟨_, h, rfl⟩
 
@@ -1969,18 +1969,18 @@ 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 :=
-(nodup_map_on H s.2).erase_dup
+(nodup_map_on H s.2).dedup
 
 @[simp] lemma image_id [decidable_eq α] : s.image id = s :=
 ext $ λ _, by simp only [mem_image, exists_prop, id, exists_eq_right]
 
 @[simp] theorem image_id' [decidable_eq α] : s.image (λ x, x) = s := image_id
 
 theorem image_image [decidable_eq γ] {g : β → γ} : (s.image f).image g = s.image (g ∘ f) :=
-eq_of_veq $ by simp only [image_val, erase_dup_map_erase_dup_eq, multiset.map_map]
+eq_of_veq $ by simp only [image_val, dedup_map_dedup_eq, multiset.map_map]
 
 theorem image_subset_image {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : s₁.image f ⊆ s₂.image f :=
-by simp only [subset_def, image_val, subset_erase_dup', erase_dup_subset',
+by simp only [subset_def, image_val, subset_dedup', dedup_subset',
   multiset.map_subset_map h]
 
 lemma image_subset_iff : s.image f ⊆ t ↔ ∀ x ∈ s, f x ∈ t :=
@@ -2064,7 +2064,7 @@ lemma range_add (a b : ℕ) : range (a + b) = range a ∪ (range b).map (add_lef
 by { rw [←val_inj, union_val], exact multiset.range_add_eq_union a b }
 
 @[simp] lemma attach_image_val [decidable_eq α] {s : finset α} : s.attach.image subtype.val = s :=
-eq_of_veq $ by rw [image_val, attach_val, multiset.attach_map_val, erase_dup_eq_self]
+eq_of_veq $ by rw [image_val, attach_val, multiset.attach_map_val, dedup_eq_self]
 
 @[simp] lemma attach_image_coe [decidable_eq α] {s : finset α} : s.attach.image coe = s :=
 finset.attach_image_val
@@ -2078,7 +2078,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 (s.map f).2.erase_dup.symm
+eq_of_veq (s.map f).2.dedup.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,
@@ -2173,7 +2173,7 @@ end image
 
 lemma _root_.multiset.to_finset_map [decidable_eq α] [decidable_eq β] (f : α → β) (m : multiset α) :
   (m.map f).to_finset = m.to_finset.image f :=
-finset.val_inj.1 (multiset.erase_dup_map_erase_dup_eq _ _).symm
+finset.val_inj.1 (multiset.dedup_map_dedup_eq _ _).symm
 
 section to_list
 
@@ -2224,12 +2224,12 @@ protected def bUnion (s : finset α) (t : α → finset β) : finset β :=
 (s.1.bind (λ a, (t a).1)).to_finset
 
 @[simp] theorem bUnion_val (s : finset α) (t : α → finset β) :
-  (s.bUnion t).1 = (s.1.bind (λ a, (t a).1)).erase_dup := rfl
+  (s.bUnion t).1 = (s.1.bind (λ a, (t a).1)).dedup := rfl
 
 @[simp] theorem bUnion_empty : finset.bUnion ∅ t = ∅ := rfl
 
 @[simp] lemma mem_bUnion {b : β} : b ∈ s.bUnion t ↔ ∃ a ∈ s, b ∈ t a :=
-by simp only [mem_def, bUnion_val, mem_erase_dup, mem_bind, exists_prop]
+by simp only [mem_def, bUnion_val, mem_dedup, mem_bind, exists_prop]
 
 @[simp] lemma coe_bUnion : (s.bUnion t : set β) = ⋃ x ∈ (s : set α), t x :=
 by simp only [set.ext_iff, mem_bUnion, set.mem_Union, iff_self, mem_coe, implies_true_iff]

src/data/finset/card.lean

@@ -118,14 +118,14 @@ end finset
 section to_list_multiset
 variables [decidable_eq α] (m : multiset α) (l : list α)
 
-lemma multiset.card_to_finset : m.to_finset.card = m.erase_dup.card := rfl
+lemma multiset.card_to_finset : m.to_finset.card = m.dedup.card := rfl
 
-lemma multiset.to_finset_card_le : m.to_finset.card ≤ m.card := card_le_of_le $ erase_dup_le _
+lemma multiset.to_finset_card_le : m.to_finset.card ≤ m.card := card_le_of_le $ dedup_le _
 
 lemma multiset.to_finset_card_of_nodup {m : multiset α} (h : m.nodup) : m.to_finset.card = m.card :=
-congr_arg card $ multiset.erase_dup_eq_self.mpr h
+congr_arg card $ multiset.dedup_eq_self.mpr h
 
-lemma list.card_to_finset : l.to_finset.card = l.erase_dup.length := rfl
+lemma list.card_to_finset : l.to_finset.card = l.dedup.length := rfl
 
 lemma list.to_finset_card_le : l.to_finset.card ≤ l.length := multiset.to_finset_card_le ⟦l⟧
 
@@ -148,12 +148,12 @@ by simp only [card, image_val_of_inj_on H, card_map]
 
 lemma inj_on_of_card_image_eq [decidable_eq β] (H : (s.image f).card = s.card) : set.inj_on f s :=
 begin
-  change (s.1.map f).erase_dup.card = s.1.card at H,
-  have : (s.1.map f).erase_dup = s.1.map f,
-  { refine multiset.eq_of_le_of_card_le (multiset.erase_dup_le _) _,
+  change (s.1.map f).dedup.card = s.1.card at H,
+  have : (s.1.map f).dedup = s.1.map f,
+  { refine multiset.eq_of_le_of_card_le (multiset.dedup_le _) _,
     rw H,
     simp only [multiset.card_map] },
-  rw multiset.erase_dup_eq_self at this,
+  rw multiset.dedup_eq_self at this,
   exact inj_on_of_nodup_map this,
 end
 

src/data/finset/noncomm_prod.lean

@@ -188,7 +188,7 @@ def noncomm_prod (s : finset α) (f : α → β) (comm : ∀ (x ∈ s) (y ∈ s)
   (hl : l.nodup) :
   noncomm_prod l.to_finset f comm = (l.map f).prod :=
 begin
-  rw ←list.erase_dup_eq_self at hl,
+  rw ←list.dedup_eq_self at hl,
   simp [noncomm_prod, hl]
 end
 

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 ← (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 $
+  rw ← (pi (insert a s) t).2.dedup,
+  refine (λ s' (h : s' = a ::ₘ s.1), (_ : dedup (multiset.pi s' (λ a, (t a).1)) =
+    dedup ((t a).1.bind $ λ b,
+    dedup $ (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.nodup.erase_dup,
+  rw multiset.nodup.dedup,
   exact multiset.nodup_map (multiset.pi_cons_injective ha) (pi s t).2,
 end
 

src/data/list/alist.lean

@@ -47,7 +47,7 @@ structure alist (β : α → Type v) : Type (max u v) :=
 entries with duplicate keys. -/
 def list.to_alist [decidable_eq α] {β : α → Type v} (l : list (sigma β)) : alist β :=
 { entries := _,
-  nodupkeys := nodupkeys_erase_dupkeys l }
+  nodupkeys := nodupkeys_dedupkeys l }
 
 namespace alist
 
@@ -221,7 +221,7 @@ by simp only [lookup, insert, lookup_kinsert]
 lookup_kinsert_ne h
 
 @[simp] theorem lookup_to_alist {a} (s : list (sigma β)) : lookup a s.to_alist = s.lookup a :=
-by rw [list.to_alist,lookup,lookup_erase_dupkeys]
+by rw [list.to_alist,lookup,lookup_dedupkeys]
 
 @[simp] theorem insert_insert {a} {b b' : β a} (s : alist β) :
   (s.insert a b).insert a b' = s.insert a b' :=
@@ -239,7 +239,7 @@ ext $ by simp only [alist.insert_entries, list.kerase_cons_eq, and_self, alist.s
   heq_iff_eq, eq_self_iff_true]
 
 @[simp] theorem entries_to_alist (xs : list (sigma β)) :
-  (list.to_alist xs).entries = erase_dupkeys xs := rfl
+  (list.to_alist xs).entries = dedupkeys xs := rfl
 
 theorem to_alist_cons (a : α) (b : β a) (xs : list (sigma β)) :
   list.to_alist (⟨a,b⟩ :: xs) = insert a b xs.to_alist := rfl