diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean
index 5bacf2bf..cbc11dd5 100644
--- a/Aesop/Builder/Forward.lean
+++ b/Aesop/Builder/Forward.lean
@@ -47,7 +47,7 @@ def getImmediatePremises (name : Name) (type : Expr) : Option (Array Name) →
     -- If immediate names are given, we check that corresponding arguments
     -- exists and record these arguments' positions.
     forallTelescopeReducing type λ args _ => do
-      let mut unseen := immediate.deduplicate (ord := ⟨Name.quickCmp⟩)
+      let mut unseen := immediate.sortAndDeduplicate (ord := ⟨Name.quickCmp⟩)
       let mut result := #[]
       for h : i in [:args.size] do
         have h : i < args.size := by simp_all [Membership.mem]
diff --git a/Aesop/Frontend/RuleExpr.lean b/Aesop/Frontend/RuleExpr.lean
index 66e2d0d0..c74772f7 100644
--- a/Aesop/Frontend/RuleExpr.lean
+++ b/Aesop/Frontend/RuleExpr.lean
@@ -673,7 +673,7 @@ def toAdditionalRules (e : RuleExpr) (init : RuleConfig Option)
       | .ruleSets newRuleSets =>
         have _ : Ord RuleSetName := ⟨Name.quickCmp⟩
         let ruleSets :=
-          ⟨Array.mergeSortedFilteringDuplicates r.ruleSets.ruleSets $
+          ⟨Array.mergeSortedDeduplicating r.ruleSets.ruleSets $
             newRuleSets.ruleSets.qsortOrd⟩
         return { r with ruleSets }
 
@@ -775,7 +775,7 @@ def toRuleNameFilters (e : RuleExpr) :
       | .ruleSets newRuleSets =>
         have _ : Ord RuleSetName := ⟨Name.quickCmp⟩
         let ruleSets :=
-          ⟨Array.mergeSortedFilteringDuplicates r.ruleSets.ruleSets $
+          ⟨Array.mergeSortedDeduplicating r.ruleSets.ruleSets $
             newRuleSets.ruleSets.qsortOrd⟩
         return { r with ruleSets }
 
diff --git a/Aesop/Index.lean b/Aesop/Index.lean
index 42c576e3..ff818248 100644
--- a/Aesop/Index.lean
+++ b/Aesop/Index.lean
@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.Index.Basic
+import Std.Lean.Meta.InstantiateMVars
 
 open Lean
 open Lean.Meta
@@ -37,8 +38,8 @@ instance : EmptyCollection (Index α) where
   }
 
 def merge (ri₁ ri₂ : Index α) : Index α where
-  byTarget := ri₁.byTarget.merge ri₂.byTarget
-  byHyp := ri₁.byHyp.merge ri₂.byHyp
+  byTarget := ri₁.byTarget.mergePreservingDuplicates ri₂.byTarget
+  byHyp := ri₁.byHyp.mergePreservingDuplicates ri₂.byHyp
   unindexed := ri₁.unindexed.merge ri₂.unindexed
 
 @[specialize]
diff --git a/Aesop/Profiling.lean b/Aesop/Profiling.lean
index d8e3dea3..414ad301 100644
--- a/Aesop/Profiling.lean
+++ b/Aesop/Profiling.lean
@@ -8,8 +8,7 @@ import Aesop.Nanos
 import Aesop.Tree.Data
 import Aesop.Tracing
 
-open Lean hiding HashMap
-open Std (HashMap)
+open Lean
 
 namespace Aesop
 
@@ -108,18 +107,18 @@ protected def toMessageData (p : Profile) : MessageData :=
           node (displayRuleApplications p.ruleApplicationTotals)
   ]]]
   where
-    compareTimings : (x y : RuleProfileName × Nanos × Nanos) → Ordering :=
-      compareOpposite $
-        compareLexicographic
-          (compareOn (λ (_, s, f) => s + f))
-          (compareOn (λ (n, _, _) => n))
+    compareTimings (x y : RuleProfileName × Nanos × Nanos) : Ordering :=
+      compareLex
+        (compareOn (λ (_, s, f) => s + f))
+        (compareOn (λ (n, _, _) => n))
+        x y
+      |>.swap
 
     displayRuleApplications (apps : HashMap RuleProfileName (Nanos × Nanos)) :
         Array MessageData := Id.run do
