diff --git a/src/Lean/Data/NameMap/Basic.lean b/src/Lean/Data/NameMap/Basic.lean
index 4229f72aded3..503397f52b0f 100644
--- a/src/Lean/Data/NameMap/Basic.lean
+++ b/src/Lean/Data/NameMap/Basic.lean
@@ -52,6 +52,7 @@ 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
+instance : Membership Name NameSet := ⟨fun (s : NameSet) (n : Name) => s.contains n = true⟩
 instance [Monad m] : ForIn m NameSet Name :=
   inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)
 
@@ -91,6 +92,8 @@ 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
+instance : Membership Name NameSSet := ⟨fun (s : NameSSet) (n : Name) => s.contains n = true⟩
+instance [Monad m] : ForIn m NameSSet Name := inferInstanceAs (ForIn _ (SSet _) ..)
 end NameSSet
 
 @[expose] def NameHashSet := Std.HashSet Name
@@ -101,9 +104,23 @@ instance : EmptyCollection NameHashSet := ⟨empty⟩
 instance : Inhabited NameHashSet := ⟨{}⟩
 def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n
 def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n
+instance : Membership Name NameHashSet := ⟨fun (s : NameHashSet) (n : Name) => s.contains n = true⟩
 
 /-- `filter f s` returns the `NameHashSet` consisting of all `x` in `s` where `f x` returns `true`. -/
 def filter (f : Name → Bool) (s : NameHashSet) : NameHashSet := Std.HashSet.filter f s
+
+/-- The union of two `NameHashSet`s. -/
+def append (s t : NameHashSet) : NameHashSet :=
+  t.fold (init := s) fun s n => s.insert n
+
+instance : Append NameHashSet := ⟨NameHashSet.append⟩
+
+instance : Singleton Name NameHashSet where
+  singleton := fun n => (∅ : NameHashSet).insert n
+
+instance : Union NameHashSet where
+  union := NameHashSet.append
+
 end NameHashSet
 
 def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=
diff --git a/src/Lean/Data/PersistentHashSet.lean b/src/Lean/Data/PersistentHashSet.lean
index 2a4ec0585a7d..1822e5bf5450 100644
--- a/src/Lean/Data/PersistentHashSet.lean
+++ b/src/Lean/Data/PersistentHashSet.lean
@@ -51,6 +51,9 @@ variable {_ : BEq α} {_ : Hashable α}
 @[inline] def contains (s : PersistentHashSet α) (a : α) : Bool :=
   s.set.contains a
 
+instance {_ : BEq α} {_ : Hashable α} : Membership α (PersistentHashSet α) :=
+  ⟨fun (s : PersistentHashSet α) (a : α) => s.contains a = true⟩
+
 @[inline] def foldM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (s : PersistentHashSet α) : m β :=
   s.set.foldlM (init := init) fun d a _ => f d a
 
diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index 439e34b86fa8..4cbb8ce924f8 100644
--- a/src/Lean/Data/Position.lean
+++ b/src/Lean/Data/Position.lean
@@ -22,6 +22,19 @@ namespace Position
 protected def lt : Position → Position → Bool
   | ⟨l₁, c₁⟩, ⟨l₂, c₂⟩ => Prod.lexLt (l₁, c₁) (l₂, c₂)
 
+instance : LT Position := ⟨fun a b => a.lt b⟩
+instance (a b : Position) : Decidable (a < b) := inferInstanceAs (Decidable (a.lt b))
+
+protected def compare : Position → Position → Ordering
+  | ⟨l₁, c₁⟩, ⟨l₂, c₂⟩ =>
+    match Ord.compare l₁ l₂ with
+    | .eq => Ord.compare c₁ c₂
+    | ord => ord
+
+instance : Ord Position := ⟨Position.compare⟩
+
+instance : LE Position := leOfOrd
+
 instance : ToFormat Position :=
   ⟨fun ⟨l, c⟩ => "⟨" ++ format l ++ ", " ++ format c ++ "⟩"⟩
 
diff --git a/src/Lean/Data/RBTree.lean b/src/Lean/Data/RBTree.lean
index af0e305b2a94..8005a96374a9 100644
--- a/src/Lean/Data/RBTree.lean
+++ b/src/Lean/Data/RBTree.lean
@@ -91,6 +91,8 @@ instance [Repr α] : Repr (RBTree α cmp) where
 @[inline] def contains (t : RBTree α cmp) (a : α) : Bool :=
   (t.find? a).isSome
 
+instance : Membership α (RBTree α cmp) := ⟨fun (t : RBTree α cmp) (a : α) => t.contains a = true⟩
+
 def fromList (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=
   l.foldl insert (mkRBTree α cmp)
 
@@ -115,9 +117,21 @@ def union (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
   else
     t₂.fold .insert t₁
 
+instance : Append (RBTree α cmp) := ⟨union⟩
+
+instance : Union (RBTree α cmp) := ⟨union⟩
+
 def diff (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
   t₂.fold .erase t₁
 
+instance : SDiff (RBTree α cmp) := ⟨diff⟩
+
+instance : Singleton α (RBTree α cmp) where
+  singleton := fun a => (mkRBTree α cmp).insert a
+
+instance : Inter (RBTree α cmp) where
+  inter := fun s t => s.fold (fun r a => if t.contains a then r.insert a else r) (mkRBTree α cmp)
+
 /--
 `filter f m` returns the `RBTree` consisting of all
 `x` in `m` where `f x` returns `true`.
diff --git a/src/Lean/Data/SSet.lean b/src/Lean/Data/SSet.lean
index 5a73aa8cd187..582ed0043cf3 100644
--- a/src/Lean/Data/SSet.lean
+++ b/src/Lean/Data/SSet.lean
@@ -28,9 +28,18 @@ abbrev insert (s : SSet α) (a : α) : SSet α :=
 abbrev contains (s : SSet α) (a : α) : Bool :=
   SMap.contains s a
 
+instance : Membership α (SSet α) := ⟨fun (s : SSet α) (a : α) => s.contains a = true⟩
+
 abbrev forM [Monad m] (s : SSet α) (f : α → m PUnit) : m PUnit :=
   SMap.forM s fun a _ => f a
 
+protected def forIn [Monad m] (s : SSet α) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ := do
+  let inst : ForIn m (SMap α Unit) (α × Unit) := inferInstance
+  inst.forIn s init fun (a, _) acc => f a acc
+
+instance [Monad m] : ForIn m (SSet α) α where
+  forIn := SSet.forIn
+
 /-- Move from stage 1 into stage 2. -/
 abbrev switch (s : SSet α) : SSet α :=
   SMap.switch s
diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index 90889ade1fb3..b9f12d43c028 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -61,6 +61,11 @@ def lt : ReducibilityHints → ReducibilityHints → Bool
   | .regular _,  .opaque     => true
   | _,           _           => false
 
+instance : LT ReducibilityHints := ⟨fun a b => a.lt b⟩
+instance (a b : ReducibilityHints) : Decidable (a < b) := inferInstanceAs (Decidable (a.lt b))
+instance : LE ReducibilityHints := ⟨fun a b => a < b ∨ a = b⟩
+instance (a b : ReducibilityHints) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a < b ∨ a = b))
+
 protected def compare : ReducibilityHints → ReducibilityHints → Ordering
   | .abbrev,     .abbrev     => .eq
   | .abbrev,     _           => .lt
diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean
index e30524d7d7fd..2946639f9990 100644
--- a/src/Lean/Meta/Tactic/FVarSubst.lean
+++ b/src/Lean/Meta/Tactic/FVarSubst.lean
@@ -74,6 +74,8 @@ This satisfies `(s.append t).apply e = t.apply (s.apply e)`
 def append (s t : FVarSubst) : FVarSubst :=
   s.1.foldl (fun s' k v => s'.insert k (t.apply v)) t
 
+instance : Append FVarSubst := ⟨append⟩
+
 end FVarSubst
 end Meta
 
diff --git a/src/Lean/Meta/TransparencyMode.lean b/src/Lean/Meta/TransparencyMode.lean
index 420ecb9ee12e..617d62403af1 100644
--- a/src/Lean/Meta/TransparencyMode.lean
+++ b/src/Lean/Meta/TransparencyMode.lean
@@ -32,6 +32,28 @@ def lt : TransparencyMode → TransparencyMode → Bool
   | default,   all       => true
   | _,         _         => false
 
+instance : LT TransparencyMode := ⟨fun a b => a.lt b⟩
+instance (a b : TransparencyMode) : Decidable (a < b) := inferInstanceAs (Decidable (a.lt b))
+
+instance : LE TransparencyMode := ⟨fun a b => a < b ∨ a = b⟩
+instance (a b : TransparencyMode) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a < b ∨ a = b))
+
+protected def beq : TransparencyMode → TransparencyMode → Bool
+  | none,      none      => true
+  | reducible, reducible => true
+  | instances, instances => true
+  | default,   default   => true
+  | all,       all       => true
+  | _,         _         => false
+
+instance : BEq TransparencyMode := ⟨TransparencyMode.beq⟩
+
+protected def compare (a b : TransparencyMode) : Ordering :=
+  if a.lt b then .lt else if b.lt a then .gt else .eq
+
+instance : Ord TransparencyMode where
+  compare := TransparencyMode.compare
+
 end TransparencyMode
 
 example (a b c : TransparencyMode) : a.lt b → b.lt c → a.lt c := by
diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean
index 1b80a1b03aa1..356aaaf76de5 100644
--- a/src/Lean/SubExpr.lean
+++ b/src/Lean/SubExpr.lean
@@ -81,6 +81,8 @@ def all (pred : Nat → Bool) (p : Pos) : Bool :=
 
 def append : Pos → Pos → Pos := foldl push
 
+instance : Append Pos := ⟨append⟩
+
 /-- Creates a subexpression `Pos` from an array of 'coordinates'.
 Each coordinate is a number {0,1,2} expressing which child subexpression should be explored.
 The first coordinate in the array corresponds to the root of the expression tree.  -/