English
For p, q and i, if p.last = q.head, then smashing p with q at index i.castAdd q.length yields the same value as p at i.castSucc: p.smash q h (i.castAdd q.length).castSucc = p i.castSucc.
Русский
Если p.last = q.head, то слитие p и q в позиции i.castAdd q.length эквивалентно значению p на i.castSucc: p.smash q h (i.castAdd q.length).castSucc = p i.castSucc.
LaTeX
$$$ p.smash q h (i.castAdd q.length).castSucc = p i.castSucc $$$
Lean4
theorem smash_castLE {p q : RelSeries r} (h : p.last = q.head) (i : Fin (p.length + 1)) :
p.smash q h (i.castLE (by simp)) = p i :=
by
refine i.lastCases ?_ fun _ ↦ by dsimp only [smash]; apply Fin.addCases_left
change p.smash q h (Fin.natAdd p.length (0 : Fin (q.length + 1))) = _
simpa only [smash, Fin.addCases_right] using h.symm
