. intro hf
  cases hf with
  | head => apply Or.intro_left _ (Mem.head _)
  | tail _ h => apply Or.intro_right _ h
case mp
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ y :: ys → x ∈ [y] ∨ x ∈ ys

case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys
case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys