left_mem_of_mk_mem_sym2 — Mathlib

English

If s(a,b) appears in xs.sym2, then a belongs to xs.

Русский

Если s(a,b) встречается в xs.sym2, то a ∈ xs.

LaTeX

$$$$ s(a,b) \\in xs.sym2 \\Rightarrow a \\in xs $$$$

Lean4

theorem left_mem_of_mk_mem_sym2 {xs : List α} {a b : α} (h : s(a, b) ∈ xs.sym2) : a ∈ xs := by
  induction xs with
  | nil => exact (not_mem_nil h).elim
  | cons x xs ih =>
    rw [mem_cons]
    rw [mem_sym2_cons_iff] at h
    obtain (h | ⟨c, hc, h⟩ | h) := h
    · rw [Sym2.eq_iff, ← and_or_left] at h
      exact .inl h.1
    · rw [Sym2.eq_iff] at h
      obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h <;> simp [hc]
    · exact .inr <| ih h

Похожие утверждения