prefix_append_drop — Mathlib

English

If l1 is a prefix of l2, then l2 = l1 ++ l2.drop l1.length.

Русский

Если l1 является префиксом l2, то l2 = l1 ++ l2.drop l1.length.

LaTeX

$$$\forall {\alpha} {l_1 l_2 : \text{List}(\alpha)}\; (l_1 \text{ IsPrefix } l_2) \Rightarrow l_2 = l_1 ++ l_2.drop l_1.length.$$$

Lean4

theorem prefix_append_drop {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₂ = l₁ ++ l₂.drop l₁.length := by
  induction l₂ generalizing l₁ with
  | nil => simp [List.prefix_nil.mp h]
  | cons _ _ ih =>
    cases l₁ with
    | nil => rfl
    | cons =>
      obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'

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