α : Type u_1
f : α → α
n : Nat
l : List α
h : n < length l
⊢ Option.getD ((fun a => set l n (f a)) <$> some (get l { val := n, isLt := h })) l =
    set l n (f (get l { val := n, isLt := h }))
α : Type u_1
f : α → α
n : Nat
l : List α
h : n < length l
⊢ modifyNth f n l = set l n (f (get l { val := n, isLt := h }))
rw [modifyNth_eq_set_get?, get?_eq_get h]
no goals
α : Type u_1
f : α → α
n : Nat
l : List α
h : n < length l
⊢ Option.getD ((fun a => set l n (f a)) <$> some (get l { val := n, isLt := h })) l =
    set l n (f (get l { val := n, isLt := h }))
rfl