English
Let a: Fin n → α and m1, m2 ∈ ℕ. The repeat by m1+m2 equals the composition of the concatenation Fin.repeat m1 a and Fin.repeat m2 a with the cast for addition.
Русский
Пусть a: Fin n → α и m1, m2 ∈ ℕ. Повторение суммой m1+m2 эквивалентно конкатенации Fin.repeat m1 a и Fin.repeat m2 a с соответствующим отображением сложения.
LaTeX
$$$\\mathrm{Fin.repeat}(m_1 + m_2)\\,a = \\mathrm{append}(\\mathrm{Fin.repeat}m_1\\,a)\\ (\\mathrm{Fin.repeat}m_2\\,a) \\circ \\mathrm{Fin.cast}(\\mathrm{Nat.add\\_mul}\\,\\_).$$$
Lean4
@[simp]
theorem repeat_add (a : Fin n → α) (m₁ m₂ : ℕ) :
Fin.repeat (m₁ + m₂) a = append (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ Fin.cast (Nat.add_mul ..) :=
by
generalize_proofs h
apply funext
rw [(Fin.rightInverse_cast h.symm).surjective.forall]
refine Fin.addCases (fun l => ?_) fun r => ?_
· simp [modNat]
· simp [modNat, Nat.add_mod]
