From a4e27d30905fa9d952edb2f7b33fa4d439e34404 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Fri, 16 Feb 2024 12:38:16 +1100
Subject: [PATCH] chore: upstream HashSet.merge (#3357)

---
 src/Lean/Data/HashSet.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

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.