-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem getElem_insertIdx_self {l : List α} {x : α} {n : Nat} (hn : n < (insertIdx n x l).length) :
    (insertIdx n x l)[n] = x

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

Tactic:
simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_lt_add_iff_right] at hn ih

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

Proof state:
case nil.isTrue
α : Type u
x : α
n : Nat
hn✝ : n < (insertIdx n x []).length
h✝ : n = 0
hn : n < 1
⊢ (insertIdx n x [])[n] = x

Tactic:
simp_all

Result:
no goals

Proof state:
case nil
α : Type u
x : α
n : Nat
hn✝ : n < (insertIdx n x []).length
hn : n < if n = 0 then 1 else 0
⊢ (insertIdx n x [])[n] = x

Tactic:
split at hn

Result:
case nil.isTrue
α : Type u
x : α
n : Nat
hn✝ : n < (insertIdx n x []).length
h✝ : n = 0
hn : n < 1
⊢ (insertIdx n x [])[n] = x

case nil.isFalse
α : Type u
x : α
n : Nat
hn✝ : n < (insertIdx n x []).length
h✝ : ¬n = 0
hn : n < 0
⊢ (insertIdx n x [])[n] = x

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

Tactic:
simp

Result:
no goals

Proof state:
case nil.isFalse
α : Type u
x : α
n : Nat
hn✝ : n < (insertIdx n x []).length
h✝ : ¬n = 0
hn : n < 0
⊢ (insertIdx n x [])[n] = x

Tactic:
omega

Result:
no goals

Proof state:
case nil
α : Type u
x : α
n : Nat
hn : n < (insertIdx n x []).length
⊢ (insertIdx n x [])[n] = x

Tactic:
simp [length_insertIdx] at hn

Result:
case nil
α : Type u
x : α
n : Nat
hn✝ : n < (insertIdx n x []).length
hn : n < if n = 0 then 1 else 0
⊢ (insertIdx n x [])[n] = x

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

Tactic:
cases n

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

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

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

Tactic:
simpa using ih hn

Result:
no goals