English
Appending in the order (append a b) then c is the same as appending a with (append b c), up to index shift by Nat.add_assoc.
Русский
Складывание последовательностей по схеме (append a b) затем c равно сложению a с (append b c) с сдвигом индексов на Nat.add_assoc.
LaTeX
$$$\\mathrm{append}(\\mathrm{append}(a,b), c) = \\mathrm{append}(a, \\mathrm{append}(b,c)) \\circ \\mathrm{Fin.cast}(\\mathrm{Nat.add_assoc}()).$$$
Lean4
theorem append_assoc {p : ℕ} (a : Fin m → α) (b : Fin n → α) (c : Fin p → α) :
append (append a b) c = append a (append b c) ∘ Fin.cast (Nat.add_assoc ..) :=
by
ext i
rw [Function.comp_apply]
refine Fin.addCases (fun l => ?_) (fun r => ?_) i
· rw [append_left]
refine Fin.addCases (fun ll => ?_) (fun lr => ?_) l
· rw [append_left]
simp [castAdd_castAdd]
· rw [append_right]
simp [castAdd_natAdd]
· rw [append_right]
simp [← natAdd_natAdd]
