English
For m,n and xs : Fin m → α, ys : Fin n → α, and i : Fin (m+n), the reversed-index equality holds: append xs ys i.rev = append (ys ∘ rev) (xs ∘ rev) (i.cast (Nat.add_comm ..)).
Русский
Для m,n и xs : Fin m → α, ys : Fin n → α и i : Fin (m+n) выполняется: append xs ys i.rev = append (ys ∘ rev) (xs ∘ rev) (i.cast (Nat.add_comm ..)).
LaTeX
$$$\\mathrm{append}(xs,ys)(i.rev) = \\mathrm{append}(ys\\circ\\mathrm{rev}, xs\\circ\\mathrm{rev}) (i.cast(\\mathrm{Nat.add\\_comm}())).$$$
Lean4
theorem append_rev {m n} (xs : Fin m → α) (ys : Fin n → α) (i : Fin (m + n)) :
append xs ys (rev i) = append (ys ∘ rev) (xs ∘ rev) (i.cast (Nat.add_comm ..)) :=
by
rcases rev_surjective i with ⟨i, rfl⟩
rw [rev_rev]
induction i using Fin.addCases
· simp [rev_castAdd]
· simp [cast_rev, rev_addNat]
