-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem getElem_insertIdx_of_lt {l : List α} {x : α} {n k : Nat} (hn : k < n)
    (hk : k < (insertIdx n x l).length) :
    (insertIdx n x l)[k] = l[k]'(by simp [length_insertIdx] at hk; split at hk <;> omega)

Proof state:
case succ.cons.succ
α : Type u
x : α
n : Nat
ih : ∀ {l : List α} {k : Nat} (hn : k < n) (hk : k < (insertIdx n x l).length), (insertIdx n x l)[k] = l[k]
head✝ : α
tail✝ : List α
n✝ : Nat
hn : n✝ + 1 < n + 1
hk : n✝ + 1 < (insertIdx (n + 1) x (head✝ :: tail✝)).length
⊢ (insertIdx (n + 1) x (head✝ :: tail✝))[n✝ + 1] = (head✝ :: tail✝)[n✝ + 1]

Tactic:
rw [Nat.succ_lt_succ_iff] at hn

Result:
case succ.cons.succ
α : Type u
x : α
n : Nat
ih : ∀ {l : List α} {k : Nat} (hn : k < n) (hk : k < (insertIdx n x l).length), (insertIdx n x l)[k] = l[k]
head✝ : α
tail✝ : List α
n✝ : Nat
hn✝ : n✝ + 1 < n + 1
hn : n✝ < n
hk : n✝ + 1 < (insertIdx (n + 1) x (head✝ :: tail✝)).length
⊢ (insertIdx (n + 1) x (head✝ :: tail✝))[n✝ + 1] = (head✝ :: tail✝)[n✝ + 1]

Proof state:
case succ.nil
α : Type u
x : α
n : Nat
ih : ∀ {l : List α} {k : Nat} (hn : k < n) (hk : k < (insertIdx n x l).length), (insertIdx n x l)[k] = l[k]
k : Nat
hn : k < n + 1
hk : k < (insertIdx (n + 1) x []).length
⊢ (insertIdx (n + 1) x [])[k] = [][k]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
x : α
n k : Nat
hn : k < n
hk : k < (insertIdx n x l).length
⊢ k < l.length

Tactic:
simp [length_insertIdx] at hk

Result:
α : Type u
a : α
l : List α
x : α
n k : Nat
hn : k < n
hk : k < if n ≤ l.length then l.length + 1 else l.length
⊢ k < l.length

Proof state:
case zero
α : Type u
x : α
l : List α
k : Nat
hn : k < 0
hk : k < (insertIdx 0 x l).length
⊢ (insertIdx 0 x l)[k] = l[k]

Tactic:
simp at hn

Result:
no goals

Proof state:
case succ.cons.zero
α : Type u
x : α
n : Nat
ih : ∀ {l : List α} {k : Nat} (hn : k < n) (hk : k < (insertIdx n x l).length), (insertIdx n x l)[k] = l[k]
head✝ : α
tail✝ : List α
hn : 0 < n + 1
hk : 0 < (insertIdx (n + 1) x (head✝ :: tail✝)).length
⊢ (insertIdx (n + 1) x (head✝ :: tail✝))[0] = (head✝ :: tail✝)[0]

Tactic:
simp [get]

Result:
no goals

Proof state:
case succ.cons.succ
α : Type u
x : α
n : Nat
ih : ∀ {l : List α} {k : Nat} (hn : k < n) (hk : k < (insertIdx n x l).length), (insertIdx n x l)[k] = l[k]
head✝ : α
tail✝ : List α
n✝ : Nat
hn✝ : n✝ + 1 < n + 1
hn : n✝ < n
hk : n✝ + 1 < (insertIdx (n + 1) x (head✝ :: tail✝)).length
⊢ (insertIdx (n + 1) x (head✝ :: tail✝))[n✝ + 1] = (head✝ :: tail✝)[n✝ + 1]

Tactic:
simpa using ih hn _

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
x : α
n k : Nat
hn : k < n
hk : k < if n ≤ l.length then l.length + 1 else l.length
⊢ k < l.length

Tactic:
split at hk <;> omega

Result:
no goals

Proof state:
case succ.cons
α : Type u
x : α
n : Nat
ih : ∀ {l : List α} {k : Nat} (hn : k < n) (hk : k < (insertIdx n x l).length), (insertIdx n x l)[k] = l[k]
k : Nat
hn : k < n + 1
head✝ : α
tail✝ : List α
hk : k < (insertIdx (n + 1) x (head✝ :: tail✝)).length
⊢ (insertIdx (n + 1) x (head✝ :: tail✝))[k] = (head✝ :: tail✝)[k]

Tactic:
cases k

Result:
case succ.cons.zero
α : Type u
x : α
n : Nat
ih : ∀ {l : List α} {k : Nat} (hn : k < n) (hk : k < (insertIdx n x l).length), (insertIdx n x l)[k] = l[k]
head✝ : α
tail✝ : List α
hn : 0 < n + 1
hk : 0 < (insertIdx (n + 1) x (head✝ :: tail✝)).length
⊢ (insertIdx (n + 1) x (head✝ :: tail✝))[0] = (head✝ :: tail✝)[0]

case succ.cons.succ
α : Type u
x : α
n : Nat
ih : ∀ {l : List α} {k : Nat} (hn : k < n) (hk : k < (insertIdx n x l).length), (insertIdx n x l)[k] = l[k]
head✝ : α
tail✝ : List α
n✝ : Nat
hn : n✝ + 1 < n + 1
hk : n✝ + 1 < (insertIdx (n + 1) x (head✝ :: tail✝)).length
⊢ (insertIdx (n + 1) x (head✝ :: tail✝))[n✝ + 1] = (head✝ :: tail✝)[n✝ + 1]