diff --git a/src/Std/Data/BinomialHeap.lean b/src/Std/Data/BinomialHeap.lean
index e231d979f9..00bf4cd57e 100644
--- a/src/Std/Data/BinomialHeap.lean
+++ b/src/Std/Data/BinomialHeap.lean
@@ -51,7 +51,7 @@ def singleton (a : α) : Heap α :=
 
 -- Merge two forests of binomial trees. The forests are assumed to be ordered
 -- by rank and `mergeNodes` maintains this invariant.
-@[specialize] partial def mergeNodes (le : α → α → Bool) : List (HeapNode α) → List (HeapNode α) → List (HeapNode α)
+@[specialize] def mergeNodes (le : α → α → Bool) : List (HeapNode α) → List (HeapNode α) → List (HeapNode α)
   | [], h  => h
   | h,  [] => h
   | f@(h₁ :: t₁), s@(h₂ :: t₂) =>
@@ -64,6 +64,8 @@ def singleton (a : α) : Heap α :=
         if r != hRank t₂ then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
       else
         if r != hRank t₂ then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂
+termination_by _ h₁ h₂ => h₁.length + h₂.length
+decreasing_by simp_wf; simp_arith [*]
 
 @[specialize] def merge (le : α → α → Bool) : Heap α → Heap α → Heap α
   | heap h₁, heap h₂ => heap (mergeNodes le h₁ h₂)
diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean
index 160223408d..c0edcd82c8 100644
--- a/src/Std/Data/HashMap.lean
+++ b/src/Std/Data/HashMap.lean
@@ -76,8 +76,7 @@ def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
     let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     (buckets.val.uget i h).contains a
 
--- TODO: remove `partial` by using well-founded recursion
-partial def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
+def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
   if h : i < source.size then
      let idx : Fin source.size := ⟨i, h⟩
      let es  : AssocList α β   := source.get idx
@@ -86,6 +85,7 @@ partial def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else target
+termination_by _ i source _ => source.size - i
 
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let nbuckets := buckets.val.size * 2
diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean
index a23aa6af23..df611a6dca 100644
--- a/src/Std/Data/HashSet.lean
+++ b/src/Std/Data/HashSet.lean
@@ -58,8 +58,7 @@ def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
     let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     (buckets.val.uget i h).contains a
 
--- TODO: remove `partial` by using well-founded recursion
-partial def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
+def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
   if h : i < source.size then
      let idx : Fin source.size := ⟨i, h⟩
      let es  : List α   := source.get idx
@@ -67,7 +66,9 @@ partial def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (targ
      let source                := source.set idx []
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
-  else target
+  else
+    target
+termination_by _ i source _ => source.size - i
 
 def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
   let nbuckets := buckets.val.size * 2