feat: relate Array.eraseIdx with List.eraseIdx (#5952)

src/Init/Data/Array/Lemmas.lean

@@ -10,6 +10,7 @@ import Init.Data.List.Monadic
 import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
+import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
 import Init.Data.List.OfFn
 import Init.Data.Array.Mem
@@ -1460,6 +1461,10 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
+theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
+    a.feraseIdx i = a.eraseIdx i.1 := by
+  simp [eraseIdx]
+
 end Array
 
 open Array
@@ -1611,7 +1616,7 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   apply ext'
   simp
 
-@[simp] theorem toArray_extract (l : List α) (start stop : Nat) :
+@[simp] theorem extract_toArray (l : List α) (start stop : Nat) :
     l.toArray.extract start stop = ((l.drop start).take (stop - start)).toArray := by
   apply ext'
   simp
@@ -1651,6 +1656,32 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
+@[simp] theorem feraseIdx_toArray (l : List α) (i : Fin l.toArray.size) :
+    l.toArray.feraseIdx i = (l.eraseIdx i).toArray := by
+  rw [feraseIdx]
+  split <;> rename_i h
+  · rw [feraseIdx_toArray]
+    simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
+    rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
+    simp
+  · rcases i with ⟨i, w⟩
+    simp at h w
+    have t : i = l.length - 1 := by omega
+    simp [t]
+termination_by l.length - i
+decreasing_by
+  rename_i h
+  simp at h
+  simp
+  omega
+
+@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) :
+    l.toArray.eraseIdx i = (l.eraseIdx i).toArray := by
+  rw [Array.eraseIdx]
+  split
+  · simp
+  · simp_all [eraseIdx_eq_self.2]
+
 end List
 
 namespace Array
@@ -1665,6 +1696,16 @@ namespace Array
     (as.takeWhile p).toList = as.toList.takeWhile p := by
   induction as; simp
 
+@[simp] theorem toList_feraseIdx (as : Array α) (i : Fin as.size) :
+    (as.feraseIdx i).toList = as.toList.eraseIdx i.1 := by
+  induction as
+  simp
+
+@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) :
+    (as.eraseIdx i).toList = as.toList.eraseIdx i := by
+  induction as
+  simp
+
 end Array
 
 /-! ### Deprecations -/

src/Init/Data/List/Nat/Erase.lean

@@ -64,3 +64,82 @@ theorem getElem_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : j < (l.era
     (l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
   rw [getElem_eraseIdx, dif_neg]
   omega
+
+theorem eraseIdx_set_eq {l : List α} {i : Nat} {a : α} :
+    (l.set i a).eraseIdx i = l.eraseIdx i := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    rw [getElem_eraseIdx, getElem_eraseIdx]
+    split <;>
+    · rw [getElem_set_ne]
+      omega
+
+theorem eraseIdx_set_lt {l : List α} {i : Nat} {j : Nat} {a : α} (h : j < i) :
+    (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    simp only [length_eraseIdx, length_set] at h₁
+    simp only [getElem_eraseIdx, getElem_set]
+    split
+    · split
+      · split
+        · rfl
+        · omega
+      · split
+        · omega
+        · rfl
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : i - 1 ≠ n := by omega
+        simp [t]
+
+theorem eraseIdx_set_gt {l : List α} {i : Nat} {j : Nat} {a : α} (h : i < j) :
+    (l.set i a).eraseIdx j = (l.eraseIdx j).set i a := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    simp only [length_eraseIdx, length_set] at h₁
+    simp only [getElem_eraseIdx, getElem_set]
+    split
+    · rfl
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : i ≠ n := by omega
+        simp [t]
+
+@[simp] theorem set_getElem_succ_eraseIdx_succ
+    {l : List α} {i : Nat} (h : i + 1 < l.length) :
+    (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i := by
+  apply ext_getElem
+  · simp only [length_set, length_eraseIdx, h, ↓reduceIte]
+    rw [if_pos]
+    omega
+  · intro n h₁ h₂
+    simp [getElem_set, getElem_eraseIdx]
+    split
+    · split
+      · omega
+      · simp_all
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : ¬ n < i := by omega
+        simp [t]
+
+@[simp] theorem eraseIdx_length_sub_one (l : List α) :
+    (l.eraseIdx (l.length - 1)) = l.dropLast := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+    omega
+  · intro n h₁ h₂
+    rw [getElem_eraseIdx_of_lt, getElem_dropLast]
+    simp_all
+
+end List