English
For s, a, connect and i ∈ Fin(s.length+1), the value at i.castSucc in (s.snoc a connect) equals the value at i in s: (s.snoc a connect).toFun i.castSucc = s.toFun i.
Русский
Для s, a, connect и i ∈ Fin(s.length+1) значение на i.castSucc в (s.snoc a connect) равно значению на i в s: (s.snoc a connect).toFun i.castSucc = s.toFun i.
LaTeX
$$$ (s.\text{snoc } a\ connect).toFun i.castSucc = s.toFun i $$$
Lean4
@[simp]
theorem snoc_castSucc (s : RelSeries r) (a : α) (connect : s.last ~[r] a) (i : Fin (s.length + 1)) :
snoc s a connect (Fin.castSucc i) = s i :=
Fin.append_left _ _ i