English
For any s,t, s is in tails t iff s is a suffix of t.
Русский
Для любых s,t, s входит в tails t тогда и только тогда, когда s является суффиксом t.
LaTeX
$$$\forall s,t : \text{List}(\alpha),\; s \in t.tails \iff s \text{ is a suffix of } t.$$$
Lean4
@[simp]
theorem mem_tails : ∀ s t : List α, s ∈ tails t ↔ s <:+ t
| s, [] => by simp only [tails, mem_singleton, suffix_nil]
| s, a :: t => by
simp only [tails, mem_cons, mem_tails s t]
exact
show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
⟨fun o =>
match s, t, o with
| _, t, Or.inl rfl => suffix_rfl
| s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
fun e =>
match s, t, e with
| _, t, ⟨[], rfl⟩ => Or.inl rfl
| s, t, ⟨b :: l, he⟩ => List.noConfusion he fun _ lt => Or.inr ⟨l, lt⟩⟩
