ι : Type ?u.220838
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
n : ℕ
l : List α
h : n < length l
⊢ take n l ++ modifyHead f (get l { val := n, isLt := h } :: drop (n + 1) l) =
    take n l ++ f (get l { val := n, isLt := h }) :: drop (n + 1) l
ι : Type ?u.220838
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
n : ℕ
l : List α
h : n < length l
⊢ modifyNth f n l = take n l ++ f (get l { val := n, isLt := h }) :: drop (n + 1) l
rw [modifyNth_eq_take_drop, drop_eq_get_cons h]
no goals
ι : Type ?u.220838
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
n : ℕ
l : List α
h : n < length l
⊢ take n l ++ modifyHead f (get l { val := n, isLt := h } :: drop (n + 1) l) =
    take n l ++ f (get l { val := n, isLt := h }) :: drop (n + 1) l
rfl