exact Exists.intro x (And.intro (List.Mem.head _) rfl)
case mp.head
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : f x ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = f x
⊢ ∃ a, a ∈ x :: xs ∧ f a = f x
no goals