no goals
ι : Type ?u.109543
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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.109543
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
n : ℕ
b : α
l : List α
⊢ b :: Option.getD ((fun a => set l n (f a)) <$> get? l n) l =
    Option.getD ((fun a => set (b :: l) (n + 1) (f a)) <$> get? (b :: l) (n + 1)) (b :: l)
cases get? l n <;> rfl