-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
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
        l[k]'(by simp [length_insertIdx] at h; split at h <;> omega)
      else
        if h₂ : k = n then
          x
        else
          l[k-1]'(by simp [length_insertIdx] at h; split at h <;> omega)

Proof state:
case isFalse.isTrue
α : Type u
l : List α
x : α
k : Nat
h : k < (insertIdx k x l).length
h₁ : ¬k < k
⊢ (insertIdx k x l)[k] = x

Tactic:
rw [getElem_insertIdx_self h]

Result:
no goals

Proof state:
case isFalse
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
h₁ : ¬k < n
⊢ (insertIdx n x l)[k] = if h₂ : k = n then x else l[k - 1]

Tactic:
split <;> rename_i h₂

Result:
case isFalse.isTrue
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
h₁ : ¬k < n
h₂ : k = n
⊢ (insertIdx n x l)[k] = x

case isFalse.isFalse
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
h₁ : ¬k < n
h₂ : ¬k = n
⊢ (insertIdx n x l)[k] = l[k - 1]

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

Tactic:
simp [length_insertIdx] at h

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

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

Tactic:
split at h <;> omega

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
x : α
n k : Nat
h₁ : ¬k < n
h₂ : ¬k = n
h : k < if n ≤ l.length then l.length + 1 else l.length
⊢ k - 1 < l.length

Tactic:
split at h <;> omega

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
h₁ : ¬k < n
h₂ : ¬k = n
⊢ n + 1 ≤ k

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
⊢ (insertIdx n x l)[k] = if h₁ : k < n then l[k] else if h₂ : k = n then x else l[k - 1]

Tactic:
split <;> rename_i h₁

Result:
case isTrue
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
h₁ : k < n
⊢ (insertIdx n x l)[k] = l[k]

case isFalse
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
h₁ : ¬k < n
⊢ (insertIdx n x l)[k] = if h₂ : k = n then x else l[k - 1]

Proof state:
case isTrue
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
h₁ : k < n
⊢ (insertIdx n x l)[k] = l[k]

Tactic:
rw [getElem_insertIdx_of_lt h₁]

Result:
no goals

Proof state:
case isFalse.isTrue
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
h₁ : ¬k < n
h₂ : k = n
⊢ (insertIdx n x l)[k] = x

Tactic:
subst h₂

Result:
case isFalse.isTrue
α : Type u
l : List α
x : α
k : Nat
h : k < (insertIdx k x l).length
h₁ : ¬k < k
⊢ (insertIdx k x l)[k] = x

Proof state:
α : Type u
a : α
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
h₁ : ¬k < n
h₂ : ¬k = n
⊢ k - 1 < l.length

Tactic:
simp [length_insertIdx] at h

Result:
α : Type u
a : α
l : List α
x : α
n k : Nat
h₁ : ¬k < n
h₂ : ¬k = n
h : k < if n ≤ l.length then l.length + 1 else l.length
⊢ k - 1 < l.length

Proof state:
case isFalse.isFalse
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
h₁ : ¬k < n
h₂ : ¬k = n
⊢ (insertIdx n x l)[k] = l[k - 1]

Tactic:
rw [getElem_insertIdx_of_ge (by omega)]

Result:
no goals