-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem getElem_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (hn : n + 1 ≤ 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)

Proof state:
case nil.zero
α : Type u
x : α
k : Nat
hn : 0 + 1 ≤ k
hk✝ : k < (insertIdx 0 x []).length
hk : k = 0
⊢ (insertIdx 0 x [])[k] = [][k - 1]

Tactic:
omega

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
cases n with
| zero =>
  simp only [insertIdx_zero] at hk
  cases k with
  | zero => omega
  | succ k => simp
| succ n =>
  cases k with
  | zero => simp
  | succ k =>
    simp only [insertIdx_succ_cons, getElem_cons_succ]
    rw [ih (by omega)]
    cases k with
    | zero => omega
    | succ k => simp

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
cases k with
| zero => simp
| succ k =>
  simp only [insertIdx_succ_cons, getElem_cons_succ]
  rw [ih (by omega)]
  cases k with
  | zero => omega
  | succ k => simp

Result:
no goals

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

Tactic:
simp only [insertIdx_zero] at hk

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

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

Tactic:
simp only [insertIdx_succ_cons, getElem_cons_succ]

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

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

Tactic:
simp [length_insertIdx] at hk

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

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

Tactic:
simp

Result:
no goals

Proof state:
case nil.succ
α : Type u
x : α
k n : Nat
hn : n + 1 + 1 ≤ k
hk : k < (insertIdx (n + 1) x []).length
⊢ (insertIdx (n + 1) x [])[k] = [][k - 1]

Tactic:
simp at hk

Result:
no goals

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

Tactic:
omega

Result:
no goals

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

Tactic:
cases k with
| zero => omega
| succ k => simp

Result:
no goals

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

Tactic:
rw [ih (by omega)]

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

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

Tactic:
omega

Result:
no goals

Proof state:
case nil
α : Type u
x : α
n k : Nat
hn : n + 1 ≤ k
hk : k < (insertIdx n x []).length
⊢ (insertIdx n x [])[k] = [][k - 1]

Tactic:
cases n with
| zero =>
  simp only [insertIdx_zero, length_singleton, lt_one_iff] at hk
  omega
| succ n => simp at hk

Result:
no goals

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

Tactic:
omega

Result:
no goals

Proof state:
case nil.zero
α : Type u
x : α
k : Nat
hn : 0 + 1 ≤ k
hk : k < (insertIdx 0 x []).length
⊢ (insertIdx 0 x [])[k] = [][k - 1]

Tactic:
simp only [insertIdx_zero, length_singleton, lt_one_iff] at hk

Result:
case nil.zero
α : Type u
x : α
k : Nat
hn : 0 + 1 ≤ k
hk✝ : k < (insertIdx 0 x []).length
hk : k = 0
⊢ (insertIdx 0 x [])[k] = [][k - 1]