no goals
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ b ∈ map f [] ↔ ∃ a, a ∈ [] ∧ f a = b
simp
no goals
α : Type u_1
β : Type u_2
b : β
f : α → β
head✝ : α
l : List α
⊢ b ∈ map f (head✝ :: l) ↔ ∃ a, a ∈ head✝ :: l ∧ f a = b
simp [mem_map (l := l), eq_comm (a := b)]