English
Let p and q be finite relation series with p.last = q.head. Form their concatenation smash(p, q, h). Then for every i in Fin(q.length), the element at position |p| + i + 1 of smash(p, q, h) equals the (i+1)-th element of q. In other words, the tail part coming from q aligns exactly with q beyond its head after the join point.
Русский
Пусть p, q — конечные реляционные ряды such that p.last = q.head. Тогда для любого i из Fin(q.length) элемент на позиции |p| + i + 1 в smash(p, q, h) равен i+1-му элементу q. Иными словами, часть, полученная из q, совпадает с q начиная со второго элемента после точки соединения.
LaTeX
$$$$ (\\text{smash}(p,q,h))_{|p|+i+1} = q_{i+1} \\quad \\text{for all } i \\text{ with } 0 \\le i < |q|. $$$$
Lean4
theorem smash_succ_natAdd {p q : RelSeries r} (h : p.last = q.head) (i : Fin q.length) :
smash p q h (i.natAdd p.length).succ = q i.succ :=
by
dsimp only [smash, Fin.succ_natAdd]
apply Fin.addCases_right
