Init.Data.List.Nat.InsertIdx

List.insertIdx_zero theorem

{xs : List α} {x : α} : xs.insertIdx 0 x = x :: xs

Full source

@[simp]
theorem insertIdx_zero {xs : List α} {x : α} : xs.insertIdx 0 x = x :: xs :=
  rfl

Insertion at index zero prepends the element

Informal description

For any list $L$ of elements of type $\alpha$ and any element $x \in \alpha$, inserting $x$ at index $0$ in $L$ results in the list $x :: L$.

List.insertIdx_succ_nil theorem

{n : Nat} {a : α} : ([] : List α).insertIdx (n + 1) a = []

Full source

@[simp]
theorem insertIdx_succ_nil {n : Nat} {a : α} : ([] : List α).insertIdx (n + 1) a = [] :=
  rfl

Insertion at index $n+1$ in empty list is empty

Informal description

For any natural number $n$ and any element $a$ of type $\alpha$, inserting $a$ at index $n+1$ into the empty list results in the empty list, i.e., $\text{insertIdx}\ [\,]\ (n+1)\ a = [\,]$.

List.insertIdx_succ_cons theorem

{xs : List α} {hd x : α} {i : Nat} : (hd :: xs).insertIdx (i + 1) x = hd :: xs.insertIdx i x

Full source

@[simp]
theorem insertIdx_succ_cons {xs : List α} {hd x : α} {i : Nat} :
    (hd :: xs).insertIdx (i + 1) x = hd :: xs.insertIdx i x :=
  rfl

Recursive Insertion at Successor Index in List

Informal description

For any list $L = \text{hd} :: \text{xs}$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural number index $i$, inserting $x$ into $L$ at position $i + 1$ is equivalent to prepending $\text{hd}$ to the result of inserting $x$ into $\text{xs}$ at position $i$. More formally: \[ \text{insertIdx } (\text{hd} :: \text{xs}) \, (i + 1) \, x = \text{hd} :: (\text{insertIdx } \text{xs} \, i \, x). \]

List.length_insertIdx theorem

: ∀ {i} {as : List α}, (as.insertIdx i a).length = if i ≤ as.length then as.length + 1 else as.length

Full source

theorem length_insertIdx : ∀ {i} {as : List α}, (as.insertIdx i a).length = if i ≤ as.length then as.length + 1 else as.length
  | 0, _ => by simp
  | n + 1, [] => by simp
  | n + 1, a :: as => by
    simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_le_add_iff_right]
    split <;> rfl

Length of List After Insertion: $\text{length}(\text{insertIdx } L \, i \, a) = \text{length}(L) + 1$ if $i \leq \text{length}(L)$

Informal description

For any list $L$ of elements of type $\alpha$, any natural number index $i$, and any element $a \in \alpha$, the length of the list obtained by inserting $a$ into $L$ at position $i$ is equal to $\text{length}(L) + 1$ if $i \leq \text{length}(L)$, and remains $\text{length}(L)$ otherwise. More formally: \[ \text{length}(\text{insertIdx } L \, i \, a) = \begin{cases} \text{length}(L) + 1 & \text{if } i \leq \text{length}(L) \\ \text{length}(L) & \text{otherwise.} \end{cases} \]

List.length_insertIdx_of_le_length theorem

(h : i ≤ length as) (a : α) : (as.insertIdx i a).length = as.length + 1

Full source

theorem length_insertIdx_of_le_length (h : i ≤ length as) (a : α) : (as.insertIdx i a).length = as.length + 1 := by
  simp [length_insertIdx, h]

Length Increase After Insertion: $\text{length}(L[i \mapsto a]) = \text{length}(L) + 1$ when $i \leq \text{length}(L)$

Informal description

For any list $L$ of elements of type $\alpha$, any natural number index $i$, and any element $a \in \alpha$, if $i \leq \text{length}(L)$, then the length of the list obtained by inserting $a$ into $L$ at position $i$ is equal to $\text{length}(L) + 1$.

List.length_insertIdx_of_length_lt theorem

(h : length as < i) (a : α) : (as.insertIdx i a).length = as.length

Full source

theorem length_insertIdx_of_length_lt (h : length as < i) (a : α) : (as.insertIdx i a).length = as.length := by
  simp [length_insertIdx, h]

Length Preservation in List Insertion Beyond Length: $\text{length}(\text{insertIdx } L \, i \, a) = \text{length}(L)$ when $i > \text{length}(L)$

Informal description

