case intro
ι : Type ?u.108113
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : List α → List α
n : ℕ
l : List α
m : ℕ
h : n ≤ n + m
⊢ modifyNthTail g (n + m) (modifyNthTail f n l) = modifyNthTail (fun l => modifyNthTail g (n + m - n) (f l)) n l
ι : Type ?u.108113
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : List α → List α
m n : ℕ
l : List α
h : n ≤ m
⊢ modifyNthTail g m (modifyNthTail f n l) = modifyNthTail (fun l => modifyNthTail g (m - n) (f l)) n l
rcases exists_add_of_le h with ⟨m, rfl⟩
no goals
case intro
ι : Type ?u.108113
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : List α → List α
n : ℕ
l : List α
m : ℕ
h : n ≤ n + m
⊢ modifyNthTail g (n + m) (modifyNthTail f n l) = modifyNthTail (fun l => modifyNthTail g (n + m - n) (f l)) n l
rw [@add_tsub_cancel_left, add_comm, modifyNthTail_modifyNthTail]