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

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 + 1) l).eraseIdx i).length
h' : j + 1 = 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 + 1 = k then f l[k] else l[k] else if j + 1 = 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 + 1) l).eraseIdx i).length
h' : ¬j + 1 = 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 + 1 = k then f l[k] else l[k] else if j + 1 = k + 1 then f l[k + 1] else l[k + 1]

Tactic:
repeat' split

Result:
case pos.isTrue.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 + 1) l).eraseIdx i).length
h' : j + 1 = k + 1
h✝² : j = k
h✝¹ : k < i
h✝ : j + 1 = k
⊢ f l[k] = f l[k]

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

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

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

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

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

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

case neg.isFalse.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 + 1) l).eraseIdx i).length
h' : ¬j + 1 = k + 1
h✝² : ¬j = k
h✝¹ : k < i
h✝ : ¬j + 1 = k
⊢ 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 + 1) l).eraseIdx i).length
h' : ¬j + 1 = k + 1
h✝¹ : ¬j = k
h✝ : ¬k < i
⊢ l[k + 1] = l[k + 1]

Proof state:
case pos.isTrue.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 + 1) l).eraseIdx i).length
h' : j + 1 = k + 1
h✝² : j = k
h✝¹ : k < i
h✝ : j + 1 = k
⊢ f l[k] = f l[k]

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

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

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

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

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

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

case neg.isFalse.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 + 1) l).eraseIdx i).length
h' : ¬j + 1 = k + 1
h✝² : ¬j = k
h✝¹ : k < i
h✝ : ¬j + 1 = k
⊢ 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 + 1) l).eraseIdx i).length
h' : ¬j + 1 = k + 1
h✝¹ : ¬j = k
h✝ : ¬k < i
⊢ l[k + 1] = l[k + 1]

Tactic:
all_goals (first | rfl | omega)

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