pullSub_append — Mathlib

English

pullSub (pullSub T y) x = pullSub T (x ++ y).

Русский

pullSub (pullSub T y) x = pullSub T (x ++ y).

LaTeX

$$$ pullSub (pullSub T y) x = pullSub T (x ++ y) $$$

Lean4

@[simp]
theorem pullSub_append : pullSub (pullSub T y) x = pullSub T (x ++ y) :=
  by
  ext z; rcases le_total x.length z.length with hl | hl
  · by_cases hp : x <+: z
    · obtain ⟨z, rfl⟩ := hp
      simp [pullSub, List.take_add]
    ·
      constructor <;> intro ⟨h, _⟩ <;> [skip; replace h := by simpa [List.take_take] using h.take x.length] <;>
        cases hp <| List.prefix_iff_eq_take.mpr (h.eq_of_length (by simpa)).symm
  · rw [mem_pullSub_short hl, mem_pullSub_short (by simp), mem_pullSub_short (by simp; cutsat)]
    simpa using fun _ ↦ (z.isPrefix_append_of_length hl).symm

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