English
For any s and t, s is inits of t iff s is a prefix of t.
Русский
Для любых s и t, s является префиксом t эквивалентно тому, что s входит в inits t.
LaTeX
$$$\forall s,t : \text{List}(\alpha),\ s \in t.inits \iff s \text{ is a prefix of } t.$$$
Lean4
@[simp]
theorem mem_inits : ∀ s t : List α, s ∈ inits t ↔ s <+: t
| s, [] =>
suffices s = nil ↔ s <+: nil by simpa only [inits, mem_singleton]
⟨fun h => h.symm ▸ prefix_rfl, eq_nil_of_prefix_nil⟩
| s, a :: t =>
suffices (s = nil ∨ ∃ l ∈ inits t, a :: l = s) ↔ s <+: a :: t by simpa
⟨fun o =>
match s, o with
| _, Or.inl rfl => ⟨_, rfl⟩
| s, Or.inr ⟨r, hr, hs⟩ => by
let ⟨s, ht⟩ := (mem_inits _ _).1 hr
rw [← hs, ← ht]; exact ⟨s, rfl⟩,
fun mi =>
match s, mi with
| [], ⟨_, rfl⟩ => Or.inl rfl
| b :: s, ⟨r, hr⟩ =>
(List.noConfusion hr) fun ba (st : s ++ r = t) =>
Or.inr <| by rw [ba]; exact ⟨_, (mem_inits _ _).2 ⟨_, st⟩, rfl⟩⟩
