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

Proof state:
case h.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : i < j
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i 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 = n then a else l[n]

Tactic:
rfl

Result:
no goals

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

Tactic:
rfl

Result:
no goals

Proof state:
case h.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : i < j
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i 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 = n then a else l[n + 1]

Tactic:
split

Result:
case h.isFalse.isTrue
α : Type u_1
l : List α
i j : Nat
a : α
h : i < j
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i 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 = n then a else l[n + 1]

case h.isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : i < j
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i 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 = n then a else l[n + 1]

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

Tactic:
intro n h₁ h₂

Result:
case h
α : Type u_1
l : List α
i j : Nat
a : α
h : i < j
n : Nat
h₁ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i a).length
⊢ ((l.set i a).eraseIdx j)[n] = ((l.eraseIdx j).set i a)[n]

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

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

Proof state:
case h.isFalse.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : i < j
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i 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 = n then a else l[n + 1]

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

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
apply ext_getElem

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

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

Proof state:
case h
α : Type u_1
l : List α
i j : Nat
a : α
h : i < j
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i 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 a)[n]

Tactic:
simp only [getElem_eraseIdx, getElem_set]

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

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

Tactic:
simp [t]

Result:
no goals

Proof state:
case h
α : Type u_1
l : List α
i j : Nat
a : α
h : i < j
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i 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 = 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 : i < j
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i 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 = n then a else l[n]

case h.isFalse
α : Type u_1
l : List α
i j : Nat
a : α
h : i < j
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i 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 = n then a else l[n + 1]

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

Tactic:
simp [length_eraseIdx]

Result:
no goals

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

Tactic:
omega

Result:
no goals

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

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

Result:
case h
α : Type u_1
l : List α
i j : Nat
a : α
h : i < j
n : Nat
h₁✝ : n < ((l.set i a).eraseIdx j).length
h₂ : n < ((l.eraseIdx j).set i 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 a)[n]