-      let mut timings : Array (RuleProfileName × Nanos × Nanos) := #[]
-      for (n, (successful, failed)) in apps do
-        timings := timings.push (n, successful, failed)
-      timings := timings.qsortOrd (ord := ⟨compareTimings⟩)
+      let timings := apps.fold (init := Array.mkEmpty apps.size)
+        λ timings n (successful, failed) => timings.push (n, successful, failed)
+      let timings := timings.qsortOrd (ord := ⟨compareTimings⟩)
       let result := timings.map λ (n, s, f) =>
         m!"[{(s + f).printAsMillis} / {s.printAsMillis} / {f.printAsMillis}] {n}"
       return result
diff --git a/Aesop/Rule/Name.lean b/Aesop/Rule/Name.lean
index 039f545e..c92b2e67 100644
--- a/Aesop/Rule/Name.lean
+++ b/Aesop/Rule/Name.lean
@@ -109,9 +109,9 @@ instance : BEq RuleName where
     n₁.scope == n₂.scope && n₁.name == n₂.name
 
 protected def compare : (_ _ : RuleName) → Ordering :=
-  compareLexicographic (compareOn (·.builder)) $
-  compareLexicographic (compareOn (·.phase)) $
-  compareLexicographic (compareOn (·.scope)) $
+  compareLex (compareOn (·.builder)) $
+  compareLex (compareOn (·.phase)) $
+  compareLex (compareOn (·.scope)) $
   (λ n₁ n₂ => n₁.name.cmp n₂.name)
 
 protected def quickCompare (n₁ n₂ : RuleName) : Ordering :=
diff --git a/Aesop/RuleSet.lean b/Aesop/RuleSet.lean
index d0609e42..7c206c81 100644
--- a/Aesop/RuleSet.lean
+++ b/Aesop/RuleSet.lean
@@ -115,12 +115,12 @@ def merge (rs₁ rs₂ : RuleSet) : RuleSet where
   unsafeRules := rs₁.unsafeRules.merge rs₂.unsafeRules
   safeRules := rs₁.safeRules.merge rs₂.safeRules
   normSimpLemmaDescrs :=
-    rs₁.normSimpLemmaDescrs.merge rs₂.normSimpLemmaDescrs λ _ nsd₁ _ => nsd₁
+    rs₁.normSimpLemmaDescrs.mergeWith rs₂.normSimpLemmaDescrs λ _ nsd₁ _ => nsd₁
     -- We can merge left-biased here because `nsd₁` and `nsd₂` should be equal
     -- anyway.
   localNormSimpLemmas := rs₁.localNormSimpLemmas ++ rs₂.localNormSimpLemmas
   ruleNames :=
-    rs₁.ruleNames.merge rs₂.ruleNames λ _ ns₁ ns₂ =>
+    rs₁.ruleNames.mergeWith rs₂.ruleNames λ _ ns₁ ns₂ =>
       ns₁ ++ ns₂
   erased :=
     -- Add the erased rules from `rs₁` to `init`, except those rules which are
diff --git a/Aesop/Script.lean b/Aesop/Script.lean
index 1837240d..d00a0f10 100644
--- a/Aesop/Script.lean
+++ b/Aesop/Script.lean
@@ -7,6 +7,7 @@ Authors: Jannis Limperg
 import Aesop.Util
 import Std.Lean.Meta.Clear
 import Std.Lean.Meta.Inaccessible
+import Std.Lean.HashSet
 
 open Lean
 open Lean.Elab.Tactic
diff --git a/Aesop/Tree/UnsafeQueue.lean b/Aesop/Tree/UnsafeQueue.lean
index f5194389..5961cefd 100644
--- a/Aesop/Tree/UnsafeQueue.lean
+++ b/Aesop/Tree/UnsafeQueue.lean
@@ -6,6 +6,7 @@ Authors: Jannis Limperg
 
 import Aesop.Constants
 import Aesop.Rule
+import Std.Data.Array.Merge
 
 open Lean
 
@@ -45,8 +46,8 @@ def name : UnsafeQueueEntry → RuleName
   | postponedSafeRule r => r.rule.name
 
 instance : Ord UnsafeQueueEntry :=
-  ⟨ compareLexicographic
-      (compareOpposite $ compareOn successProbability)
+  ⟨ compareLex
+      (λ x y => compareOn successProbability x y |>.swap)
       (compareOn name) ⟩
 
 end UnsafeQueueEntry
@@ -70,7 +71,7 @@ def initial (postponedSafeRules : Array PostponedSafeRule)
   let postponedSafeRules :=
     postponedSafeRules.map .postponedSafeRule
       |>.qsort (λ x y => compare x y |>.isLT)
-  postponedSafeRules.mergeSortedFilteringDuplicates unsafeRules |>.toSubarray
+  postponedSafeRules.mergeSortedDeduplicating unsafeRules |>.toSubarray
 
 def entriesToMessageData (q : UnsafeQueue) : Array MessageData :=
   q.toArray.map toMessageData
diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean
index ca868a3f..575beb7e 100644
--- a/Aesop/Util/Basic.lean
+++ b/Aesop/Util/Basic.lean
@@ -6,91 +6,13 @@ Authors: Jannis Limperg, Asta Halkjær From
 
 import Aesop.Nanos
 import Aesop.Util.UnionFind
-import Std.Lean.Meta.InstantiateMVars
-
-
-def BEq.ofOrd (ord : Ord α) : BEq α where
-  beq x y :=
-    match ord.compare x y with
-    | Ordering.eq => true
-    | _ => false
-
-namespace Option
-
-def toArray : Option α → Array α
-  | none => #[]
-  | some a => #[a]
-
-def forM [Monad m] (f : α → m Unit) : Option α → m Unit
-  | none => pure ()
-  | some a => f a
-
-end Option
-
-namespace Ordering
-
-def isLT : Ordering → Bool
-  | lt => true
-  | _ => false
-
-def isEQ : Ordering → Bool
-  | eq => true
-  | _ => false
-
-def isGT : Ordering → Bool
-  | gt => true
-  | _ => false
-
-def isGE : Ordering → Bool
-  | lt => false
-  | eq => true
-  | gt => true
-
-def opposite : Ordering → Ordering
-  | lt => gt
-  | eq => eq
-  | gt => lt
-
-end Ordering
-
-
-@[inline]
-def compareLexicographic (cmp₁ : α → α → Ordering) (cmp₂ : α → α → Ordering)
-    (x y : α) : Ordering :=
-  match cmp₁ x y with
-  | Ordering.eq => cmp₂ x y
-  | ord => ord
-
-@[inline]
-def compareOn [ord : Ord β] (f : α → β) (x y : α) : Ordering :=
-  compare (f x) (f y)
-
-@[inline]
-def compareOpposite (cmp : α → α → Ordering) (x y : α) : Ordering :=
-  cmp x y |>.opposite
+import Std.Lean.Expr
+import Std.Lean.Meta.DiscrTree
+import Std.Lean.PersistentHashSet
 
 
 namespace Subarray
 
-protected def empty : Subarray α where
-  as := #[]
-  start := 0
-  stop := 0
-  h₁ := Nat.le_refl 0
-  h₂ := Nat.le_refl 0
-
-instance : EmptyCollection (Subarray α) :=
-  ⟨Subarray.empty⟩
-
-instance : Inhabited (Subarray α) :=
-  ⟨{}⟩
-
-def isEmpty (as : Subarray α) : Bool :=
-  as.start == as.stop
-
-def contains [BEq α] (as : Subarray α) (a : α) : Bool :=
-  as.any (· == a)
-
 def popFront? (as : Subarray α) : Option (α × Subarray α) :=
   if h : as.start < as.stop
     then
@@ -106,179 +28,6 @@ def popFront? (as : Subarray α) : Option (α × Subarray α) :=
 end Subarray
 
 
