toList_tail — Mathlib

English

The list of tail elements is the tail of the list of p: (p.tail hp).toList = p.toList.tail.

Русский

Список хвостовых элементов равен хвосту списка p: (p.tail hp).toList = p.toList.tail.

LaTeX

$$$ (p.tail\ hp).toList = p.toList.tail $$$

Lean4

@[simp]
theorem toList_tail {p : RelSeries r} (hp : p.length ≠ 0) : (p.tail hp).toList = p.toList.tail :=
  by
  refine List.ext_getElem ?_ fun i h1 h2 ↦ ?_
  · simp
    cutsat
  · rw [List.getElem_tail, toList_getElem_eq_apply_of_lt_length (by simp_all),
      toList_getElem_eq_apply_of_lt_length (by simp_all)]
    simp_all [Fin.tail]

Похожие утверждения