English
Taking the first n+m elements of append u v equals append u with take m h v.
Русский
Взятие первых n+m элементов из append u v эквивалентно append u (take m h v).
LaTeX
$$$\\forall {n'}\\ (m:\\mathbb{N})\\ (h:\\ m \\le n')\\ (u:(i:\\mathrm{Fin}(n))\\to \\mathrm{α})\\ (v:(i:\\mathrm{Fin}(n'))\\to \\mathrm{α}):\\ \\operatorname{take}(\\mathrm{instHAdd.hAdd}\\,n\\,m)\\bigl(\\mathrm{append}\\,u\\,v\\bigr) = \\mathrm{append}\\,u\\bigl(\\operatorname{take} m h v\\bigr)$$$
Lean4
/-- Version of `take_addCases_right` that specializes `addCases` to `append`. -/
theorem take_append_right {n' : ℕ} {α : Sort*} (m : ℕ) (h : m ≤ n') (u : (i : Fin n) → α) (v : (i : Fin n') → α) :
take (n + m) (Nat.add_le_add_left h n) (append u v) = append u (take m h v) :=
take_addCases_right m h _ _
