From 2385abc282e2afd24b784b3ed2371a096f7d859e Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Tue, 4 Feb 2025 23:23:27 +1100
Subject: [PATCH] feat: align List/Array/Vector.insertIdx lemmas (#6948)

This PR completes the alignment of `List/Array/Vectors` lemmas for
`insertIdx`.
---
 src/Init/Data/Array.lean              |   1 +
 src/Init/Data/Array/Basic.lean        |   6 +-
 src/Init/Data/Array/InsertIdx.lean    | 129 ++++++++++++++++++++++++++
 src/Init/Data/List/Nat/InsertIdx.lean |  13 ++-
 src/Init/Data/List/Nat/TakeDrop.lean  |  13 ++-
 src/Init/Data/List/TakeDrop.lean      |   3 +
 src/Init/Data/List/ToArray.lean       |  62 +++++++++++++
 src/Init/Data/Vector.lean             |   1 +
 src/Init/Data/Vector/Basic.lean       |  14 +++
 src/Init/Data/Vector/InsertIdx.lean   | 126 +++++++++++++++++++++++++
 src/Init/Data/Vector/Lemmas.lean      |  21 +++++
 11 files changed, 384 insertions(+), 5 deletions(-)
 create mode 100644 src/Init/Data/Array/InsertIdx.lean
 create mode 100644 src/Init/Data/Vector/InsertIdx.lean

diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean
index 2a91c25595..c31c9ebcf9 100644
--- a/src/Init/Data/Array.lean
+++ b/src/Init/Data/Array.lean
@@ -26,3 +26,4 @@ import Init.Data.Array.Lex
 import Init.Data.Array.Range
 import Init.Data.Array.Erase
 import Init.Data.Array.Zip
+import Init.Data.Array.InsertIdx
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index f656f988a0..c0c37b8299 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -953,7 +953,11 @@ def eraseP (as : Array α) (p : α → Bool) : Array α :=
   | none   => as
   | some i => as.eraseIdx i
 
-/-- Insert element `a` at position `i`. -/
+/-- Insert element `a` at position `i`.
+
+This function takes worst case O(n) time because
+it has to swap the inserted element into place.
+-/
 @[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   loop (as : Array α) (j : Fin as.size) :=
diff --git a/src/Init/Data/Array/InsertIdx.lean b/src/Init/Data/Array/InsertIdx.lean
new file mode 100644
index 0000000000..f2a35a8b28
--- /dev/null
+++ b/src/Init/Data/Array/InsertIdx.lean
@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.InsertIdx
+
+/-!
+# insertIdx
+
+Proves various lemmas about `Array.insertIdx`.
+-/
+
+open Function
+
+open Nat
+
+namespace Array
+
+universe u
+
+variable {α : Type u}
+
+section InsertIdx
+
+variable {a : α}
+
+@[simp] theorem toList_insertIdx (a : Array α) (i x) (h) :
+    (a.insertIdx i x h).toList = a.toList.insertIdx i x := by
+  rcases a with ⟨a⟩
+  simp
+
+@[simp]
+theorem insertIdx_zero (s : Array α) (x : α) : s.insertIdx 0 x = #[x] ++ s := by
+  cases s
+  simp
+
+@[simp] theorem size_insertIdx {as : Array α} (h : n ≤ as.size) : (as.insertIdx n a).size = as.size + 1 := by
+  cases as
+  simp [List.length_insertIdx, h]
+
+theorem eraseIdx_insertIdx (i : Nat) (l : Array α) (h : i ≤ l.size) :
+    (l.insertIdx i a).eraseIdx i (by simp; omega) = l := by
+  cases l
+  simp_all
+
+theorem insertIdx_eraseIdx_of_ge {as : Array α}
+    (w₁ : i < as.size) (w₂ : j ≤ (as.eraseIdx i).size) (h : i ≤ j) :
+    (as.eraseIdx i).insertIdx j a =
+      (as.insertIdx (j + 1) a (by simp at w₂; omega)).eraseIdx i (by simp_all; omega) := by
+  cases as
+  simpa using List.insertIdx_eraseIdx_of_ge _ _ _ (by simpa) (by simpa)
+
+theorem insertIdx_eraseIdx_of_le {as : Array α}
+    (w₁ : i < as.size) (w₂ : j ≤ (as.eraseIdx i).size) (h : j ≤ i) :
+    (as.eraseIdx i).insertIdx j a =
+      (as.insertIdx j a (by simp at w₂; omega)).eraseIdx (i + 1) (by simp_all) := by
+  cases as
+  simpa using List.insertIdx_eraseIdx_of_le _ _ _ (by simpa) (by simpa)
+
+theorem insertIdx_comm (a b : α) (i j : Nat) (l : Array α) (_ : i ≤ j) (_ : j ≤ l.size) :
+    (l.insertIdx i a).insertIdx (j + 1) b (by simpa) =
+      (l.insertIdx j b).insertIdx i a (by simp; omega) := by
+  cases l
+  simpa using List.insertIdx_comm a b i j _ (by simpa) (by simpa)
+
+theorem mem_insertIdx {l : Array α} {h : i ≤ l.size} : a ∈ l.insertIdx i b h ↔ a = b ∨ a ∈ l := by
+  cases l
+  simpa using List.mem_insertIdx (by simpa)
+
+@[simp]
+theorem insertIdx_size_self (l : Array α) (x : α) : l.insertIdx l.size x = l.push x := by
+  cases l
+  simp
+
+theorem getElem_insertIdx {as : Array α} {x : α} {i k : Nat} (w : i ≤ as.size) (h : k < (as.insertIdx i x).size) :
+    (as.insertIdx i x)[k] =
+      if h₁ : k < i then
+        as[k]'(by simp [size_insertIdx] at h; omega)
+      else
+        if h₂ : k = i then
+          x
+        else
+          as[k-1]'(by simp [size_insertIdx] at h; omega) := by
+  cases as
+  simp [List.getElem_insertIdx, w]
+
+theorem getElem_insertIdx_of_lt {as : Array α} {x : α} {i k : Nat} (w : i ≤ as.size) (h : k < i) :
+    (as.insertIdx i x)[k]'(by simp; omega) = as[k] := by
+  simp [getElem_insertIdx, w, h]
+
+theorem getElem_insertIdx_self {as : Array α} {x : α} {i : Nat} (w : i ≤ as.size) :
+    (as.insertIdx i x)[i]'(by simp; omega) = x := by
+  simp [getElem_insertIdx, w]
+
+theorem getElem_insertIdx_of_gt {as : Array α} {x : α} {i k : Nat} (w : k ≤ as.size) (h : k > i) :
+    (as.insertIdx i x)[k]'(by simp; omega) = as[k - 1]'(by omega) := by
+  simp [getElem_insertIdx, w, h]
+  rw [dif_neg (by omega), dif_neg (by omega)]
+
+theorem getElem?_insertIdx {l : Array α} {x : α} {i k : Nat} (h : i ≤ l.size) :
+    (l.insertIdx i x)[k]? =
+      if k < i then
+        l[k]?
+      else
+        if k = i then
+          if k ≤ l.size then some x else none
+        else
+          l[k-1]? := by
+  cases l
+  simp [List.getElem?_insertIdx, h]
+
+theorem getElem?_insertIdx_of_lt {l : Array α} {x : α} {i k : Nat} (w : i ≤ l.size) (h : k < i) :
+    (l.insertIdx i x)[k]? = l[k]? := by
+  rw [getElem?_insertIdx, if_pos h]
+
+theorem getElem?_insertIdx_self {l : Array α} {x : α} {i : Nat} (w : i ≤ l.size) :
+    (l.insertIdx i x)[i]? = some x := by
+  rw [getElem?_insertIdx, if_neg (by omega), if_pos rfl, if_pos w]
+
+theorem getElem?_insertIdx_of_ge {l : Array α} {x : α} {i k : Nat} (w : i < k) (h : k ≤ l.size) :
+    (l.insertIdx i x)[k]? = l[k - 1]? := by
+  rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]
+
+end InsertIdx
+
+end Array
diff --git a/src/Init/Data/List/Nat/InsertIdx.lean b/src/Init/Data/List/Nat/InsertIdx.lean
index ab86095a05..9d6672641e 100644
--- a/src/Init/Data/List/Nat/InsertIdx.lean
+++ b/src/Init/Data/List/Nat/InsertIdx.lean
@@ -52,6 +52,7 @@ theorem length_insertIdx_of_le_length (h : n ≤ length as) : length (insertIdx
 theorem length_insertIdx_of_length_lt (h : length as < n) : length (insertIdx n a as) = length as := by
   simp [length_insertIdx, h]
 
+@[simp]
 theorem eraseIdx_insertIdx (n : Nat) (l : List α) : (l.insertIdx n a).eraseIdx n = l := by
   rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]
   exact modifyTailIdx_id _ _
@@ -150,7 +151,7 @@ theorem getElem_insertIdx_self {l : List α} {x : α} {n : Nat} (hn : n < (inser
     · simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_lt_add_iff_right] at hn ih
       simpa using ih hn
 
-theorem getElem_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (hn : n + 1 ≤ k)
+theorem getElem_insertIdx_of_gt {l : List α} {x : α} {n k : Nat} (hn : n < k)
     (hk : k < (insertIdx n x l).length) :
     (insertIdx n x l)[k] = l[k - 1]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
   induction l generalizing n k with
@@ -177,6 +178,9 @@ theorem getElem_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (hn : n + 1 
         | zero => omega
         | succ k => simp
 
+@[deprecated getElem_insertIdx_of_gt (since := "2025-02-04")]
+abbrev getElem_insertIdx_of_ge := @getElem_insertIdx_of_gt
+
 theorem getElem_insertIdx {l : List α} {x : α} {n k : Nat} (h : k < (insertIdx n x l).length) :
     (insertIdx n x l)[k] =
       if h₁ : k < n then
@@ -191,7 +195,7 @@ theorem getElem_insertIdx {l : List α} {x : α} {n k : Nat} (h : k < (insertIdx
   · split <;> rename_i h₂
     · subst h₂
       rw [getElem_insertIdx_self h]
-    · rw [getElem_insertIdx_of_ge (by omega)]
+    · rw [getElem_insertIdx_of_gt (by omega)]
 
 theorem getElem?_insertIdx {l : List α} {x : α} {n k : Nat} :
     (insertIdx n x l)[k]? =
@@ -233,10 +237,13 @@ theorem getElem?_insertIdx_self {l : List α} {x : α} {n : Nat} :
   rw [getElem?_insertIdx, if_neg (by omega)]
   simp
 
-theorem getElem?_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (h : n + 1 ≤ k) :
+theorem getElem?_insertIdx_of_gt {l : List α} {x : α} {n k : Nat} (h : n < k) :
     (insertIdx n x l)[k]? = l[k - 1]? := by
   rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]
 
+@[deprecated getElem?_insertIdx_of_gt (since := "2025-02-04")]
+abbrev getElem?_insertIdx_of_ge := @getElem?_insertIdx_of_gt
+
 end InsertIdx
 
 end List
diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index f97b8951f8..ffc109e56d 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -101,7 +101,7 @@ theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m)
   | succ n, succ m, a :: l => by
     simp only [take, succ_min_succ, take_take n m l]
 
-theorem take_set_of_lt (a : α) {n m : Nat} (l : List α) (h : m < n) :
+theorem take_set_of_le (a : α) {n m : Nat} (l : List α) (h : m ≤ n) :
     (l.set n a).take m = l.take m :=
   List.ext_getElem? fun i => by
     rw [getElem?_take, getElem?_take]
@@ -109,6 +109,9 @@ theorem take_set_of_lt (a : α) {n m : Nat} (l : List α) (h : m < n) :
     · next h' => rw [getElem?_set_ne (by omega)]
     · rfl
 
+@[deprecated take_set_of_le (since := "2025-02-04")]
+abbrev take_set_of_lt := @take_set_of_le
+
 @[simp] theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
   | n, 0 => by simp [Nat.min_zero]
   | 0, m => by simp [Nat.zero_min]
@@ -165,6 +168,10 @@ theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.dro
 theorem take_one {l : List α} : l.take 1 = l.head?.toList := by
   induction l <;> simp
 
+theorem take_eq_append_getElem_of_pos {n} {l : List α} (h₁ : 0 < n) (h₂ : n < l.length) : l.take n = l.take (n - 1) ++ [l[n - 1]] :=
+  match n, h₁ with
+  | n + 1, _ => take_succ_eq_append_getElem (n := n) (by omega)
+
 theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
     (l.take n).dropLast = l.take (n - 1) := by
   simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, Nat.min_eq_left, take_take, sub_le]
@@ -359,6 +366,10 @@ theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m -
     congr 1
     omega
 
+@[simp] theorem drop_take_self : drop n (take n l) = [] := by
+  rw [drop_take]
+  simp
+
 theorem take_reverse {α} {xs : List α} {n : Nat} :
     xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
   by_cases h : n ≤ xs.length
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index 4a87969b88..4ec41f8580 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -183,6 +183,9 @@ theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
     (l.take i) ++ [l[i]] = l.take (i+1) := by
   simpa using take_concat_get l i h
 
+theorem take_succ_eq_append_getElem {n} {l : List α} (h : n < l.length) : l.take (n + 1) = l.take n ++ [l[n]] :=
+  (take_append_getElem _ _ h).symm
+
 @[simp] theorem take_append_getLast (l : List α) (h : l ≠ []) :
     (l.take (l.length - 1)) ++ [l.getLast h] = l := by
   rw [getLast_eq_getElem]
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
index c620ef6fe5..5ed2e511c6 100644
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Data.List.Impl
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
+import Init.Data.List.Nat.InsertIdx
 import Init.Data.Array.Lex.Basic
 
 /-! ### Lemmas about `List.toArray`.
@@ -555,4 +556,65 @@ decreasing_by
   rw [idxOf?_eq_map_finIdxOf?_val]
   split <;> simp_all
 
+private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j < l.toArray.size) (h : i ≤ j) :
+    insertIdx.loop i l.toArray ⟨j, hj⟩ = (l.take i ++ l[j] :: (l.take j).drop i ++ l.drop (j + 1)).toArray := by
+  rw [insertIdx.loop]
+  simp only [size_toArray] at hj
+  split <;> rename_i h'
+  · simp only at h'
+    have w : j - 1 + 1 = j := by omega
+    simp only [append_assoc, cons_append]
+    rw [insertIdx_loop_toArray _ _ _ _ (by omega)]
+    simp only [swap_toArray, w, append_assoc, cons_append, mk.injEq]
+    rw [List.take_set_of_le _ _ (by omega)]
+    rw [List.drop_eq_getElem_cons (n := j) (by simpa)]
+    rw [List.getElem_set_self]
+    rw [List.drop_set_of_lt _ _ (by omega)]
+    rw [List.drop_set_of_lt _ _ (by omega)]
+    rw [List.getElem_set_ne (by omega)]
+    rw [List.getElem_set_self]
+    rw [List.take_set_of_le (m := j - 1) _ _ (by omega)]
+    rw [List.take_set_of_le (m := j - 1) _ _ (by omega)]
+    rw [List.take_eq_append_getElem_of_pos (n := j) (l := l) (by omega) hj]
+    rw [List.drop_append_of_le_length (by simp; omega)]
+    simp only [append_assoc, cons_append, nil_append, append_cancel_right_eq]
+    cases i with
+    | zero => simp
+    | succ i => rw [List.take_set_of_le _ _ (by omega)]
+  · simp only [Nat.not_lt] at h'
+    have : i = j := by omega
+    subst this
+    simp
+
+@[simp] theorem insertIdx_toArray (l : List α) (i : Nat) (a : α) (h : i ≤ l.toArray.size):
+    l.toArray.insertIdx i a = (l.insertIdx i a).toArray := by
+  rw [Array.insertIdx]
+  rw [insertIdx_loop_toArray (h := h)]
+  ext j h₁ h₂
+  · simp at h
+    simp [length_insertIdx, h]
+    omega
+  · simp [length_insertIdx] at h₁ h₂
+    simp [getElem_insertIdx]
+    split <;> rename_i h₃
+    · rw [getElem_append_left (by simp; split at h₂ <;> omega)]
+      simp only [getElem_take]
+      rw [getElem_append_left]
+    · rw [getElem_append_right (by simp; omega)]
+      rw [getElem_cons]
+      simp
+      split <;> rename_i h₄
+      · rw [dif_pos (by omega)]
+      · rw [dif_neg (by omega)]
+        congr
+        omega
+
+@[simp] theorem insertIdxIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
+    l.toArray.insertIdxIfInBounds i a = (l.insertIdx i a).toArray := by
+  rw [Array.insertIdxIfInBounds]
+  split <;> rename_i h'
+  · simp
+  · simp only [size_toArray, Nat.not_le] at h'
+    rw [List.insertIdx_of_length_lt (h := h')]
+
 end List
diff --git a/src/Init/Data/Vector.lean b/src/Init/Data/Vector.lean
index dfd52707c5..194dd6db36 100644
--- a/src/Init/Data/Vector.lean
+++ b/src/Init/Data/Vector.lean
@@ -15,3 +15,4 @@ import Init.Data.Vector.OfFn
 import Init.Data.Vector.Range
 import Init.Data.Vector.Erase
 import Init.Data.Vector.Monadic
+import Init.Data.Vector.InsertIdx
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 3b156f81da..8da7af928e 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -7,6 +7,7 @@ Authors: Shreyas Srinivas, François G. Dorais, Kim Morrison
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Array.MapIdx
+import Init.Data.Array.InsertIdx
 import Init.Data.Range
 import Init.Data.Stream
 
@@ -355,6 +356,19 @@ instance [BEq α] : BEq (Vector α n) where
     have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
     panic! "index out of bounds"
 
+/-- Insert an element into a vector using a `Nat` index and a tactic provided proof. -/
+@[inline] def insertIdx (v : Vector α n) (i : Nat) (x : α) (h : i ≤ n := by get_elem_tactic) :
+    Vector α (n+1) :=
+  ⟨v.toArray.insertIdx i x (v.size_toArray.symm ▸ h), by simp [Array.size_insertIdx]⟩
+
+/-- Insert an element into a vector using a `Nat` index. Panics if the index is out of bounds. -/
+@[inline] def insertIdx! (v : Vector α n) (i : Nat) (x : α) : Vector α (n+1) :=
+  if _ : i ≤ n then
+    v.insertIdx i x
+  else
+    have : Inhabited (Vector α (n+1)) := ⟨v.push x⟩
+    panic! "index out of bounds"
+
 /-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
 @[inline] def tail (v : Vector α n) : Vector α (n-1) :=
   if _ : 0 < n then
diff --git a/src/Init/Data/Vector/InsertIdx.lean b/src/Init/Data/Vector/InsertIdx.lean
new file mode 100644
index 0000000000..27dfe5a661
--- /dev/null
+++ b/src/Init/Data/Vector/InsertIdx.lean
@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Vector.Lemmas
+import Init.Data.Array.InsertIdx
+
+/-!
+# insertIdx
+
+Proves various lemmas about `Vector.insertIdx`.
+-/
+
+open Function
+
+open Nat
+
+namespace Vector
+
+universe u
+
+variable {α : Type u}
+
+section InsertIdx
+
+variable {a : α}
+
+@[simp]
+theorem insertIdx_zero (s : Vector α n) (x : α) : s.insertIdx 0 x = (#v[x] ++ s).cast (by omega) := by
+  cases s
+  simp
+
+theorem eraseIdx_insertIdx (i : Nat) (l : Vector α n) (h : i ≤ n) :
+    (l.insertIdx i a).eraseIdx i = l := by
+  rcases l with ⟨l, rfl⟩
+  simp_all [Array.eraseIdx_insertIdx]
+
+theorem insertIdx_eraseIdx_of_ge {as : Vector α n}
+    (w₁ : i < n) (w₂ : j ≤ n - 1) (h : i ≤ j) :
+    (as.eraseIdx i).insertIdx j a =
+      ((as.insertIdx (j + 1) a).eraseIdx i).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simpa using Array.insertIdx_eraseIdx_of_ge (by simpa) (by simpa) (by simpa)
+
+theorem insertIdx_eraseIdx_of_le {as : Vector α n}
+    (w₁ : i < n) (w₂ : j ≤ n - 1) (h : j ≤ i) :
+    (as.eraseIdx i).insertIdx j a =
+      ((as.insertIdx j a).eraseIdx (i + 1)).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simpa using Array.insertIdx_eraseIdx_of_le (by simpa) (by simpa) (by simpa)
+
+theorem insertIdx_comm (a b : α) (i j : Nat) (l : Vector α n) (_ : i ≤ j) (_ : j ≤ n) :
+    (l.insertIdx i a).insertIdx (j + 1) b =
+      (l.insertIdx j b).insertIdx i a := by
+  rcases l with ⟨l, rfl⟩
+  simpa using Array.insertIdx_comm a b i j _ (by simpa) (by simpa)
+
+theorem mem_insertIdx {l : Vector α n} {h : i ≤ n} : a ∈ l.insertIdx i b h ↔ a = b ∨ a ∈ l := by
+  rcases l with ⟨l, rfl⟩
+  simpa using Array.mem_insertIdx
+
+@[simp]
+theorem insertIdx_size_self (l : Vector α n) (x : α) : l.insertIdx n x = l.push x := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+theorem getElem_insertIdx {as : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < n + 1) :
+    (as.insertIdx i x)[k] =
+      if h₁ : k < i then
+        as[k]
+      else
+        if h₂ : k = i then
+          x
+        else
+          as[k-1] := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.getElem_insertIdx, w]
+
+theorem getElem_insertIdx_of_lt {as : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < i) :
+    (as.insertIdx i x)[k] = as[k] := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.getElem_insertIdx, w, h]
+
+theorem getElem_insertIdx_self {as : Vector α n} {x : α} {i : Nat} (w : i ≤ n) :
+    (as.insertIdx i x)[i] = x := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.getElem_insertIdx, w]
+
+theorem getElem_insertIdx_of_gt {as : Vector α n} {x : α} {i k : Nat} (w : k ≤ n) (h : k > i) :
+    (as.insertIdx i x)[k] = as[k - 1] := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.getElem_insertIdx, w, h]
+  rw [dif_neg (by omega), dif_neg (by omega)]
+
+theorem getElem?_insertIdx {l : Vector α n} {x : α} {i k : Nat} (h : i ≤ n) :
+    (l.insertIdx i x)[k]? =
+      if k < i then
+        l[k]?
+      else
+        if k = i then
+          if k ≤ l.size then some x else none
+        else
+          l[k-1]? := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.getElem?_insertIdx, h]
+
+theorem getElem?_insertIdx_of_lt {l : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < i) :
+    (l.insertIdx i x)[k]? = l[k]? := by
+  rcases l with ⟨l, rfl⟩
+  rw [getElem?_insertIdx, if_pos h]
+
+theorem getElem?_insertIdx_self {l : Vector α n} {x : α} {i : Nat} (w : i ≤ n) :
+    (l.insertIdx i x)[i]? = some x := by
+  rcases l with ⟨l, rfl⟩
+  rw [getElem?_insertIdx, if_neg (by omega), if_pos rfl, if_pos w]
+
+theorem getElem?_insertIdx_of_ge {l : Vector α n} {x : α} {i k : Nat} (w : i < k) (h : k ≤ n) :
+    (l.insertIdx i x)[k]? = l[k - 1]? := by
+  rcases l with ⟨l, rfl⟩
+  rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]
+
+end InsertIdx
+
+end Vector
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 45edc49dcc..89058e8a0c 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -95,6 +95,13 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
     (Vector.mk a h).eraseIdx! i = Vector.mk (a.eraseIdx i) (by simp [h, hi]) := by
   simp [Vector.eraseIdx!, hi]
 
