α : Type u_1
n : Nat
a' : α
l : List α
h : n < length l
⊢ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ length l₁ = n ∧ modifyNth (fun x => a') n l = l₁ ++ a' :: l₂
α : Type u_1
n : Nat
a' : α
l : List α
h : n < length l
⊢ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ length l₁ = n ∧ set l n a' = l₁ ++ a' :: l₂
rw [set_eq_modifyNth]
no goals
α : Type u_1
n : Nat
a' : α
l : List α
h : n < length l
⊢ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ length l₁ = n ∧ modifyNth (fun x => a') n l = l₁ ++ a' :: l₂
exact exists_of_modifyNth _ h