For any list $L$ of elements of type $\alpha$, any natural number index $i$, and any element $a \in \alpha$, if the length of $L$ is strictly less than $i$, then the length of the list obtained by inserting $a$ into $L$ at position $i$ remains equal to the length of $L$. More formally: \[ \text{If } \text{length}(L) < i, \text{ then } \text{length}(\text{insertIdx } L \, i \, a) = \text{length}(L). \]

List.eraseIdx_insertIdx theorem

{i : Nat} {l : List α} (a : α) : (l.insertIdx i a).eraseIdx i = l

Full source

@[simp]
theorem eraseIdx_insertIdx {i : Nat} {l : List α} (a : α) : (l.insertIdx i a).eraseIdx i = l := by
  rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]
  exact modifyTailIdx_id _ _

Insertion and Deletion Cancel: $\text{eraseIdx}(\text{insertIdx } L \, i \, a, i) = L$

Informal description

For any natural number index $i$, any list $L$ of elements of type $\alpha$, and any element $a \in \alpha$, removing the element at position $i$ from the list obtained by inserting $a$ into $L$ at position $i$ yields the original list $L$. More formally: \[ \text{eraseIdx}(\text{insertIdx } L \, i \, a, i) = L. \]

List.insertIdx_eraseIdx_of_ge theorem

: ∀ {i m as}, i < length as → i ≤ m → (as.eraseIdx i).insertIdx m a = (as.insertIdx (m + 1) a).eraseIdx i

Full source

theorem insertIdx_eraseIdx_of_ge :
    ∀ {i m as},
      i < length as → i ≤ m → (as.eraseIdx i).insertIdx m a = (as.insertIdx (m + 1) a).eraseIdx i
  | 0, 0, [], has, _ => (Nat.lt_irrefl _ has).elim
  | 0, 0, _ :: as, _, _ => by simp [eraseIdx, insertIdx]
  | 0, _ + 1, _ :: _, _, _ => rfl
  | n + 1, m + 1, a :: as, has, hmn =>
    congrArg (cons a) <|
      insertIdx_eraseIdx_of_ge (Nat.lt_of_succ_lt_succ has) (Nat.le_of_succ_le_succ hmn)

Insertion and Deletion Commute for Indices with $m \geq i$ in Lists

Informal description

For any list $L$ of elements of type $\alpha$, any index $i$ such that $i < \text{length}(L)$, any element $a \in \alpha$, and any index $m \geq i$, the following equality holds: \[ (L.\text{eraseIdx}(i)).\text{insertIdx}(m, a) = (L.\text{insertIdx}(m + 1, a)).\text{eraseIdx}(i). \] Here, $\text{eraseIdx}(k)$ removes the element at position $k$ in $L$, and $\text{insertIdx}(k, x)$ inserts element $x$ at position $k$ in $L$.

List.insertIdx_eraseIdx_of_le theorem

: ∀ {i j as}, i < length as → j ≤ i → (as.eraseIdx i).insertIdx j a = (as.insertIdx j a).eraseIdx (i + 1)

Full source

theorem insertIdx_eraseIdx_of_le :
    ∀ {i j as},
      i < length as → j ≤ i → (as.eraseIdx i).insertIdx j a = (as.insertIdx j a).eraseIdx (i + 1)
  | _, 0, _ :: _, _, _ => rfl
  | _ + 1, _ + 1, a :: _, has, hmn =>
    congrArg (cons a) <|
      insertIdx_eraseIdx_of_le (Nat.lt_of_succ_lt_succ has) (Nat.le_of_succ_le_succ hmn)

Insertion and Deletion Commute for Ordered Indices in Lists

Informal description

For any list $L$ of elements of type $\alpha$, any index $i$ such that $i < \text{length}(L)$, any element $a \in \alpha$, and any index $j \leq i$, the following equality holds: \[ (L.\text{eraseIdx}(i)).\text{insertIdx}(j, a) = (L.\text{insertIdx}(j, a)).\text{eraseIdx}(i + 1). \] Here, $\text{eraseIdx}(k)$ removes the element at position $k$ in $L$, and $\text{insertIdx}(k, x)$ inserts element $x$ at position $k$ in $L$.

List.insertIdx_comm theorem

 (a b : α) :
  ∀ {i j : Nat} {l : List α} (_ : i ≤ j) (_ : j ≤ length l),
    (l.insertIdx i a).insertIdx (j + 1) b = (l.insertIdx j b).insertIdx i a

Full source

