getLast_eq_D — Mathlib

English

The last symbol of a nonempty Dyck word is D.

Русский

Последний символ непустого Dyck слова — D.

LaTeX

$$$$ p.toList.getLast h = D $$$$

Lean4

/-- The last element of a nonempty Dyck word is `D`. -/
theorem getLast_eq_D (p : DyckWord) (h) : p.toList.getLast h = D :=
  by
  by_contra f; have s := p.count_U_eq_count_D
  rw [← dropLast_append_getLast h, (dichotomy _).resolve_right f] at s
  simp_rw [dropLast_eq_take, count_append, count_singleton', ite_true, reduceCtorEq, ite_false] at s
  have := p.count_D_le_count_U (p.toList.length - 1); cutsat

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