diff --git a/src/Lean/Data/NameMap/Basic.lean b/src/Lean/Data/NameMap/Basic.lean
index 4229f72aded3..bde2639b310a 100644
--- a/src/Lean/Data/NameMap/Basic.lean
+++ b/src/Lean/Data/NameMap/Basic.lean
@@ -52,6 +52,8 @@ instance : EmptyCollection NameSet := ⟨empty⟩
 instance : Inhabited NameSet := ⟨empty⟩
 def insert (s : NameSet) (n : Name) : NameSet := Std.TreeSet.insert s n
 def contains (s : NameSet) (n : Name) : Bool := Std.TreeSet.contains s n
+abbrev subset : NameSet -> NameSet -> Bool := Std.TreeSet.subset
+abbrev diff (t₁ t₂ : NameSet) : NameSet := Std.TreeSet.diff t₁ t₂
 instance [Monad m] : ForIn m NameSet Name :=
   inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)
 
@@ -91,6 +93,7 @@ instance : EmptyCollection NameSSet := ⟨empty⟩
 instance : Inhabited NameSSet := ⟨empty⟩
 abbrev insert (s : NameSSet) (n : Name) : NameSSet := SSet.insert s n
 abbrev contains (s : NameSSet) (n : Name) : Bool := SSet.contains s n
+abbrev subset : NameSSet -> NameSSet -> Bool := SSet.subset
 end NameSSet
 
 @[expose] def NameHashSet := Std.HashSet Name
diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index 0cb3f5ff0f61..cff9c9d24b72 100644
--- a/src/Lean/Data/SMap.lean
+++ b/src/Lean/Data/SMap.lean
@@ -107,6 +107,27 @@ def numBuckets (m : SMap α β) : Nat :=
 def toList (m : SMap α β) : List (α × β) :=
   m.fold (init := []) fun es a b => (a, b)::es
 
+/-- Check if any element satisfies the predicate, short-circuiting if a predicate fails. -/
+@[inline]
+def any (s : SMap α β) (p : α → β → Bool) : Bool := Id.run do
+  for ⟨a, b⟩ in s do
+    if p a b then return true
+  return false
+
+/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/
+@[inline]
+def all (s : SMap α β) (p : α → β → Bool) : Bool := Id.run do
+  for ⟨a, b⟩ in s do
+    if p a b = false then return false
+  return true
+
+/--
+`t₁.subset t₂` means that every element of `t₁` is also an element of `t₂`, ignoring multiplicity.
+-/
+@[inline]
+def subset [BEq β] (m₁ m₂ : SMap α β) : Bool :=
+  m₁.all (fun a b => m₂.find? a == some b)
+
 end SMap
 
 def _root_.List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β :=
diff --git a/src/Lean/Data/SSet.lean b/src/Lean/Data/SSet.lean
index 5a73aa8cd187..4931cfa90834 100644
--- a/src/Lean/Data/SSet.lean
+++ b/src/Lean/Data/SSet.lean
@@ -41,6 +41,9 @@ abbrev fold (f : σ → α → σ) (init : σ) (s : SSet α) : σ :=
 def toList (m : SSet α) : List α :=
   m.fold (init := []) fun es a => a::es
 
+abbrev subset (s₁ s₂ : SSet α) : Bool :=
+  s₁.all (fun k .unit => s₂.contains k)
+
 end SSet
 
 end Lean
diff --git a/src/Std/Data/TreeSet/Basic.lean b/src/Std/Data/TreeSet/Basic.lean
index 7f6b98e36793..1fc5bfb6c839 100644
--- a/src/Std/Data/TreeSet/Basic.lean
+++ b/src/Std/Data/TreeSet/Basic.lean
@@ -437,6 +437,22 @@ def any (t : TreeSet α cmp) (p : α → Bool) : Bool :=
 def all (t : TreeSet α cmp) (p : α → Bool) : Bool :=
   t.inner.all (fun a _ => p a)
 
+/--
+`t₁.subset t₂` means that every element of `t₁` is also an element of `t₂`, ignoring multiplicity.
+-/
+@[inline]
+def subset (t₁ t₂ : TreeSet α cmp) : Bool :=
+  t₁.all (t₂.contains ·)
+
+/--
+`t₁.diff t₂` returns a new `TreeSet` containing all elements of `t₁`
+that are not present in `t₂`. Effectively, it removes from `t₁`
+every element found in `t₂`.
+-/
+@[inline]
+def diff (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp :=
+  t₂.foldl .erase t₁
+
 /-- Transforms the tree set into a list of elements in ascending order. -/
 @[inline]
 def toList (t : TreeSet α cmp) : List α :=
@@ -503,14 +519,6 @@ def inter (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp :=
 
 instance : Inter (TreeSet α cmp) := ⟨inter⟩
 
-/--
-Computes the difference of the given tree sets.
-
-This function always iterates through the smaller set.
--/
-def diff (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp :=
-  ⟨TreeMap.diff t₁.inner t₂.inner⟩
-
 instance : SDiff (TreeSet α cmp) := ⟨diff⟩
 
 /--