-namespace Array
-
-/--
-Merge arrays `xs` and `ys`, which must be sorted according to `compare`. The
-result is sorted as well. If two (or more) elements are equal according to
-`compare`, they are preserved.
--/
-def mergeSortedPreservingDuplicates [ord : Ord α] (xs ys : Array α) :
-    Array α :=
-  let acc := Array.mkEmpty (xs.size + ys.size)
-  go acc 0 0
-  where
-    go (acc : Array α) (i j : Nat) : Array α :=
-      if hi : i ≥ xs.size then
-        acc ++ ys[j:]
-      else if hj : j ≥ ys.size then
-        acc ++ xs[i:]
-      else
-        have hi : i < xs.size := Nat.lt_of_not_le hi
-        have hj : j < ys.size := Nat.lt_of_not_le hj
-        have hij : i + j < xs.size + ys.size := Nat.add_lt_add hi hj
-        let x := xs.get ⟨i, hi⟩
-        let y := ys.get ⟨j, hj⟩
-        if compare x y |>.isLE then
-          have : xs.size + ys.size - (i + 1 + j) < xs.size + ys.size - (i + j) := by
-            rw [show i + 1 + j = i + j + 1 by simp_arith]
-            exact Nat.sub_succ_lt_self _ _ hij
-          go (acc.push x) (i + 1) j
-        else
-          have : xs.size + ys.size - (i + j + 1) < xs.size + ys.size - (i + j) :=
-            Nat.sub_succ_lt_self _ _ hij
-          go (acc.push y) i (j + 1)
-    termination_by _ => xs.size + ys.size - (i + j)
-
-/--
-Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
-not contain duplicates. The result is sorted as well. Equal elements are merged
-using `merge`. If `xs` and `ys` do not contain duplicates according to
-`compare`, then neither does the result.
--/
-def mergeSortedMergingDuplicates [ord : Ord α] (xs ys : Array α)
-    (merge : α → α → α) : Array α :=
-  let acc := Array.mkEmpty (xs.size + ys.size)
-  go acc 0 0
-  where
-    go (acc : Array α) (i j : Nat) : Array α :=
-      if hi : i ≥ xs.size then
-        acc ++ ys[j:]
-      else if hj : j ≥ ys.size then
-        acc ++ xs[i:]
-      else
-        have hi : i < xs.size := Nat.lt_of_not_le hi
-        have hj : j < ys.size := Nat.lt_of_not_le hj
-        have hij : i + j < xs.size + ys.size := Nat.add_lt_add hi hj
-        let x := xs.get ⟨i, hi⟩
-        let y := ys.get ⟨j, hj⟩
-        match compare x y with
-        | Ordering.lt =>
-          have : xs.size + ys.size - (i + 1 + j) < xs.size + ys.size - (i + j) := by
-            rw [show i + 1 + j = i + j + 1 by simp_arith]
-            exact Nat.sub_succ_lt_self _ _ hij
-          go (acc.push x) (i + 1) j
-        | Ordering.gt =>
-          have : xs.size + ys.size - (i + j + 1) < xs.size + ys.size - (i + j) :=
-            Nat.sub_succ_lt_self _ _ hij
-          go (acc.push y) i (j + 1)
-        | Ordering.eq =>
-          have : xs.size + ys.size - (i + 1 + (j + 1)) < xs.size + ys.size - (i + j) := by
-            rw [show i + 1 + (j + 1) = i + j + 2 by simp_arith]
-            apply Nat.sub_add_lt_sub _ (by simp_arith)
-            rw [show i + j + 2 = (i + 1) + (j + 1) by simp_arith]
-            exact Nat.add_le_add hi hj
-          go (acc.push (merge x y)) (i + 1) (j + 1)
-    termination_by _ => xs.size + ys.size - (i + j)
-
-set_option linter.unusedVariables false in
-def mergeSortedFilteringDuplicates [ord : Ord α] (xs ys : Array α) :
-    Array α :=
-  mergeSortedMergingDuplicates xs ys λ x _ => x
-
--- Merge `xs` and `ys`, which do not need to be sorted. Elements which occur in
--- both `xs` and `ys` are only added once. If `xs` and `ys` do not contain
--- duplicates, then neither does the result. O(n*m)!
-set_option linter.unusedVariables false in
-def mergeUnsortedFilteringDuplicates [eq : BEq α] (xs ys : Array α) :
-    Array α :=
-  -- Ideally we would check whether `xs` or `ys` have spare capacity, to prevent
-  -- copying if possible. But Lean arrays don't expose their capacity.
-  if xs.size < ys.size then go ys xs else go xs ys
-  where
-    @[inline]
-    go (xs ys : Array α) :=
-      let xsSize := xs.size
-      ys.foldl (init := xs) λ xs y =>
-        if xs[:xsSize].contains y then xs else xs.push y
-
-def mergeAdjacentDuplicates [eq : BEq α] (f : α → α → α) (xs : Array α) :
-    Array α :=
-  if h : 0 < xs.size then loop #[] 1 (xs.get ⟨0, h⟩) else xs
-  where
-    loop (acc : Array α) (i : Nat) (hd : α) :=
-      if h : i < xs.size then
-        let x := xs.get ⟨i, h⟩
-        if x == hd then
-          loop acc (i + 1) (f hd x)
-        else
-          loop (acc.push hd) (i + 1) x
-      else
-        acc.push hd
-    termination_by _ i _ => xs.size - i
-
-set_option linter.unusedVariables false in
-def deduplicateSorted [eq : BEq α] (xs : Array α) : Array α :=
-  xs.mergeAdjacentDuplicates (λ x _ => x)
-
-set_option linter.unusedVariables false in
-def deduplicate [Inhabited α] [BEq α] [ord : Ord α] (xs : Array α) : Array α :=
-  deduplicateSorted $ xs.qsort λ x y => compare x y |>.isLT
-
-def equalSet [BEq α] (xs ys : Array α) : Bool :=
-  xs.all (ys.contains ·) && ys.all (xs.contains ·)
-
-set_option linter.unusedVariables false in
-def qsortOrd [Inhabited α] [ord : Ord α] (xs : Array α) : Array α :=
-  xs.qsort λ x y => compare x y |>.isLT
-
-set_option linter.unusedVariables false in
-@[inline]
-protected def maxD [ord : Ord α] (d : α) (xs : Array α) (start := 0)
-    (stop := xs.size) : α :=
-  xs.foldl (init := d) (start := start) (stop := stop) λ max x =>
-    if compare x max |>.isLT then max else x
-
-set_option linter.unusedVariables false in
-@[inline]
-protected def max? [ord : Ord α] (xs : Array α) (start := 0)
-    (stop := xs.size) : Option α :=
-  if h : start < xs.size then
-    some $ xs.maxD (xs.get ⟨start, h⟩) start stop
-  else
-    none
-
-set_option linter.unusedVariables false in
-@[inline]
-protected def max [ord : Ord α] [Inhabited α] (xs : Array α) (start := 0)
-    (stop := xs.size) : α :=
-  xs.maxD default start stop
-
-set_option linter.unusedVariables false in
-@[inline]
-protected def minD [ord : Ord α] (d : α) (xs : Array α) (start := 0)
-    (stop := xs.size) : α :=
-  xs.foldl (init := d) (start := start) (stop := stop) λ min x =>
-    if compare x min |>.isGE then min else x
-
-set_option linter.unusedVariables false in
-@[inline]
-protected def min? [ord : Ord α] (xs : Array α) (start := 0)
-    (stop := xs.size) : Option α :=
-  if h : start < xs.size then
-    some $ xs.minD (xs.get ⟨start, h⟩) start stop
-  else
-    none
-
-set_option linter.unusedVariables false in
-@[inline]
-protected def min [ord : Ord α] [Inhabited α] (xs : Array α) (start := 0)
-    (stop := xs.size) : α :=
-  xs.minD default start stop
-
-end Array
-
-
 namespace IO
 
 @[inline]
