English
Taking the first m elements of an appended sequence is the same as taking the first m elements of the left part.
Русский
Взятие первых m элементов у конкатенации равно взятию первых m элементов от левой части.
LaTeX
$$$\\forall {n' : \\mathbb{N}}\\ (m:\\mathbb{N})\\ (h:\\ m \\le n)\\ (u:(i:\\mathrm{Fin}(n))\\to \\mathrm{α})\\ (v:(i:\\mathrm{Fin}(n'))\\to \\mathrm{α}):\\ \\operatorname{take}(m,\\mathrm{Nat.le_add_right_of_le}\\,h)(\\mathrm{Fin.append}\\,u\\,v) = \\operatorname{take}(m,h) u$$$
Lean4
/-- Version of `take_addCases_left` that specializes `addCases` to `append`. -/
theorem take_append_left {n' : ℕ} {α : Sort*} (m : ℕ) (h : m ≤ n) (u : (i : Fin n) → α) (v : (i : Fin n') → α) :
take m (Nat.le_add_right_of_le h) (append u v) = take m h u :=
take_addCases_left m h _ _
