English
Applying vecAlt1 to vecAppend of v with itself yields v composed with the map n ↦ (2n)+1.
Русский
Применение vecAlt1 к vecAppend(v,v) даёт v после индексации по (2n+1).
LaTeX
$$$\\text{vecAlt1}(hm,\\mathrm{vecAppend}\\,v\\,v) = v \\circ (\\lambda n. (2n)+1)$$$
Lean4
theorem vecAlt1_vecAppend (v : Fin (n + 1) → α) : vecAlt1 rfl (vecAppend rfl v v) = v ∘ (fun n ↦ (n + n) + 1) :=
by
ext i
simp_rw [Function.comp, vecAlt1, vecAppend_eq_ite]
cases n with
| zero =>
obtain ⟨i, hi⟩ := i
simp only [Nat.zero_add, Nat.lt_one_iff] at hi; subst i; rfl
| succ n =>
split_ifs with h <;> congr
· simp [Nat.mod_eq_of_lt, h]
· rw [Fin.val_mk, not_lt] at h
simp only [Nat.mod_add_mod, Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by cutsat)]
refine (Nat.mod_eq_of_lt ?_).symm
cutsat
