diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index 2697f9e30b..c23a9783ca 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -472,8 +472,8 @@ partial def eraseIdxSzAux {α} (a : Array α) : ∀ (i : Nat) (r : Array α), r.
     ⟨r.pop, (szPopEq r).trans (heq ▸ rfl)⟩
 end
 
-def eraseIdxSz {α} (a : Array α) (i : Nat) : { r : Array α // r.size = a.size - 1 } :=
-eraseIdxSzAux a i a rfl
+def eraseIdx' {α} (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
+eraseIdxSzAux a (i.val + 1) a rfl
 
 end Array
 
diff --git a/library/init/data/persistenthashmap/basic.lean b/library/init/data/persistenthashmap/basic.lean
index eb278fcbe1..8e58d6e768 100644
--- a/library/init/data/persistenthashmap/basic.lean
+++ b/library/init/data/persistenthashmap/basic.lean
@@ -175,8 +175,8 @@ partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β ×
 | n@(Node.collision keys vals heq) _ k :=
   match keys.indexOf k with
   | some idx =>
-    let ⟨keys', keq⟩ := keys.eraseIdxSz idx.val;
-    let ⟨vals', veq⟩ := vals.eraseIdxSz idx.val;
+    let ⟨keys', keq⟩ := keys.eraseIdx' idx;
+    let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.rec idx heq);
     have keys.size - 1 = vals.size - 1 from heq ▸ rfl;
     (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
   | none     => (n, false)