. intro h
  cases h with | intro a ha =>
  simp only [map]
  cases ha.left with
  | head => rw [ha.right]; constructor
  | tail x h' =>
    have h_in_tail := ih.mpr (Exists.intro a ⟨h', ha.right⟩)
    exact Mem.tail _ h_in_tail
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)
no goals