refactor: replace Array.eraseIdx' with Array.size_feraseIdx

`Array.eraseIdx'` which was just `Array.feraseIdx` wrapped in a subtype.
`Array.size_feraseIdx` proves the property as a standalone theorem.

Author: timotree3

src/Init/Data/Array/Basic.lean

@@ -760,9 +760,6 @@ theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size =
 def eraseIdx (a : Array α) (i : Nat) : Array α :=
   if h : i < a.size then a.feraseIdx ⟨i, h⟩ else a
 
-def eraseIdx' (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
-  ⟨a.feraseIdx i, size_feraseIdx a i⟩
-
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
   match as.indexOf? a with
   | none   => as

src/Lean/Data/PersistentHashMap.lean

@@ -226,8 +226,10 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
-      let ⟨keys', keq⟩ := keys.eraseIdx' idx
-      let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.ndrec idx heq)
+      let keys' := keys.feraseIdx idx
+      have keq := keys.size_feraseIdx idx
+      let vals' := vals.feraseIdx (Eq.ndrec idx heq)
+      have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
       (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
     | none     => (n, false)