English
Let a: Fin n → α and m: ℕ. The (m+1)-fold repeat is obtained by appending the m-fold repeat to a and reindexing via Fin.cast of the appropriate addition-multiplication map.
Русский
Пусть a: Fin n → α и m: ℕ. (m+1)-кратное повторение получается добавлением к a m-раз повторения и повторной индексацией с помощью соответствующего отображения сложения.
LaTeX
$$$\\mathrm{Fin.repeat}(m\\!\\text{-}\\!\\mathrm{succ})\\,a = \\mathrm{append}\\,a\\ (\\mathrm{Fin.repeat}\\,m\\,a) \\circ \\mathrm{Fin.cast}((\\mathrm{Nat.succ\\_mul}\\ _\\ _).trans (\\mathrm{Nat.add\\_comm}\\ _)).$$$
Lean4
theorem repeat_succ (a : Fin n → α) (m : ℕ) :
Fin.repeat m.succ a = append a (Fin.repeat m a) ∘ Fin.cast ((Nat.succ_mul _ _).trans (Nat.add_comm ..)) :=
by
generalize_proofs h
apply funext
rw [(Fin.rightInverse_cast h.symm).surjective.forall]
refine Fin.addCases (fun l => ?_) fun r => ?_
· simp [modNat, Nat.mod_eq_of_lt l.is_lt]
· simp [modNat]
