ι : Type ?u.113196
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
l : List α
⊢ modifyNthTail (tail ∘ cons a) n l = l
ι : Type ?u.113196
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
l : List α
⊢ removeNth (insertNth n a l) n = l
rw [removeNth_eq_nth_tail, insertNth, modifyNthTail_modifyNthTail_same]
no goals
ι : Type ?u.113196
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
l : List α
⊢ modifyNthTail (tail ∘ cons a) n l = l
exact modifyNthTail_id _ _