dropLast_tail — Mathlib

English

If L is nonempty and the first element equals the last element, then L.dropLast is rotated to L.tail.

Русский

Если L непуст и его первый элемент равен последнему элементу, то L.dropLast является поворотом L.tail.

LaTeX

$$$L.dropLast ~r L.tail$$$

Lean4

theorem dropLast_tail {α} {L : List α} (hL : L ≠ []) (hL' : L.head hL = L.getLast hL) : L.dropLast ~r L.tail :=
  match L with
  | [] => by simp
  | [_] => by simp
  | a :: b :: L => by
    simp only [head_cons, ne_eq, reduceCtorEq, not_false_eq_true, getLast_cons] at hL'
    simp [hL', IsRotated.cons_getLast_dropLast]

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