-- 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.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
h✝ : ¬i - 1 = n
⊢ l[n] = l[n]

Tactic:
rfl

Result:
no goals

Proof state:
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]

Tactic:
omega

Result:
no goals

Proof state:
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

Tactic:
rfl

Result:
no goals

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

Tactic:
apply ext_getElem

Result:
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

case h
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
⊢ ∀ (i_1 : Nat) (h₁ : i_1 < ((l.set i a).eraseIdx j).length) (h₂ : i_1 < ((l.eraseIdx j).set (i - 1) a).length),
    ((l.set i a).eraseIdx j)[i_1] = ((l.eraseIdx j).set (i - 1) a)[i_1]

Proof state:
case h
α : Type u_1
l : List α
i j : Nat
a : α
h : j < i
⊢ ∀ (i_1 : Nat) (h₁ : i_1 < ((l.set i a).eraseIdx j).length) (h₂ : i_1 < ((l.eraseIdx j).set (i - 1) a).length),
    ((l.set i a).eraseIdx j)[i_1] = ((l.eraseIdx j).set (i - 1) a)[i_1]

Tactic:
intro n h₁ h₂

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
⊢ ((l.set i a).eraseIdx j)[n] = ((l.eraseIdx j).set (i - 1) a)[n]

Proof state:
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]

Tactic:
split

Result:
case h.isTrue.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
h✝ : i - 1 = n
⊢ l[n] = a

case h.isTrue.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
h✝ : ¬i - 1 = n
⊢ l[n] = 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
⊢ ((l.set i a).eraseIdx j)[n] = ((l.eraseIdx j).set (i - 1) a)[n]

Tactic:
simp only [length_eraseIdx, length_set] at h₁

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
⊢ ((l.set i a).eraseIdx j)[n] = ((l.eraseIdx j).set (i - 1) a)[n]

Proof state:
case h.isTrue.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
h✝ : i - 1 = n
⊢ l[n] = a

Tactic:
omega

Result:
no goals