theorem insertIdx_comm (a b : α) :
    ∀ {i j : Nat} {l : List α} (_ : i ≤ j) (_ : j ≤ length l),
      (l.insertIdx i a).insertIdx (j + 1) b = (l.insertIdx j b).insertIdx i a
  | 0, j, l => by simp [insertIdx]
  | _ + 1, 0, _ => fun h => (Nat.not_lt_zero _ h).elim
  | i + 1, j + 1, [] => by simp
  | i + 1, j + 1, c :: l => fun h₀ h₁ => by
    simp only [insertIdx_succ_cons, cons.injEq, true_and]
    exact insertIdx_comm a b (Nat.le_of_succ_le_succ h₀) (Nat.le_of_succ_le_succ h₁)

Commutativity of List Insertions at Ordered Indices

Informal description

For any list $L$ of elements of type $\alpha$, any two elements $a, b \in \alpha$, and any indices $i, j \in \mathbb{N}$ such that $i \leq j \leq \text{length}(L)$, the following equality holds: \[ (L.\text{insertIdx}(i, a)).\text{insertIdx}(j + 1, b) = (L.\text{insertIdx}(j, b)).\text{insertIdx}(i, a). \] Here, $\text{insertIdx}(k, x)$ denotes the operation of inserting element $x$ at position $k$ in the list $L$.

List.mem_insertIdx theorem

{a b : α} : ∀ {i : Nat} {l : List α} (_ : i ≤ l.length), a ∈ l.insertIdx i b ↔ a = b ∨ a ∈ l

Full source