@@ -298,21 +47,6 @@ def time' [Monad m] [MonadLiftT BaseIO m] (x : m Unit) : m Aesop.Nanos := do
 end IO
 
 
-namespace Lean.Expr
-
-def arity : Expr → Nat
-  | forallE _ _ body _ => 1 + arity body
-  | _ => 0
-
-def isAppOf' : Expr → Name → Bool
-  | mdata _ b, d => isAppOf' b d
-  | const c _, d => c == d
-  | app f _,   d => isAppOf' f d
-  | _,         _ => false
-
-end Lean.Expr
-
-
 namespace Lean.MessageData
 
 def joinSepArray (ms : Array MessageData) (sep : MessageData) :
@@ -341,64 +75,8 @@ def nodeFiltering (fs : Array (Option MessageData)) : MessageData :=
 end Lean.MessageData
 
 
-namespace Lean.HashSet
-
-protected def ofArray [BEq α] [Hashable α] (as : Array α) : HashSet α :=
-  HashSet.empty.insertMany as
-
-@[inline]
-def merge [BEq α] [Hashable α] (s t : HashSet α) : HashSet α :=
-  s.insertMany t
-
-def any [BEq α] [Hashable α] (s : HashSet α) (f : α → Bool) : Bool :=
-  s.fold (init := false) λ result a => result || f a
-
-def all [BEq α] [Hashable α] (s : HashSet α) (f : α → Bool) : Bool :=
-  s.fold (init := true) λ result a => result && f a
-
-instance [BEq α] [Hashable α] : BEq (HashSet α) where
-  beq s t := s.all (t.contains ·) && t.all (s.contains ·)
-
-end Lean.HashSet
-
-
-namespace Std.HashMap
-
-variable [BEq α] [Hashable α]
-
-def merge (m n : HashMap α β) (f : α → β → β → β) : HashMap α β :=
-  if m.size < n.size then loop m n else loop n m
-  where
-    @[inline]
-    loop m n :=
-      m.fold (init := n) λ map k v =>
-        match map.find? k with
-        | none => map.insert k v
-        | some v' => map.insert k $ f k v v'
-
-instance : ForIn m (HashMap α β) (α × β) where
-  forIn m init f := do
-    let mut acc := init
-    for buckets in m.val.buckets.val do
-      for d in buckets do
-        match ← f d acc with
-        | .done b => return b
-        | .yield b => acc := b
-    return acc
-
-end Std.HashMap
-
-
 namespace Lean.PersistentHashSet
 
-@[inline]
-def merge [BEq α] [Hashable α] (s t : PersistentHashSet α) :
-    PersistentHashSet α :=
-  if s.size < t.size then loop s t else loop t s
-  where
-    @[inline]
-    loop s t := s.fold (init := t) λ s a => s.insert a
-
 -- Elements are returned in unspecified order.
 @[inline]
 def toList [BEq α] [Hashable α] (s : PersistentHashSet α) : List α :=
