English
If x ∈ xs, then mapping y ↦ s(x,y) over xs is a sublist of xs.sym2, i.e., (map (λ y, s(x,y)) xs) ⊂ xs.sym2.
Русский
Если x ∈ xs, то отображение y ↦ s(x,y) по xs является подпоследовательностью xs.sym2.
LaTeX
$$$$ \\text{If } x \\in xs, \\ (\\mathrm{map}(\\lambda y.\\mathrm{s}(x,y))\\; xs) \\;<+\\! xs.sym2 $$$$
Lean4
theorem map_mk_sublist_sym2 (x : α) (xs : List α) (h : x ∈ xs) : map (fun y ↦ s(x, y)) xs <+ xs.sym2 := by
induction xs with
| nil => simp
| cons x' xs ih =>
simp only [map_cons, List.sym2, cons_append]
cases h with
| head => exact (sublist_append_left _ _).cons₂ _
| tail _ h =>
refine .cons _ ?_
rw [← singleton_append]
refine .append ?_ (ih h)
rw [singleton_sublist, mem_map]
exact ⟨_, h, Sym2.eq_swap⟩
