English
Same principle as Revzip Sublists but for the variant sublists'.
Русский
Та же идея для варианта подсписков'.
LaTeX
$$$$ \\forall 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 generalizing l₁ l₂ with
| nil =>
simp_all only [sublists'_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons, zip_nil_right, mem_singleton,
Prod.mk.injEq, append_nil, Perm.refl]
| cons a l
IH =>
rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at * <;>
[simp only [mem_append, mem_map, Prod.map_apply, id_eq, Prod.mk.injEq, Prod.exists, exists_eq_right_right] at h;
simp]
rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)
· exact perm_middle.trans ((IH _ _ h).cons _)
· exact (IH _ _ h).cons _
