diff --git a/Batteries/Lean/HashSet.lean b/Batteries/Lean/HashSet.lean
index 4b6df398b3..7a462a7b8d 100644
--- a/Batteries/Lean/HashSet.lean
+++ b/Batteries/Lean/HashSet.lean
@@ -59,10 +59,3 @@ def insert' (s : HashSet α) (a : α) : HashSet α × Bool :=
   let oldSize := s.size
   let s := s.insert a
   (s, s.size == oldSize)
-
-/--
-`O(n)`. Obtain a `HashSet` from an array.
--/
-@[inline]
-protected def ofArray [BEq α] [Hashable α] (as : Array α) : HashSet α :=
-  HashSet.empty.insertMany as