-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem eraseIdx_modify_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
    (modify f i l).eraseIdx j = (l.eraseIdx j).modify f (i - 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 i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : ¬i - 1 = k
h✝¹ : ¬k < j
h✝ : ¬i = k + 1
⊢ l[k + 1] = l[k + 1]

Tactic:
rfl

Result:
no goals

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

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

case neg
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : ¬i - 1 = k
⊢ (if h : k < j then if i = k then f l[k] else l[k] else if i = k + 1 then f l[k + 1] else l[k + 1]) =
    if i - 1 = k then f (if h' : k < j then l[k] else l[k + 1]) else if h' : k < j then l[k] 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 i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : i - 1 = k
h✝¹ : k < j
h✝ : i = k
⊢ 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 i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : i - 1 = k
h✝¹ : k < j
h✝ : ¬i = k
⊢ l[k] = f l[k]

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

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

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

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

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

Tactic:
first | rfl | omega

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 i l).eraseIdx j).length
h₂ : k < (modify f (i - 1) (l.eraseIdx j)).length
h' : ¬i - 1 = k
h✝¹ : ¬k < j
h✝ : ¬i = k + 1
⊢ l[k + 1] = l[k + 1]

Tactic:
(first | rfl | omega)

Result:
no goals

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

Tactic:
by_cases h' : i - 1 = k

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

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

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

Tactic:
apply ext_getElem

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

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

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

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

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

Tactic:
simp [length_eraseIdx]

Result:
no goals

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

Tactic:
intro k h₁ h₂

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