@@ -413,155 +91,8 @@ def toArray [BEq α] [Hashable α] (s : PersistentHashSet α) : Array α :=
 end Lean.PersistentHashSet
 
 
-namespace Lean.PersistentHashMap
-
-variable [BEq α] [Hashable α]
-
-def merge (m n : PersistentHashMap α β) (f : α → β → β → β) :
-    PersistentHashMap α β :=
-  if m.size < n.size then loop m n f else loop n m (λ a b b' => f a b' b)
-  where
-    @[inline]
-    loop m n f := m.foldl (init := n) λ map k v =>
-      match map.find? k with
-      | none => map.insert k v
-      | some v' => map.insert k $ f k v v'
-
-universe u v
-
-def toArray (map : PersistentHashMap α β) : Array (α × β) :=
-  map.foldl (init := Array.mkEmpty map.size) λ acc a b => acc.push (a, b)
-
-end Lean.PersistentHashMap
-
-
-namespace Prod.Lex
-
-instance [αeq_dec : DecidableEq α] {r : α → α → Prop} [r_dec : DecidableRel r]
-    {s : β → β → Prop} [s_dec : DecidableRel s] : DecidableRel (Prod.Lex r s)
-  | (a, b), (a', b') => by
-    cases r_dec a a' with
-    | isTrue raa' => exact isTrue $ left b b' raa'
-    | isFalse nraa' =>
-      cases αeq_dec a a' with
-      | isTrue eq =>
-        subst eq
-        cases s_dec b b' with
-        | isTrue sbb' => exact isTrue $ right a sbb'
-        | isFalse nsbb' =>
-          apply isFalse; intro contra; cases contra <;> contradiction
-      | isFalse neqaa' =>
-        apply isFalse; intro contra; cases contra <;> contradiction
-
-end Prod.Lex
-
-
 namespace Lean.Meta.DiscrTree
 
