-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem getElem?_eraseIdx (l : List α) (i : Nat) (j : Nat) :
    (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]?

Proof state:
case isTrue.isTrue
α : Type u_1
l : List α
i j : Nat
h : j < (take i l).length
h✝ : j < i
⊢ l[j]? = l[j]?

Tactic:
rfl

Result:
no goals

Proof state:
case isFalse.isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
h' : j < i
h✝ : ¬i ≤ l.length
h : l.length ≤ j
⊢ l[i + 1 + (j - (take i l).length)]? = l[j]?

Tactic:
simp_all [getElem?_eq_none]

Result:
case isFalse.isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
h' : j < i
h✝ : l.length < i
h : l.length ≤ j
⊢ l.length ≤ i + 1 + (j - min i l.length)

Proof state:
case isFalse.isFalse.isTrue.e_a
α : Type u_1
l : List α
i j : Nat
h' : ¬j < i
h✝ : i ≤ l.length
h : i ≤ j
⊢ i + 1 + (j - min i l.length) = j + 1

Tactic:
omega

Result:
no goals

Proof state:
case isFalse.isTrue
α : Type u_1
l : List α
i j : Nat
h : ¬j < (take i l).length
h' : j < i
⊢ l[i + 1 + (j - (take i l).length)]? = l[j]?

Tactic:
simp only [length_take, Nat.min_def, Nat.not_lt] at h

Result:
case isFalse.isTrue
α : Type u_1
l : List α
i j : Nat
h' : j < i
h : (if i ≤ l.length then i else l.length) ≤ j
⊢ l[i + 1 + (j - (take i l).length)]? = l[j]?

Proof state:
case isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
h : ¬j < (take i l).length
h' : ¬j < i
⊢ l[i + 1 + (j - (take i l).length)]? = l[j + 1]?

Tactic:
simp only [length_take]

Result:
case isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
h : ¬j < (take i l).length
h' : ¬j < i
⊢ l[i + 1 + (j - min i l.length)]? = l[j + 1]?

Proof state:
case isFalse.isFalse.isTrue
α : Type u_1
l : List α
i j : Nat
h' : ¬j < i
h✝ : i ≤ l.length
h : i ≤ j
⊢ l[i + 1 + (j - min i l.length)]? = l[j + 1]?

Tactic:
congr 1

Result:
case isFalse.isFalse.isTrue.e_a
α : Type u_1
l : List α
i j : Nat
h' : ¬j < i
h✝ : i ≤ l.length
h : i ≤ j
⊢ i + 1 + (j - min i l.length) = j + 1

Proof state:
case isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
h' : ¬j < i
h : (if i ≤ l.length then i else l.length) ≤ j
⊢ l[i + 1 + (j - min i l.length)]? = l[j + 1]?

Tactic:
split at h

Result:
case isFalse.isFalse.isTrue
α : Type u_1
l : List α
i j : Nat
h' : ¬j < i
h✝ : i ≤ l.length
h : i ≤ j
⊢ l[i + 1 + (j - min i l.length)]? = l[j + 1]?

case isFalse.isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
h' : ¬j < i
h✝ : ¬i ≤ l.length
h : l.length ≤ j
⊢ l[i + 1 + (j - min i l.length)]? = l[j + 1]?

Proof state:
case isFalse
α : Type u_1
l : List α
i j : Nat
h : ¬j < (take i l).length
⊢ (drop (i + 1) l)[j - (take i l).length]? = if j < i then l[j]? else l[j + 1]?

Tactic:
rw [getElem?_drop]

Result:
case isFalse
α : Type u_1
l : List α
i j : Nat
h : ¬j < (take i l).length
⊢ l[i + 1 + (j - (take i l).length)]? = if j < i then l[j]? else l[j + 1]?

Proof state:
case isFalse.isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
h' : ¬j < i
h✝ : ¬i ≤ l.length
h : l.length ≤ j
⊢ l[i + 1 + (j - min i l.length)]? = l[j + 1]?

Tactic:
rw [getElem?_eq_none, getElem?_eq_none] <;> omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
⊢ (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]?

Tactic:
rw [eraseIdx_eq_take_drop_succ, getElem?_append]

