Theorem: mem_map_of_mem (Talk/10Aesop.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
a : α
l : List α
h : a ∈ l
⊢ f a ∈ List.map f l
Tactic:
aesop
State after:
no goals