English
Taking m+1 elements equals taking m elements and appending the (m+1)-th value; i.e., take m.succ h v = snoc (take m h.le v) (v ⟨m, h⟩).
Русский
Взятые (m+1) элементов равны взятию m элементов с дописыванием (m+1)-го значения; т.е. take m.succ h v = snoc (take m h.le v) (v ⟨m, h⟩).
LaTeX
$$$\\mathrm{take}_{m.succ}(h)\,v = \\mathrm{snoc}\\bigl(\\mathrm{take}_{m}(h.le)\,v\\bigr)\\; v_{⟨m,h⟩}$$$
Lean4
/-- Taking `m + 1` elements is equal to taking `m` elements and adding the `(m + 1)`th one. -/
theorem take_succ_eq_snoc (m : ℕ) (h : m < n) (v : (i : Fin n) → α i) :
take m.succ h v = snoc (take m h.le v) (v ⟨m, h⟩) := by
ext i
induction m with
| zero =>
have h' : i = 0 := by ext; simp
subst h'
simp [take, snoc, castLE]
| succ m _ =>
induction i using reverseInduction with
| last => simp [take, snoc]; congr
| cast i _ => simp