+@[simp] theorem insertIdx_mk (a : Array α) (h : a.size = n) (i x) (h') :
+    (Vector.mk a h).insertIdx i x h' = Vector.mk (a.insertIdx i x) (by simp [h, h']) := rfl
+
+@[simp] theorem insertIdx!_mk (a : Array α) (h : a.size = n) (i x) (hi : i ≤ n) :
+    (Vector.mk a h).insertIdx! i x = Vector.mk (a.insertIdx i x) (by simp [h, hi]) := by
+  simp [Vector.insertIdx!, hi]
+
 @[simp] theorem cast_mk (a : Array α) (h : a.size = n) (h' : n = m) :
     (Vector.mk a h).cast h' = Vector.mk a (by simp [h, h']) := rfl
 
@@ -272,6 +279,13 @@ abbrev zipWithIndex_mk := @zipIdx_mk
     (a.eraseIdx! i).toArray = a.toArray.eraseIdx! i := by
   cases a; simp_all [Array.eraseIdx!]
 
+@[simp] theorem toArray_insertIdx (a : Vector α n) (i x) (h) :
+    (a.insertIdx i x h).toArray = a.toArray.insertIdx i x (by simp [h]) := rfl
+
+@[simp] theorem toArray_insertIdx! (a : Vector α n) (i x) (hi : i ≤ n) :
+    (a.insertIdx! i x).toArray = a.toArray.insertIdx! i x := by
+  cases a; simp_all [Array.insertIdx!]
+
 @[simp] theorem toArray_cast (a : Vector α n) (h : n = m) :
     (a.cast h).toArray = a.toArray := rfl
 
@@ -494,6 +508,13 @@ theorem toList_eraseIdx (a : Vector α n) (i) (h) :
     (a.eraseIdx! i).toList = a.toList.eraseIdx i := by
   cases a; simp_all [Array.eraseIdx!]
 
+theorem toList_insertIdx (a : Vector α n) (i x) (h) :
+    (a.insertIdx i x h).toList = a.toList.insertIdx i x := by simp
+
+theorem toList_insertIdx! (a : Vector α n) (i x) (hi : i ≤ n) :
+    (a.insertIdx! i x).toList = a.toList.insertIdx i x := by
+  cases a; simp_all [Array.insertIdx!]
+
 theorem toList_cast (a : Vector α n) (h : n = m) :
     (a.cast h).toList = a.toList := rfl