ι : Type ?u.108636
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : List α → List α
n : ℕ
l : List α
⊢ modifyNthTail (fun l => modifyNthTail g 0 (f l)) n l = modifyNthTail (g ∘ f) n l
ι : Type ?u.108636
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : List α → List α
n : ℕ
l : List α
⊢ modifyNthTail g n (modifyNthTail f n l) = modifyNthTail (g ∘ f) n l
rw [modifyNthTail_modifyNthTail_le n n l (le_refl n), tsub_self]
no goals
ι : Type ?u.108636
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : List α → List α
n : ℕ
l : List α
⊢ modifyNthTail (fun l => modifyNthTail g 0 (f l)) n l = modifyNthTail (g ∘ f) n l
rfl