diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean
index 7ddcb61ecf..c528dddbe0 100644
--- a/src/Lean/Data/HashSet.lean
+++ b/src/Lean/Data/HashSet.lean
@@ -194,3 +194,11 @@ def insertMany [ForIn Id ρ α] (s : HashSet α) (as : ρ) : HashSet α := Id.ru
   for a in as do
     s := s.insert a
   return s
+
+/--
+`O(|t|)` amortized. Merge two `HashSet`s.
+-/
+@[inline]
+def merge {α : Type u} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α :=
+  t.fold (init := s) fun s a => s.insert a
+  -- We don't use `insertMany` here because it gives weird universes.