mem_of_mem_tail — Mathlib

English

If a belongs to drop s n, then a belongs to s.

Русский

Если a ∈ drop s n, то a ∈ s.

LaTeX

$$$$\forall s:\\mathrm{WSeq}\,\alpha,\forall a:\\alpha,\forall n:\\mathbb{N},\ a \in \mathrm{drop}\,s\,n \Rightarrow a \in s.$$$$

Lean4

theorem mem_of_mem_tail {s : WSeq α} {a} : a ∈ tail s → a ∈ s :=
  by
  intro h; have := h; obtain ⟨n, e⟩ := h; revert s; simp only [Stream'.get]
  induction n <;> intro s <;> induction s using WSeq.recOn <;> simp <;> intro m e <;> injections
  · exact Or.inr m
  · exact Or.inr m
  case succ.think n IH s =>
    apply IH m
    rw [e]
    cases tail s
    rfl

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