English
The toList of the concatenated series equals the concatenation of toLists: toList(p ⧺ q) = toList(p) ++ toList(q).
Русский
У.toList конкатенированного ряда равно конкатенации toList(p) и toList(q).
LaTeX
$$$ (p \\append q \\;\\text{connect}).toList = p.toList \\;\\!\\!\\!++\\; q.toList $$$
Lean4
@[simp]
theorem toList_append (p q : RelSeries r) (connect : p.last ~[r] q.head) :
(p.append q connect).toList = p.toList ++ q.toList :=
by
apply List.ext_getElem
· simp
cutsat
· intro i h1 h2
have h3' : i < p.length + 1 + (q.length + 1) := by simp_all
rw [toList_getElem_eq_apply_of_lt_length (by simp; cutsat)]
· simp only [append, Function.comp_apply, Fin.cast_mk, List.getElem_append]
split
· have : Fin.mk i h3' = Fin.castAdd _ ⟨i, by simp_all⟩ := rfl
rw [this, Fin.append_left, toList_getElem_eq_apply_of_lt_length]
· simp_all only [length_toList]
have : Fin.mk i h3' = Fin.natAdd _ ⟨i - p.length - 1, by omega⟩ := by simp_all; cutsat
rw [this, Fin.append_right, toList_getElem_eq_apply_of_lt_length]
rfl
