induction xs with
| nil => exact Or.intro_right _ hb
| cons z xs ih =>
  cases hb with
  | head _ => apply Or.intro_left _ (List.Mem.head _)
  | tail _ h' =>
    cases ys with
    | nil =>
      apply Or.intro_left
      apply List.Mem.tail
      simp at h'
      exact h'
    | cons y ys =>
      simp at h'
      cases ih h' with
      | inl hxxs =>
        apply Or.intro_left
        exact List.Mem.tail _ hxxs
      | inr hxys =>
        exact Or.intro_right _ hxys
case mpr
α : Type u_1
x : α
xs ys : List α
hb : x ∈ xs ++ ys
⊢ x ∈ xs ∨ x ∈ ys
no goals