English
If two lists l1 and l2 appear as a pair in the reverse zip of the sublists of l, then l1 concatenated with l2 is a permutation of l.
Русский
Если пара списков (l1, l2) встречается в revzip левого подсписочного списка l, то l1 ++ l2 является перестановкой l.
LaTeX
$$$$ \\text{For all } l,l_1,l_2:\\ (l_1,l_2) \\in \\mathrm{revzip}\\,l.\\mathrm{sublists} \\Rightarrow l_1 \\;\\mathrel{\\sim}\\; l $$$$
Lean4
theorem revzip_sublists (l l₁ l₂ : List α) (h : (l₁, l₂) ∈ revzip l.sublists) : l₁ ++ l₂ ~ l :=
by
rw [revzip] at h
induction l using List.reverseRecOn generalizing l₁ l₂ with
| nil =>
have : l₁ = [] ∧ l₂ = [] := by simpa using h
simp [this]
| append_singleton l' a
ih =>
rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right, zip_map_left] at *
simp only [Prod.mk_inj, mem_map, mem_append, Prod.map_apply, Prod.exists] at h
rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)
· rw [← append_assoc]
exact (ih _ _ h).append_right _
· rw [append_assoc]
apply (perm_append_comm.append_left _).trans
rw [← append_assoc]
exact (ih _ _ h).append_right _
