English
If xs is permuted to ys, then xs.sym2 is permuted to ys.sym2.
Русский
Если xs переставлена в ys, то xs.sym2 переставлена в ys.sym2.
LaTeX
$$$$ xs ~ ys \\Rightarrow xs.sym2 ~ ys.sym2 $$$$
Lean4
protected theorem sym2 {xs ys : List α} (h : xs ~ ys) : xs.sym2 ~ ys.sym2 := by
induction h with
| nil => rfl
| cons x h ih =>
simp only [List.sym2, map_cons, cons_append, perm_cons]
exact (h.map _).append ih
| swap x y xs =>
simp only [List.sym2, map_cons, cons_append]
conv => enter [1, 2, 1];
rw [Sym2.eq_swap]
-- Explicit permutation to speed up simps that follow.
refine Perm.trans (Perm.swap ..) (Perm.trans (Perm.cons _ ?_) (Perm.swap ..))
simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe, ← Multiset.coe_add, ← Multiset.singleton_add]
simp only [add_left_comm]
| trans _ _ ih1 ih2 => exact ih1.trans ih2
