cases h with
| head =>
  exact Exists.intro x (And.intro (List.Mem.head _) rfl)
| tail x h' =>
  have ih_val := ih.mp h'
  cases ih_val with | intro a ha =>
  exact Exists.intro a (And.intro (Mem.tail _ ha.left) ha.right)
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h : b ∈ map f (x :: xs)
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
no goals