rw [ha.right]
case mpr.intro.head
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
ha : x ∈ x :: xs ∧ f x = b
⊢ b ∈ f x :: map f xs
case mpr.intro.head
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
ha : x ∈ x :: xs ∧ f x = b
⊢ b ∈ b :: map f xs