-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem getElem?_insertIdx {l : List α} {x : α} {n k : Nat} :
    (insertIdx n x l)[k]? =
      if k < n then
        l[k]?
      else
        if k = n then
          if k ≤ l.length then some x else none
        else
          l[k-1]?

Proof state:
case isTrue.isFalse.isTrue
α : Type u
l : List α
x : α
n k : Nat
h✝ : k < (insertIdx n x l).length
h : k < if n ≤ l.length then l.length + 1 else l.length
h₁ : ¬k < n
h₂ : k = n
⊢ some x = if k ≤ l.length then some x else none

Tactic:
rw [if_pos]

Result:
case isTrue.isFalse.isTrue.hc
α : Type u
l : List α
x : α
n k : Nat
h✝ : k < (insertIdx n x l).length
h : k < if n ≤ l.length then l.length + 1 else l.length
h₁ : ¬k < n
h₂ : k = n
⊢ k ≤ l.length

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

Tactic:
split at h <;> omega

Result:
no goals

Proof state:
case isTrue.isFalse.isTrue.hc
α : Type u
l : List α
x : α
n k : Nat
h✝ : k < (insertIdx n x l).length
h : k < if n ≤ l.length then l.length + 1 else l.length
h₁ : ¬k < n
h₂ : k = n
⊢ k ≤ l.length

Tactic:
split at h <;> omega

Result:
no goals

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

Tactic:
simp only [length_insertIdx] at h

Result:
case isFalse
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < if n ≤ l.length then l.length + 1 else l.length
⊢ none = if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

Proof state:
case isFalse.isFalse.isTrue
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < if n ≤ l.length then l.length + 1 else l.length
h₁ : ¬k < n
h₂ : k = n
⊢ none = if k ≤ l.length then some x else none

Tactic:
rw [if_neg]

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

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

Tactic:
split <;> rename_i h₂

Result:
case isTrue.isFalse.isTrue
α : Type u
l : List α
x : α
n k : Nat
h✝ : k < (insertIdx n x l).length
h : k < if n ≤ l.length then l.length + 1 else l.length
h₁ : ¬k < n
h₂ : k = n
⊢ some x = if k ≤ l.length then some x else none

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

Proof state:
case isFalse
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < if n ≤ l.length then l.length + 1 else l.length
⊢ none = if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

Tactic:
split <;> rename_i h₁

Result:
case isFalse.isTrue
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < if n ≤ l.length then l.length + 1 else l.length
h₁ : k < n
⊢ none = l[k]?

case isFalse.isFalse
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < if n ≤ l.length then l.length + 1 else l.length
h₁ : ¬k < n
⊢ none = if k = n then if k ≤ l.length then some x else none else l[k - 1]?

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

Tactic:
split at h <;> omega

Result:
no goals

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

Tactic:
rw [getElem?_def]

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

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

Tactic:
split at h <;> omega

Result:
no goals

Proof state:
case isTrue
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
⊢ some (insertIdx n x l)[k] =
    if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

Tactic:
rw [getElem_insertIdx h]

Result:
case isTrue
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
⊢ some (if h₁ : k < n then l[k] else if h₂ : k = n then x else l[k - 1]) =
    if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

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

Tactic:
simp only [Option.some_eq_dite_none_right, exists_prop, and_true]

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

Proof state:
case isTrue.isTrue
α : Type u
l : List α
x : α
n k : Nat
h✝ : k < (insertIdx n x l).length
h : k < if n ≤ l.length then l.length + 1 else l.length
h₁ : k < n
⊢ some l[k] = l[k]?

Tactic:
rw [getElem?_def, dif_pos]

Result:
no goals

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

Tactic:
simp only [length_insertIdx] at h

Result:
case isTrue
α : Type u
l : List α
x : α
n k : Nat
h✝ : k < (insertIdx n x l).length
h : k < if n ≤ l.length then l.length + 1 else l.length
⊢ some (if h₁ : k < n then l[k] else if h₂ : k = n then x else l[k - 1]) =
    if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

Proof state:
α : Type u
l : List α
x : α
n k : Nat
⊢ (insertIdx n x l)[k]? = if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

Tactic:
rw [getElem?_def]

Result:
α : Type u
l : List α
x : α
n k : Nat
⊢ (if h : k < (insertIdx n x l).length then some (insertIdx n x l)[k] else none) =
    if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

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

Tactic:
rw [getElem?_eq_none]

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

Proof state:
case isFalse.isTrue
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < if n ≤ l.length then l.length + 1 else l.length
h₁ : k < n
⊢ none = l[k]?

Tactic:
rw [getElem?_eq_none]

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