English
If xs is a sublist of ys (xs <+ ys), then xs.sym n is a sublist of ys.sym n.
Русский
Если xs является подсписком ys (xs <+ ys), то xs.sym n является подсписком ys.sym n.
LaTeX
$$$ xs \Subseteq ys \Rightarrow (xs.sym n) \Subseteq (ys.sym n) $$$
Lean4
protected theorem sym (n : ℕ) {xs ys : List α} (h : xs <+ ys) : xs.sym n <+ ys.sym n :=
match n, h with
| 0, _ => by simp [List.sym]
| n + 1, .slnil => by simp only [refl]
| n + 1, .cons a h => by
rw [List.sym, ← nil_append (List.sym (n + 1) xs)]
apply Sublist.append (nil_sublist _)
exact h.sym (n + 1)
| n + 1, .cons₂ a h => by
rw [List.sym, List.sym]
apply Sublist.append
· exact ((cons₂ a h).sym n).map _
· exact h.sym (n + 1)