theorem mem_insertIdx {a b : α} :
    ∀ {i : Nat} {l : List α} (_ : i ≤ l.length), a ∈ l.insertIdx i ba ∈ l.insertIdx i b ↔ a = b ∨ a ∈ l
  | 0, as, _ => by simp
  | _ + 1, [], h => (Nat.not_succ_le_zero _ h).elim
  | n + 1, a' :: as, h => by
    rw [List.insertIdx_succ_cons, mem_cons, mem_insertIdx (Nat.le_of_succ_le_succ h),
      ← or_assoc, @or_comm (a = a'), or_assoc, mem_cons]

Membership in List After Insertion: $a \in \text{insertIdx}(l, i, b) \leftrightarrow a = b \lor a \in l$

Informal description

For any elements $a$ and $b$ of type $\alpha$, any natural number index $i$, and any list $l$ of elements of type $\alpha$ such that $i \leq \text{length}(l)$, the element $a$ is in the list obtained by inserting $b$ at position $i$ in $l$ if and only if either $a$ equals $b$ or $a$ is in $l$. In symbols: \[ a \in \text{insertIdx}(l, i, b) \leftrightarrow (a = b \lor a \in l). \]

List.insertIdx_of_length_lt theorem

{l : List α} {x : α} {i : Nat} (h : l.length < i) : l.insertIdx i x = l

Full source

theorem insertIdx_of_length_lt {l : List α} {x : α} {i : Nat} (h : l.length < i) :
    l.insertIdx i x = l := by
  induction l generalizing i with
  | nil =>
    cases i
    · simp at h
    · simp
  | cons x l ih =>
    cases i
    · simp at h
    · simp only [Nat.succ_lt_succ_iff, length] at h
      simpa using ih h

Insertion at Index Beyond Length Preserves List

Informal description

For any list $L$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural number index $i$, if the length of $L$ is strictly less than $i$, then inserting $x$ into $L$ at position $i$ leaves $L$ unchanged, i.e., $\text{insertIdx}(L, i, x) = L$.

List.insertIdx_length_self theorem

{l : List α} {x : α} : l.insertIdx l.length x = l ++ [x]

Full source

@[simp]
theorem insertIdx_length_self {l : List α} {x : α} : l.insertIdx l.length x = l ++ [x] := by
  induction l with
  | nil => simp
  | cons x l ih => simpa using ih

Insertion at List Length Equals Append

Informal description

For any list $l$ of elements of type $\alpha$ and any element $x$ of type $\alpha$, inserting $x$ at the index equal to the length of $l$ results in the concatenation of $l$ with the singleton list $[x]$, i.e., \[ \text{insertIdx } l \, (\text{length } l) \, x = l \mathbin{+\!\!+} [x]. \]

List.length_le_length_insertIdx theorem

{l : List α} {x : α} {i : Nat} : l.length ≤ (l.insertIdx i x).length

Full source

theorem length_le_length_insertIdx {l : List α} {x : α} {i : Nat} :
    l.length ≤ (l.insertIdx i x).length := by
  simp only [length_insertIdx]
  split <;> simp

Monotonicity of List Length Under Insertion: $\text{length}(L) \leq \text{length}(\text{insertIdx } L \, i \, x)$

Informal description

For any list $L$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural number index $i$, the length of $L$ is less than or equal to the length of the list obtained by inserting $x$ into $L$ at position $i$. In other words, $\text{length}(L) \leq \text{length}(\text{insertIdx } L \, i \, x)$.

List.length_insertIdx_le_succ theorem

{l : List α} {x : α} {i : Nat} : (l.insertIdx i x).length ≤ l.length + 1

Full source

theorem length_insertIdx_le_succ {l : List α} {x : α} {i : Nat} :
    (l.insertIdx i x).length ≤ l.length + 1 := by
  simp only [length_insertIdx]
  split <;> simp

Upper Bound on List Length After Insertion: $\text{length}(\text{insertIdx } L \, i \, x) \leq \text{length}(L) + 1$

Informal description

For any list $L$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural number index $i$, the length of the list obtained by inserting $x$ into $L$ at position $i$ is at most the length of $L$ plus one. More formally: \[ \text{length}(\text{insertIdx } L \, i \, x) \leq \text{length}(L) + 1. \]

List.getElem_insertIdx_of_lt theorem

 {l : List α} {x : α} {i j : Nat} (hn : j < i) (hk : j < (l.insertIdx i x).length) :
  (l.insertIdx i x)[j] = l[j]'(by simp [length_insertIdx] at hk; split at hk <;> omega)

Full source

theorem getElem_insertIdx_of_lt {l : List α} {x : α} {i j : Nat} (hn : j < i)
    (hk : j < (l.insertIdx i x).length) :
    (l.insertIdx i x)[j] = l[j]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
  induction i generalizing j l with
  | zero => simp at hn
  | succ n ih =>
    cases l with
    | nil => simp
    | cons _ _=>
      cases j
      · simp
      · rw [Nat.succ_lt_succ_iff] at hn
        simpa using ih hn _

Element Preservation in List Insertion for Indices Less Than Insertion Point: $(\text{insertIdx } L \, i \, x)[j] = L[j]$ when $j < i$

Informal description

For any list $L$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural number indices $i$ and $j$ such that $j < i$ and $j$ is a valid index in the list obtained by inserting $x$ into $L$ at position $i$, the element at position $j$ in the modified list equals the element at position $j$ in the original list. More formally: If $j < i$ and $j < \text{length}(\text{insertIdx } L \, i \, x)$, then $(\text{insertIdx } L \, i \, x)[j] = L[j]$.

List.getElem_insertIdx_self theorem

{l : List α} {x : α} {i : Nat} (hi : i < (l.insertIdx i x).length) : (l.insertIdx i x)[i] = x

Full source

@[simp]
theorem getElem_insertIdx_self {l : List α} {x : α} {i : Nat} (hi : i < (l.insertIdx i x).length) :
    (l.insertIdx i x)[i] = x := by
  induction l generalizing i with
  | nil =>
    simp [length_insertIdx] at hi
    split at hi
    · simp_all
    · omega
  | cons _ _ ih =>
    cases i
    · simp
    · simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_lt_add_iff_right] at hi ih
      simpa using ih hi

Element at Insertion Index Equals Inserted Value: $(\text{insertIdx } L \, i \, x)[i] = x$ when $i$ is valid

Informal description

For any list $L$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural number index $i$ such that $i$ is a valid index in the list obtained by inserting $x$ into $L$ at position $i$, the element at position $i$ in the resulting list is equal to $x$. More formally: If $i < \text{length}(\text{insertIdx } L \, i \, x)$, then $(\text{insertIdx } L \, i \, x)[i] = x$.

List.getElem_insertIdx_of_gt theorem

 {l : List α} {x : α} {i j : Nat} (hn : i < j) (hk : j < (l.insertIdx i x).length) :
  (l.insertIdx i x)[j] = l[j - 1]'(by simp [length_insertIdx] at hk; split at hk <;> omega)

Full source

theorem getElem_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (hn : i < j)
    (hk : j < (l.insertIdx i x).length) :
    (l.insertIdx i x)[j] = l[j - 1]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
  induction l generalizing i j with
  | nil =>
    cases i with
    | zero =>
      simp only [insertIdx_zero, length_singleton, lt_one_iff] at hk
      omega
    | succ n => simp at hk
  | cons _ _ ih =>
    cases i with
    | zero =>
      simp only [insertIdx_zero] at hk
      cases j with
      | zero => omega
      | succ j => simp
    | succ n =>
      cases j with
      | zero => simp
      | succ j =>
        simp only [insertIdx_succ_cons, getElem_cons_succ]
        rw [ih (by omega)]
        cases j with
        | zero => omega
        | succ j => simp

Element Access After Insertion at Greater Index: $(\text{insertIdx } l \, i \, x)[j] = l[j-1]$ when $i < j$

Informal description

For any list $l$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural numbers $i$ and $j$ such that $i < j$ and $j$ is a valid index in the list obtained by inserting $x$ into $l$ at position $i$, the element at position $j$ in the modified list is equal to the element at position $j-1$ in the original list $l$. More formally, if $i < j$ and $j < \text{length}(\text{insertIdx } l \, i \, x)$, then: \[ (\text{insertIdx } l \, i \, x)[j] = l[j-1] \]

List.getElem_insertIdx_of_ge abbrev

Full source

@[deprecated getElem_insertIdx_of_gt (since := "2025-02-04")]
abbrev getElem_insertIdx_of_ge := @getElem_insertIdx_of_gt

Element Access After Insertion at Greater or Equal Index: $(\text{insertIdx } l \, i \, x)[j] = l[j-1]$ when $j \geq i$

Informal description

For any list $l$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural numbers $i$ and $j$ such that $j \geq i$ and $j$ is a valid index in the list obtained by inserting $x$ into $l$ at position $i$, the element at position $j$ in the modified list is equal to the element at position $j-1$ in the original list $l$. More formally, if $j \geq i$ and $j < \text{length}(\text{insertIdx } l \, i \, x)$, then: \[ (\text{insertIdx } l \, i \, x)[j] = l[j-1] \]

List.getElem_insertIdx theorem

 {l : List α} {x : α} {i j : Nat} (h : j < (l.insertIdx i x).length) :
  (l.insertIdx i x)[j] =
    if h₁ : j < i then l[j]'(by simp [length_insertIdx] at h; split at h <;> omega)
    else if h₂ : j = i then x else l[j - 1]'(by simp [length_insertIdx] at h; split at h <;> omega)

Full source

theorem getElem_insertIdx {l : List α} {x : α} {i j : Nat} (h : j < (l.insertIdx i x).length) :
    (l.insertIdx i x)[j] =
      if h₁ : j < i then
        l[j]'(by simp [length_insertIdx] at h; split at h <;> omega)
      else
        if h₂ : j = i then
          x
        else
          l[j-1]'(by simp [length_insertIdx] at h; split at h <;> omega) := by
  split <;> rename_i h₁
  · rw [getElem_insertIdx_of_lt h₁]
  · split <;> rename_i h₂
    · subst h₂
      rw [getElem_insertIdx_self h]
    · rw [getElem_insertIdx_of_gt (by omega)]

Element Access in List After Insertion: $(l.\text{insertIdx}\ i\ x)[j]$ under Different Index Conditions

Informal description

For any list $l$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural numbers $i$ and $j$ such that $j$ is a valid index in the list obtained by inserting $x$ into $l$ at position $i$, the element at position $j$ in the modified list is given by: \[ (l.\text{insertIdx}\ i\ x)[j] = \begin{cases} l[j] & \text{if } j < i, \\ x & \text{if } j = i, \\ l[j-1] & \text{otherwise.} \end{cases} \]

List.getElem?_insertIdx theorem

 {l : List α} {x : α} {i j : Nat} :
  (l.insertIdx i x)[j]? = if j < i then l[j]? else if j = i then if j ≤ l.length then some x else none else l[j - 1]?

Full source

theorem getElem?_insertIdx {l : List α} {x : α} {i j : Nat} :
    (l.insertIdx i x)[j]? =
      if j < i then
        l[j]?
      else
        if j = i then
          if j ≤ l.length then some x else none
        else
          l[j-1]? := by
  rw [getElem?_def]
  split <;> rename_i h
  · rw [getElem_insertIdx h]
    simp only [length_insertIdx] at h
    split <;> rename_i h₁
    · rw [getElem?_def, dif_pos]
    · split <;> rename_i h₂
      · rw [if_pos]
        split at h <;> omega
      · rw [getElem?_def]
        simp only [Option.some_eq_dite_none_right, exists_prop, and_true]
        split at h <;> omega
  · simp only [length_insertIdx] at h
    split <;> rename_i h₁
    · rw [getElem?_eq_none]
      split at h <;> omega
    · split <;> rename_i h₂
      · rw [if_neg]
        split at h <;> omega
      · rw [getElem?_eq_none]
        split at h <;> omega

Optional Element Access After List Insertion: $(l.\text{insertIdx}\ i\ x)[j]?$ under Different Index Conditions

Informal description

For any list $l$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural numbers $i$ and $j$, the optional element access at index $j$ in the list obtained by inserting $x$ into $l$ at position $i$ is given by: \[ (l.\text{insertIdx}\ i\ x)[j]? = \begin{cases} l[j]? & \text{if } j < i, \\ \text{some } x & \text{if } j = i \text{ and } j \leq \text{length}(l), \\ \text{none} & \text{if } j = i \text{ and } j > \text{length}(l), \\ l[j-1]? & \text{otherwise.} \end{cases} \]

List.getElem?_insertIdx_of_lt theorem

{l : List α} {x : α} {i j : Nat} (h : j < i) : (l.insertIdx i x)[j]? = l[j]?

Full source

theorem getElem?_insertIdx_of_lt {l : List α} {x : α} {i j : Nat} (h : j < i) :
    (l.insertIdx i x)[j]? = l[j]? := by
  rw [getElem?_insertIdx, if_pos h]

Preservation of Optional Element Access Before Insertion Index: $(l.\text{insertIdx}\ i\ x)[j]? = l[j]?$ for $j < i$

Informal description

For any list $l$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural numbers $i$ and $j$ such that $j < i$, the optional element access at index $j$ in the list obtained by inserting $x$ into $l$ at position $i$ is equal to the optional element access at index $j$ in the original list $l$. That is, \[ (l.\text{insertIdx}\ i\ x)[j]? = l[j]?. \]

List.getElem?_insertIdx_self theorem

{l : List α} {x : α} {i : Nat} : (l.insertIdx i x)[i]? = if i ≤ l.length then some x else none

Full source

theorem getElem?_insertIdx_self {l : List α} {x : α} {i : Nat} :
    (l.insertIdx i x)[i]? = if i ≤ l.length then some x else none := by
  rw [getElem?_insertIdx, if_neg (by omega)]
  simp

Optional Element Access at Insertion Index: $(l.\text{insertIdx}\ i\ x)[i]?$ is $x$ if $i$ is valid, otherwise none

Informal description

For any list $l$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural number index $i$, the optional element access at index $i$ in the list obtained by inserting $x$ into $l$ at position $i$ is given by: \[ (l.\text{insertIdx}\ i\ x)[i]? = \begin{cases} \text{some } x & \text{if } i \leq \text{length}(l), \\ \text{none} & \text{otherwise.} \end{cases} \]

List.getElem?_insertIdx_of_gt theorem

{l : List α} {x : α} {i j : Nat} (h : i < j) : (l.insertIdx i x)[j]? = l[j - 1]?

Full source

theorem getElem?_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (h : i < j) :
    (l.insertIdx i x)[j]? = l[j - 1]? := by
  rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]

