English
Coning a to the front of a snoc-tuple is the same as snoc-ing after consing the head: cons a (snoc q b) = snoc (cons a q) b.
Русский
Додавание элемента спереди кортежа, образованного snoc, эквивалентно snoc после применения cons: cons a (snoc q b) = snoc (cons a q) b.
LaTeX
$$$\\\\operatorname{cons}\\\\;a\\\\; (\\\\operatorname{snoc} q b) = \\\\operatorname{snoc}(\\\\operatorname{cons} a q) b$$$
Lean4
/-- `cons` and `snoc` commute. We state this lemma in a non-dependent setting, as otherwise it
would involve a cast to convince Lean that the two types are equal, making it harder to use. -/
theorem cons_snoc_eq_snoc_cons {β : Sort*} (a : β) (q : Fin n → β) (b : β) :
@cons n.succ (fun _ ↦ β) a (snoc q b) = snoc (cons a q) b :=
by
ext i
cases i using Fin.cases with
| zero => simp
| succ j =>
cases j using Fin.lastCases with
| last => simp
| cast j =>
rw [cons_succ]
simp [← castSucc_succ]
