cons_tail_dropLast_concat — Mathlib

English

A structural concatenation identity: the cons of U onto the tail of p after dropping last, followed by D, yields p.

Русский

Структурная тождественность конструирования: U :: tail(p.dropLast) ++ [D] = p.

LaTeX

$$$$ U :: p.toList.dropLast.tail ++ [D] = p $$$$

Lean4

theorem cons_tail_dropLast_concat : U :: p.toList.dropLast.tail ++ [D] = p :=
  by
  have h' := toList_ne_nil.mpr h
  have : p.toList.dropLast.take 1 = [p.toList.head h'] :=
    by
    rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
    · tauto
    · rename_i bal _
      cases s <;> simp at bal
    · tauto
  nth_rw 2 [← p.toList.dropLast_append_getLast h', ← p.toList.dropLast.take_append_drop 1]
  rw [getLast_eq_D, drop_one, this, head_eq_U]
  rfl

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