English
Characterization of membership in zip l.inits l.tails: (init, tail) ∈ zip l.inits l.tails iff init ++ tail = l.
Русский
Характеризация принадлежности пары (init, tail) в zip l.inits l.tails: (init, tail) ∈ zip l.inits l.tails тогда и только если init ++ tail = l.
LaTeX
$$$(init, tail) \in zip l.inits l.tails \iff init ++ tail = l$$$
Lean4
theorem mem_zip_inits_tails {l : List α} {init tail : List α} : (init, tail) ∈ zip l.inits l.tails ↔ init ++ tail = l :=
by
induction l generalizing init tail <;> simp_rw [tails, inits, zip_cons_cons]
case nil => simp
case cons hd tl ih =>
constructor <;> rw [mem_cons, zip_map_left, mem_map, Prod.exists]
· rintro (⟨rfl, rfl⟩ | ⟨_, _, h, rfl, rfl⟩)
· simp
· simp [ih.mp h]
· rcases init with - | ⟨hd', tl'⟩
· simp
· intro h
right
use tl', tail
simp_all
