no goals
ι : Type ?u.221077
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
l : List α
h : n < length l
⊢ set l n a = take n l ++ a :: drop (n + 1) l
rw [set_eq_modifyNth, modifyNth_eq_take_cons_drop _ h]