Result:
α : Type u_1
l : List α
i j : Nat
⊢ (if j < (take i l).length then (take i l)[j]? else (drop (i + 1) l)[j - (take i l).length]?) =
    if j < i then l[j]? else l[j + 1]?

Proof state:
case isFalse.isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
h' : j < i
h✝ : l.length < i
h : l.length ≤ j
⊢ l.length ≤ i + 1 + (j - min i l.length)

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
⊢ (if j < (take i l).length then (take i l)[j]? else (drop (i + 1) l)[j - (take i l).length]?) =
    if j < i then l[j]? else l[j + 1]?

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
l : List α
i j : Nat
h : j < (take i l).length
⊢ (take i l)[j]? = if j < i then l[j]? else l[j + 1]?

case isFalse
α : Type u_1
l : List α
i j : Nat
h : ¬j < (take i l).length
⊢ (drop (i + 1) l)[j - (take i l).length]? = if j < i then l[j]? else l[j + 1]?

Proof state:
case isFalse
α : Type u_1
l : List α
i j : Nat
h : ¬j < (take i l).length
⊢ l[i + 1 + (j - (take i l).length)]? = if j < i then l[j]? else l[j + 1]?

Tactic:
split <;> rename_i h'

Result:
case isFalse.isTrue
α : Type u_1
l : List α
i j : Nat
h : ¬j < (take i l).length
h' : j < i
⊢ l[i + 1 + (j - (take i l).length)]? = l[j]?

case isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
h : ¬j < (take i l).length
h' : ¬j < i
⊢ l[i + 1 + (j - (take i l).length)]? = l[j + 1]?

Proof state:
case isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
h : j < min i l.length
h✝ : i ≤ j
⊢ l.length ≤ j + 1

Tactic:
omega

Result:
no goals

Proof state:
case isFalse.isTrue.isTrue
α : Type u_1
l : List α
i j : Nat
h' : j < i
h✝ : i ≤ l.length
h : i ≤ j
⊢ l[i + 1 + (j - (take i l).length)]? = l[j]?

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
h : j < (take i l).length
h✝ : ¬j < i
⊢ none = l[j + 1]?

Tactic:
simp_all

Result:
case isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
h : j < min i l.length
h✝ : i ≤ j
⊢ l.length ≤ j + 1

Proof state:
case isTrue
α : Type u_1
l : List α
i j : Nat
h : j < (take i l).length
⊢ (take i l)[j]? = if j < i then l[j]? else l[j + 1]?

Tactic:
rw [getElem?_take]

Result:
case isTrue
α : Type u_1
l : List α
i j : Nat
h : j < (take i l).length
⊢ (if j < i then l[j]? else none) = if j < i then l[j]? else l[j + 1]?

Proof state:
case isTrue
α : Type u_1
l : List α
i j : Nat
h : j < (take i l).length
⊢ (if j < i then l[j]? else none) = if j < i then l[j]? else l[j + 1]?

Tactic:
split

Result:
case isTrue.isTrue
α : Type u_1
l : List α
i j : Nat
h : j < (take i l).length
h✝ : j < i
⊢ l[j]? = l[j]?

case isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
h : j < (take i l).length
h✝ : ¬j < i
⊢ none = l[j + 1]?

Proof state:
case isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
h : ¬j < (take i l).length
h' : ¬j < i
⊢ l[i + 1 + (j - min i l.length)]? = l[j + 1]?

Tactic:
simp only [length_take, Nat.min_def, Nat.not_lt] at h

Result:
case isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
h' : ¬j < i
h : (if i ≤ l.length then i else l.length) ≤ j
⊢ l[i + 1 + (j - min i l.length)]? = l[j + 1]?

Proof state:
case isFalse.isTrue
α : Type u_1
l : List α
i j : Nat
h' : j < i
h : (if i ≤ l.length then i else l.length) ≤ j
⊢ l[i + 1 + (j - (take i l).length)]? = l[j]?

Tactic:
split at h

Result:
case isFalse.isTrue.isTrue
α : Type u_1
l : List α
i j : Nat
h' : j < i
h✝ : i ≤ l.length
h : i ≤ j
⊢ l[i + 1 + (j - (take i l).length)]? = l[j]?

case isFalse.isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
h' : j < i
h✝ : ¬i ≤ l.length
h : l.length ≤ j
⊢ l[i + 1 + (j - (take i l).length)]? = l[j]?