Optional Element Access After Insertion for Indices Greater Than Insertion Point: $(l.\text{insertIdx}\ i\ x)[j]? = l[j-1]?$ when $i < j$

Informal description

For any list $l$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural numbers $i$ and $j$ such that $i < j$, the optional element access at index $j$ in the list obtained by inserting $x$ into $l$ at position $i$ is equal to the optional element access at index $j-1$ in the original list $l$. That is, $$(l.\text{insertIdx}\ i\ x)[j]? = l[j-1]?.$$

List.getElem?_insertIdx_of_ge abbrev

Full source

@[deprecated getElem?_insertIdx_of_gt (since := "2025-02-04")]
abbrev getElem?_insertIdx_of_ge := @getElem?_insertIdx_of_gt

Optional Element Access After Insertion for Indices Less Than or Equal to Insertion Point: $(l.\text{insertIdx}\ i\ x)[j]? = l[j]?$ when $j \leq i$

Informal description

For any list $l$ of elements of type $\alpha$, any element $x \in \alpha$, and any natural numbers $i$ and $j$ such that $j \leq i$, the optional element access at index $j$ in the list obtained by inserting $x$ into $l$ at position $i$ is equal to the optional element access at index $j$ in the original list $l$. That is, $$(l.\text{insertIdx}\ i\ x)[j]? = l[j]?.$$