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.cons.tail
α : Type u_1
x : α
ys : List α
z : α
xs : List α
ih : x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
h' : Mem x (List.append xs ys)
⊢ x ∈ z :: xs ∨ x ∈ ys
no goals