-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_eq_set [Inhabited α] (f : α → α) (n) (l : List α) :
    modify f n l = l.set n (f (l[n]?.getD default))

Proof state:
case h.isTrue
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
h₁✝ : n < (modify f n l).length
h₂ : n < (l.set n (f (l[n]?.getD default))).length
h₁ : n < l.length
⊢ f l[n] = f (l[n]?.getD default)

Tactic:
simp [h₁]

Result:
no goals

Proof state:
case hl
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
⊢ (modify f n l).length = (l.set n (f (l[n]?.getD default))).length

Tactic:
simp

Result:
no goals

Proof state:
case h.isFalse
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < (l.set n (f (l[n]?.getD default))).length
h : ¬n = m
⊢ l[m] = l[m]

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < (l.set n (f (l[n]?.getD default))).length
⊢ (if n = m then f l[m] else l[m]) = if n = m then f (l[n]?.getD default) else l[m]

Tactic:
split <;> rename_i h

Result:
case h.isTrue
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < (l.set n (f (l[n]?.getD default))).length
h : n = m
⊢ f l[m] = f (l[n]?.getD default)

case h.isFalse
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < (l.set n (f (l[n]?.getD default))).length
h : ¬n = m
⊢ l[m] = l[m]

Proof state:
case h.isTrue
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < (l.set n (f (l[n]?.getD default))).length
h : n = m
⊢ f l[m] = f (l[n]?.getD default)

Tactic:
subst h

Result:
case h.isTrue
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
h₁ : n < (modify f n l).length
h₂ : n < (l.set n (f (l[n]?.getD default))).length
⊢ f l[n] = f (l[n]?.getD default)

Proof state:
case h
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < (l.set n (f (l[n]?.getD default))).length
⊢ (modify f n l)[m] = (l.set n (f (l[n]?.getD default)))[m]

Tactic:
simp [getElem_modify, getElem_set, h₂]

Result:
case h
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < (l.set n (f (l[n]?.getD default))).length
⊢ (if n = m then f l[m] else l[m]) = if n = m then f (l[n]?.getD default) else l[m]

Proof state:
case h
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
⊢ ∀ (i : Nat) (h₁ : i < (modify f n l).length) (h₂ : i < (l.set n (f (l[n]?.getD default))).length),
    (modify f n l)[i] = (l.set n (f (l[n]?.getD default)))[i]

Tactic:
intro m h₁ h₂

Result:
case h
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < (l.set n (f (l[n]?.getD default))).length
⊢ (modify f n l)[m] = (l.set n (f (l[n]?.getD default)))[m]

Proof state:
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
⊢ modify f n l = l.set n (f (l[n]?.getD default))

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
⊢ (modify f n l).length = (l.set n (f (l[n]?.getD default))).length

case h
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
⊢ ∀ (i : Nat) (h₁ : i < (modify f n l).length) (h₂ : i < (l.set n (f (l[n]?.getD default))).length),
    (modify f n l)[i] = (l.set n (f (l[n]?.getD default)))[i]

Proof state:
case h.isTrue
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
h₁ : n < (modify f n l).length
h₂ : n < (l.set n (f (l[n]?.getD default))).length
⊢ f l[n] = f (l[n]?.getD default)

Tactic:
simp only [length_modify] at h₁

Result:
case h.isTrue
α : Type u_1
inst✝ : Inhabited α
f : α → α
n : Nat
l : List α
h₁✝ : n < (modify f n l).length
h₂ : n < (l.set n (f (l[n]?.getD default))).length
h₁ : n < l.length
⊢ f l[n] = f (l[n]?.getD default)