no goals
α : Type u_1
f : α → α
l : List α
⊢ modifyNth f 0 l = Option.getD ((fun a => set l 0 (f a)) <$> get? l 0) l
cases l <;> rfl
no goals
α : Type u_1
f : α → α
n : Nat
b : α
l : List α
⊢ b :: Option.getD ((fun a => set l (Nat.add n 0) (f a)) <$> get? l (Nat.add n 0)) l =
    Option.getD ((fun a => set (b :: l) (n + 1) (f a)) <$> get? (b :: l) (n + 1)) (b :: l)
cases l.get? n <;> rfl