-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_eraseIdx_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
    (l.eraseIdx i).modify f j = (l.modify f j).eraseIdx i

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

Tactic:
split

Result:
case neg.isFalse.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : ¬j = k
h✝ : k < i
⊢ l[k] = l[k]

case neg.isFalse.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : ¬j = k
h✝ : ¬k < i
⊢ l[k + 1] = l[k + 1]

Proof state:
case neg.isFalse.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : ¬j = k
h✝ : ¬k < i
⊢ l[k + 1] = l[k + 1]

Tactic:
rfl

Result:
no goals

Proof state:
case neg.isFalse.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : ¬j = k
h✝ : ¬k < i
⊢ l[k + 1] = l[k + 1]

Tactic:
(first | rfl | omega)

Result:
no goals

Proof state:
case pos
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : j = k + 1
⊢ (if j = k then f (if h' : k < i then l[k] else l[k + 1]) else if h' : k < i then l[k] else l[k + 1]) =
    if h : k < i then if j = k then f l[k] else l[k] else if j = k + 1 then f l[k + 1] else l[k + 1]

case neg
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
⊢ (if j = k then f (if h' : k < i then l[k] else l[k + 1]) else if h' : k < i then l[k] else l[k + 1]) =
    if h : k < i then if j = k then f l[k] else l[k] else if j = k + 1 then f l[k + 1] else l[k + 1]

Tactic:
repeat' split

Result:
case pos.isTrue.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : j = k + 1
h✝¹ : j = k
h✝ : k < i
⊢ f l[k] = f l[k]

case pos.isTrue.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : j = k + 1
h✝¹ : j = k
h✝ : ¬k < i
⊢ f l[k + 1] = f l[k + 1]

case pos.isFalse.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : j = k + 1
h✝¹ : ¬j = k
h✝ : k < i
⊢ l[k] = l[k]

case pos.isFalse.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : j = k + 1
h✝¹ : ¬j = k
h✝ : ¬k < i
⊢ l[k + 1] = f l[k + 1]

case neg.isTrue.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : j = k
h✝ : k < i
⊢ f l[k] = f l[k]

case neg.isTrue.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : j = k
h✝ : ¬k < i
⊢ f l[k + 1] = l[k + 1]

case neg.isFalse.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : ¬j = k
h✝ : k < i
⊢ l[k] = l[k]

case neg.isFalse.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : ¬j = k
h✝ : ¬k < i
⊢ l[k + 1] = l[k + 1]

Proof state:
case neg.isFalse.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : ¬j = k
h✝ : ¬k < i
⊢ l[k + 1] = l[k + 1]

Tactic:
first | rfl | omega

Result:
no goals

Proof state:
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
⊢ modify f j (l.eraseIdx i) = (modify f j l).eraseIdx i

Tactic:
apply ext_getElem

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

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

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

Tactic:
by_cases h' : j = k + 1

Result:
case pos
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : j = k + 1
⊢ (if j = k then f (if h' : k < i then l[k] else l[k + 1]) else if h' : k < i then l[k] else l[k + 1]) =
    if h : k < i then if j = k then f l[k] else l[k] else if j = k + 1 then f l[k + 1] else l[k + 1]

case neg
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
⊢ (if j = k then f (if h' : k < i then l[k] else l[k + 1]) else if h' : k < i then l[k] else l[k + 1]) =
    if h : k < i then if j = k then f l[k] else l[k] else if j = k + 1 then f l[k + 1] else l[k + 1]

Proof state:
case h
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
⊢ (modify f j (l.eraseIdx i))[k] = ((modify f j l).eraseIdx i)[k]

Tactic:
simp only [getElem_eraseIdx, getElem_modify]

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

Proof state:
case neg.isTrue.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : j = k
h✝ : ¬k < i
⊢ f l[k + 1] = l[k + 1]

Tactic:
omega

Result:
no goals