pullSub_subAt — Mathlib

English

For any tree T and list x, the pullSub of subAt T x by x is bounded above by T: pullSub (subAt T x) x ≤ T.

Русский

Для любого дерева T и списка x, pullSub (subAt T x) x ≤ T.

LaTeX

$$$ pullSub (subAt T x) x \le T $$$

Lean4

theorem pullSub_subAt : pullSub (subAt T x) x ≤ T :=
  by
  intro y (h : y ∈ pullSub _ x); rcases le_total y.length x.length with h' | h'
  · rw [mem_pullSub_short h'] at h; exact mem_of_prefix h.1 (by simpa using h.2)
  · rw [mem_pullSub_long h'] at h; obtain ⟨_, h, rfl⟩ := h; exact h

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