-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem eraseIdx_set_lt {l : List α} {i : Nat} {j : Nat} {a : α} (h : j < i) :
    (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a

Proof state:
case h.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝ : n < j
⊢ (if i = n then a else l[n]) = if i - 1 = n then a else l[n]

Tactic:
split

Result:
case h.isTrue.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝¹ : n < j
h✝ : i = n
⊢ a = if i - 1 = n then a else l[n]

case h.isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝¹ : n < j
h✝ : ¬i = n
⊢ l[n] = if i - 1 = n then a else l[n]

Proof state:
case h
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
⊢ (if h : n < j then if i = n then a else l[n] else if i = n + 1 then a else l[n + 1]) =
    if i - 1 = n then a else if h' : n < j then l[n] else l[n + 1]

Tactic:
split

Result:
case h.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝ : n < j
⊢ (if i = n then a else l[n]) = if i - 1 = n then a else l[n]

case h.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝ : ¬n < j
⊢ (if i = n + 1 then a else l[n + 1]) = if i - 1 = n then a else l[n + 1]

Proof state:
case h.isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝¹ : ¬n < j
h✝ : ¬i = n + 1
t : i - 1 ≠ n
⊢ l[n + 1] = if i - 1 = n then a else l[n + 1]

Tactic:
simp [t]

Result:
no goals

Proof state:
case h.isTrue.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝¹ : n < j
h✝ : i = n
⊢ a = if i - 1 = n then a else l[n]

Tactic:
split

Result:
case h.isTrue.isTrue.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝² : n < j
h✝¹ : i = n
h✝ : i - 1 = n
⊢ a = a

case h.isTrue.isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝² : n < j
h✝¹ : i = n
h✝ : ¬i - 1 = n
⊢ a = l[n]

Proof state:
case h.isFalse.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝¹ : ¬n < j
h✝ : i = n + 1
⊢ a = if i - 1 = n then a else l[n + 1]

Tactic:
split

Result:
case h.isFalse.isTrue.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝² : ¬n < j
h✝¹ : i = n + 1
h✝ : i - 1 = n
⊢ a = a

case h.isFalse.isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝² : ¬n < j
h✝¹ : i = n + 1
h✝ : ¬i - 1 = n
⊢ a = l[n + 1]

Proof state:
case hl
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
⊢ ((l.set i a).eraseIdx j).length = ((l.eraseIdx j).set (i - 1) a).length

Tactic:
simp [length_eraseIdx]

Result:
no goals

Proof state:
case h.isFalse.isTrue.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝² : ¬n < j
h✝¹ : i = n + 1
h✝ : i - 1 = n
⊢ a = a

Tactic:
rfl

Result:
no goals

Proof state:
case h.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝ : ¬n < j
⊢ (if i = n + 1 then a else l[n + 1]) = if i - 1 = n then a else l[n + 1]

Tactic:
split

Result:
case h.isFalse.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝¹ : ¬n < j
h✝ : i = n + 1
⊢ a = if i - 1 = n then a else l[n + 1]

case h.isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝¹ : ¬n < j
h✝ : ¬i = n + 1
⊢ l[n + 1] = if i - 1 = n then a else l[n + 1]

Proof state:
case h.isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝¹ : ¬n < j
h✝ : ¬i = n + 1
⊢ l[n + 1] = if i - 1 = n then a else l[n + 1]

Tactic:
have t : i - 1 ≠ n := by omega

Result:
case h.isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝¹ : ¬n < j
h✝ : ¬i = n + 1
t : i - 1 ≠ n
⊢ l[n + 1] = if i - 1 = n then a else l[n + 1]

Proof state:
case h
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
⊢ ((l.set i a).eraseIdx j)[n] = ((l.eraseIdx j).set (i - 1) a)[n]

Tactic:
simp only [getElem_eraseIdx, getElem_set]

Result:
case h
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
⊢ (if h : n < j then if i = n then a else l[n] else if i = n + 1 then a else l[n + 1]) =
    if i - 1 = n then a else if h' : n < j then l[n] else l[n + 1]

Proof state:
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝¹ : ¬n < j
h✝ : ¬i = n + 1
⊢ i - 1 ≠ n

Tactic:
omega

Result:
no goals

Proof state:
case h.isFalse.isTrue.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set (i - 1) a).length
h₁ : n < if j < l.length then l.length - 1 else l.length
h✝² : ¬n < j
h✝¹ : i = n + 1
h✝ : ¬i - 1 = n
⊢ a = l[n + 1]

Tactic:
omega

Result:
no goals