-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem set_getElem_succ_eraseIdx_succ
    {l : List α} {i : Nat} (h : i + 1 < l.length) :
    (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i

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

Tactic:
simp_all

Result:
no goals

Proof state:
case hl.hc
α : Type u_1
l : List α
i : Nat
h : i + 1 < l.length
⊢ i < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
h : i + 1 < l.length
n : Nat
h₁ : n < ((l.eraseIdx (i + 1)).set i l[i + 1]).length
h₂ : n < (l.eraseIdx i).length
h✝¹ : ¬i = n
h✝ : ¬n < i + 1
⊢ ¬n < i

Tactic:
omega

Result:
no goals

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

Tactic:
omega

Result:
no goals

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

Tactic:
simp [getElem_set, getElem_eraseIdx]

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

Proof state:
case hl
α : Type u_1
l : List α
i : Nat
h : i + 1 < l.length
⊢ ((l.eraseIdx (i + 1)).set i l[i + 1]).length = (l.eraseIdx i).length

Tactic:
simp only [length_set, length_eraseIdx, h, ↓reduceIte]

Result:
case hl
α : Type u_1
l : List α
i : Nat
h : i + 1 < l.length
⊢ l.length - 1 = if i < l.length then l.length - 1 else l.length

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

Tactic:
intro n h₁ h₂

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

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

Tactic:
split

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

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

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

Tactic:
split

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

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

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

Tactic:
have t : ¬ n < i := by omega

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

Proof state:
case hl
α : Type u_1
l : List α
i : Nat
h : i + 1 < l.length
⊢ l.length - 1 = if i < l.length then l.length - 1 else l.length

Tactic:
rw [if_pos]

Result:
case hl.hc
α : Type u_1
l : List α
i : Nat
h : i + 1 < l.length
⊢ i < l.length

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

Tactic:
omega

Result:
no goals

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

Tactic:
simp [t]

Result:
no goals

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

Tactic:
split

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

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

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

Tactic:
split

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

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

Proof state:
α : Type u_1
l : List α
i : Nat
h : i + 1 < l.length
⊢ (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
l : List α
i : Nat
h : i + 1 < l.length
⊢ ((l.eraseIdx (i + 1)).set i l[i + 1]).length = (l.eraseIdx i).length

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

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

Tactic:
rfl

Result:
no goals