.

src/Std/Data/HashSet/Basic.lean

@@ -283,3 +283,54 @@ end Unverified
 end HashSet
 
 end Std
+
+open Std
+
+namespace List
+
+/--
+Deduplicate an `List α`, keeping the first of each class of `==` elements.
+Uses the `Hashable α` instance for the type,
+for O(n * log n) performance for good hash hash functions.
+
+See `List.eraseDupsWithHash_eq : xs.eraseDupsWithHash = xs.eraseDups`.
+-/
+def eraseDupsWithHash [BEq α] [Hashable α] (xs : List α) : List α := Id.run do
+  let mut result := #[]
+  let mut seen : HashSet α := ∅
+  for x in xs do
+    if ¬ x ∈ seen then
+      result := result.push x
+      seen := seen.insert x
+  return result.toList
+
+def eraseDupsWithHash' [BEq α] [Hashable α] (xs : List α) (seen : HashSet α := ∅) : List α :=
+  match xs with
+  | nil => []
+  | x :: xs =>
+    if seen.contains x then
+      eraseDupsWithHash' xs seen
+    else
+      x :: eraseDupsWithHash' xs (seen.insert x)
+
+end List
+
+namespace Array
+
+/--
+Deduplicate an `Array α`, keeping the first of each class of `==` elements.
+Uses the `Hashable α` instance for the type,
+for O(n * log n) performance for good hash hash functions.
+
+See `Array.eraseDupsWithHash_eq : xs.eraseDupsWithHash = xs.eraseDups`.
+-/
+def eraseDupsWithHash [BEq α] [Hashable α] (xs : Array α) : Array α := Id.run do
+  let mut result := #[]
+  let mut seen : HashSet α := ∅
+  for x in xs do
+    if ¬ x ∈ seen then
+      result := result.push x
+      seen := seen.insert x
+  return result
+
+end Array

src/Std/Data/HashSet/Lemmas.lean

@@ -908,3 +908,42 @@ theorem getD_filter [EquivBEq α] [LawfulHashable α]
 end filter
 
 end Std.HashSet
+
+open Std
+
+namespace List
+
+theorem eraseDupsWithHash'_eq {xs : List α} {seen : HashSet α} :
+    xs.eraseDupsWithHash' seen = (xs.filter fun x => !seen.contains x).eraseDupsWithHash' := by
+  fun_induction eraseDupsWithHash'
+  case case1 =>
+    unfold eraseDupsWithHash'
+    simp
+  case case2 h ih =>
+    unfold eraseDupsWithHash'
+    simp_all [filter_cons]
+  case case3 =>
+    unfold eraseDupsWithHash'
+    simp
+
+@[simp] theorem eraseDupWithHash_nil : ([] : List α).eraseDupsWithHash = [] := by
+  simp [eraseDupsWithHash, Id.run]
+
+@[simp] theorem eraseDupsWithHash_cons {x : α} {xs : List α} :
+    (x :: xs).eraseDupsWithHash = x :: (xs.filter (· != x)).eraseDupsWithHash := by
+  simp [eraseDupsWithHash]
+
+
+theorem eraseDupsWithHash_eq {xs : List α} : xs.eraseDupsWithHash = xs.eraseDups := by
+  cases xs with
+  | nil => simp
+  | cons x xs => simp
+
+end List
+
+namespace Array
+
+theorem eraseDupsWithHash_eq {xs : Array α} : xs.eraseDupsWithHash = xs.toList.eraseDups.toArray := by
+  sorry
+
+end Array