English
For any n, xs, a and z ∈ Sym α n, if a ∈ z and z ∈ xs.sym n, then a ∈ xs.
Русский
Пусть n, xs, a и z ∈ Sym α n. Если a ∈ z и z ∈ xs.sym n, то a ∈ xs.
LaTeX
$$$ a \in z \land z \in xs.sym n \Rightarrow a \in xs $$$
Lean4
theorem mem_of_mem_of_mem_sym {n : ℕ} {xs : List α} {a : α} {z : Sym α n} (ha : a ∈ z) (hz : z ∈ xs.sym n) : a ∈ xs :=
match n, xs with
| 0, xs => by
cases Sym.eq_nil_of_card_zero z
simp at ha
| n + 1, [] => by simp [List.sym] at hz
| n + 1, x :: xs => by
rw [List.sym, mem_append, mem_map] at hz
obtain ⟨z, hz, rfl⟩ | hz := hz
· rw [Sym.mem_cons] at ha
obtain rfl | ha := ha
· simp
· exact mem_of_mem_of_mem_sym ha hz
· rw [mem_cons]
right
exact mem_of_mem_of_mem_sym ha hz