-namespace Key
-
--- TODO could be more efficient.
-protected def cmp (k l : Key s) : Ordering :=
-  if lt k l then
-    Ordering.lt
-  else if lt l k then
-    Ordering.gt
-  else
-    Ordering.eq
-
-instance : Ord (Key s) :=
-  ⟨Key.cmp⟩
-
-end Key
-
-namespace Trie
-
--- This is just a partial function, but Lean doesn't realise that its type is
--- inhabited.
-unsafe def foldMUnsafe [Monad m] (initialKeys : Array (Key s))
-    (f : σ → Array (Key s) → α → m σ) (init : σ) : Trie α s → m σ
-  | Trie.node vs children => do
-    let s ← vs.foldlM (init := init) λ s v => f s initialKeys v
-    children.foldlM (init := s) λ s (k, t) =>
-      t.foldMUnsafe (initialKeys.push k) f s
-
-@[implemented_by foldMUnsafe]
-opaque foldM [Monad m] (initalKeys : Array (Key s))
-    (f : σ → Array (Key s) → α → m σ) (init : σ) (t : Trie α s) : m σ :=
-  pure init
-
-@[inline]
-def fold (initialKeys : Array (Key s)) (f : σ → Array (Key s) → α → σ)
-    (init : σ) (t : Trie α s) : σ :=
-  Id.run $ t.foldM initialKeys (init := init) λ s k a => return f s k a
-
--- This is just a partial function, but Lean doesn't realise that its type is
--- inhabited.
-unsafe def foldValuesMUnsafe [Monad m] (f : σ → α → m σ) (init : σ) :
-    Trie α s → m σ
-| node vs children => do
-  let s ← vs.foldlM (init := init) f
-  children.foldlM (init := s) λ s (_, c) => c.foldValuesMUnsafe (init := s) f
-
-@[implemented_by foldValuesMUnsafe]
-opaque foldValuesM [Monad m] (f : σ → α → m σ) (init : σ) (t : Trie α s) :
-    m σ :=
-  pure init
-
-@[inline]
-def foldValues (f : σ → α → σ) (init : σ) (t : Trie α s) : σ :=
-  Id.run $ t.foldValuesM (init := init) f
-
-partial def size : Trie α s → Nat
-  | Trie.node vs children =>
-    children.foldl (init := vs.size) λ n (_, c) => n + size c
-
-partial def merge : Trie α s → Trie α s → Trie α s
-  | node vs₁ cs₁, node vs₂ cs₂ =>
-    node (mergeValues vs₁ vs₂) (mergeChildren cs₁ cs₂)
-  where
-    mergeValues (vs₁ vs₂ : Array α) : Array α :=
-      if vs₁.size > vs₂.size then vs₁ ++ vs₂ else vs₂ ++ vs₁
-
-    mergeChildren (cs₁ cs₂ : Array (Key s × Trie α s)) :
-        Array (Key s × Trie α s) :=
-      Array.mergeSortedMergingDuplicates
-        (ord := ⟨λ (k₁, _) (k₂, _) => compare k₁ k₂⟩) cs₁ cs₂
-        (λ (k₁, t₁) (_, t₂) => (k₁, merge t₁ t₂))
-
-end Trie
-
-@[inline]
-def foldM [Monad m] (f : σ → Array (Key s) → α → m σ) (init : σ)
-    (t : DiscrTree α s) : m σ :=
-  t.root.foldlM (init := init) λ s k t => t.foldM #[k] (init := s) f
-
-@[inline]
-def fold (f : σ → Array (Key s) → α → σ) (init : σ) (t : DiscrTree α s) : σ :=
-  Id.run $ t.foldM (init := init) λ s keys a => return f s keys a
-
-@[inline]
-def foldValuesM [Monad m] (f : σ → α → m σ) (init : σ) (t : DiscrTree α s) :
-    m σ :=
-  t.root.foldlM (init := init) λ s _ t => t.foldValuesM (init := s) f
-
-@[inline]
-def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α s) : σ :=
-  Id.run $ t.foldValuesM (init := init) f
-
-def values (t : DiscrTree α s) : Array α :=
-  t.foldValues (init := #[]) λ as a => as.push a
-
-def toArray (t : DiscrTree α s) : Array (Array (Key s) × α) :=
-  t.fold (init := #[]) λ as keys a => as.push (keys, a)
-
-def size (t : DiscrTree α s) : Nat :=
-  t.root.foldl (init := 0) λ n _ t => n + t.size
-
-@[inline]
-def merge [BEq α] (t u : DiscrTree α s) : DiscrTree α s :=
-  { root := t.root.merge u.root λ _ trie₁ trie₂ => trie₁.merge trie₂ }
-
 -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with
 -- `n` stars).
 def getConclusionKeys (type : Expr) :
@@ -577,7 +108,7 @@ def getConclusionKeys (type : Expr) :
 def getConstKeys (decl : Name) : MetaM (Array (Key s)) := do
   let (some info) ← getConst? decl
     | throwUnknownConstant decl
-  let arity := info.type.arity
+  let arity := info.type.forallArity
   let mut keys := Array.mkEmpty (arity + 1)
   keys := keys.push $ .const decl arity
   for _ in [0:arity] do
@@ -628,11 +159,11 @@ def simpEntries (thms : SimpTheorems) : Array SimpEntry :=
   thms.foldSimpEntries (init := #[]) λ s thm => s.push thm
 
 def merge (s t : SimpTheorems) : SimpTheorems := {
-    pre := s.pre.merge t.pre
-    post := s.post.merge t.post
+    pre := s.pre.mergePreservingDuplicates t.pre
+    post := s.post.mergePreservingDuplicates t.post
     lemmaNames := s.lemmaNames.merge t.lemmaNames
     toUnfold := s.toUnfold.merge t.toUnfold
-    toUnfoldThms := s.toUnfoldThms.merge t.toUnfoldThms
+    toUnfoldThms := s.toUnfoldThms.mergeWith t.toUnfoldThms
       (λ _ thms₁ _ => thms₁)
       -- We can ignore collisions here because the theorems should always be the
       -- same.
@@ -666,55 +197,6 @@ end Lean.Meta.SimpTheorems
 
 namespace Lean.Meta
 
-def unhygienic [Monad m] [MonadWithOptions m] (x : m α) : m α :=
-  withOptions (tactic.hygienic.set · false) x
-
--- Runs `tac` on `goal`, then on the subgoals created by `tac`, etc. Returns the
--- goals to which `tac` does not apply any more. If `tac` applies infinitely
--- often, `saturate1` diverges. If `tac` does not apply to `goal`, `none` is
--- returned.
-partial def saturate1 (goal : MVarId)
-    (tac : MVarId → MetaM (Option (Array MVarId))) :
-    MetaM (Option (Array MVarId)) := do
-  match ← tac goal with
-  | none => return none
-  | some goals => return some (← goals.forM go |>.run #[]).snd
-  where
-    go (goal : MVarId) : StateRefT (Array MVarId) MetaM Unit :=
-      withIncRecDepth do
-        match ← tac goal with
-        | none => modify λ s => s.push goal
-        | some goals => goals.forM go
-
-partial def _root_.Lean.MVarId.getMVarDependencies (mvarId : MVarId)
-    (includeDelayed := false) : MetaM (HashSet MVarId) :=
-  return (← go mvarId |>.run {}).snd
-  where
-    addMVars (e : Expr) : StateRefT (HashSet MVarId) MetaM Unit := do
-      let mvars ← getMVars e
-      let mut s ← get
-      set ({} : HashSet MVarId) -- Ensure that `s` is not shared.
-      for mvarId in mvars do
-        if ← pure includeDelayed <||> notM (mvarId.isDelayedAssigned) then
-          s := s.insert mvarId
-      set s
-      mvars.forM go
-
-    go (mvarId : MVarId) : StateRefT (HashSet MVarId) MetaM Unit :=
-      withIncRecDepth do
-        mvarId.instantiateMVars
-        let mdecl ← mvarId.getDecl
-        addMVars mdecl.type
-        for ldecl in mdecl.lctx do
-          addMVars ldecl.type
-          if let (some val) := ldecl.value? then
-            addMVars val
-        if let (some ass) ← getDelayedMVarAssignment? mvarId then
-          let pendingMVarId := ass.mvarIdPending
-          if ← notM pendingMVarId.isAssignedOrDelayedAssigned then
-            modify (·.insert pendingMVarId)
-          go pendingMVarId
-
 def matchAppOf (f : Expr) (e : Expr) : MetaM (Option (Array Expr)) := do
   let type ← inferType f
   let (mvars, _, _) ← forallMetaTelescope type
@@ -743,15 +225,3 @@ def runTermElabMAsCoreM (x : Elab.TermElabM α) : CoreM α :=
   runMetaMAsCoreM x.run'
 
 end Lean
-
-
-namespace Lean.Meta
-
-def mkFreshIdWithPrefix [Monad m] [MonadNameGenerator m] («prefix» : Name) :
-    m Name := do
-  let ngen ← getNGen
-  let r := { ngen with namePrefix := «prefix» }.curr
-  setNGen ngen.next
-  pure r
-
-end Lean.Meta
diff --git a/Aesop/Util/UnorderedArraySet.lean b/Aesop/Util/UnorderedArraySet.lean
index 98222fa7..499fedbf 100644
--- a/Aesop/Util/UnorderedArraySet.lean
+++ b/Aesop/Util/UnorderedArraySet.lean
@@ -46,7 +46,7 @@ set_option linter.unusedVariables false in
 /-- O(n*log(n)) -/
 protected def ofArray [ord : Ord α] [Inhabited α] (xs : Array α) :
     UnorderedArraySet α :=
-  ⟨xs.deduplicate⟩
+  ⟨xs.sortAndDeduplicate⟩
 
 /-- O(n^2) -/
 protected def ofArraySlow (xs : Array α) : UnorderedArraySet α :=
@@ -76,7 +76,7 @@ def filter (p : α → Bool) (s : UnorderedArraySet α) : UnorderedArraySet α :
 
 /-- O(n*m) -/
 def merge (s t : UnorderedArraySet α) : UnorderedArraySet α :=
-  ⟨s.rep.mergeUnsortedFilteringDuplicates t.rep⟩
+  ⟨s.rep.mergeUnsortedDeduplicating t.rep⟩
 
 instance : Append (UnorderedArraySet α) :=
   ⟨merge⟩
diff --git a/lake-manifest.json b/lake-manifest.json
index 22a32cdd..39a40cbd 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,6 +4,6 @@
  [{"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "2919713bde15d55e3ea3625a03546531283bcb54",
+    "rev": "fde95b16907bf38ea3f310af406868fc6bcf48d1",
     "name": "std",
     "inputRev?": "main"}}]}
diff --git a/lean-toolchain b/lean-toolchain
index 296592d5..b20d041b 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-12-23
+leanprover/lean4:nightly-2023-01-10
diff --git a/tests/run/List.lean b/tests/run/List.lean
index 27b788c1..be65e98f 100644
--- a/tests/run/List.lean
+++ b/tests/run/List.lean
@@ -836,7 +836,7 @@ theorem map_reverse (f : α → β) (l : List α) : map f (reverse l) = reverse
 -- attribute [-simp] map_reverseAux
 theorem map_reverse_core (f : α → β) (l₁ l₂ : List α) :
   map f (reverseAux l₁ l₂) = reverseAux (map f l₁) (map f l₂) := by
-  aesop
+  aesop (add norm simp reverse_map)
 
 attribute [-simp] mem_reverse
 @[simp] theorem X.mem_reverse {a : α} {l : List α} : a ∈ reverse l ↔ a ∈ l := by