Theorem: mem_map (Talk/10Aesop.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
b : β
l : List α
⊢ b ∈ List.map f l ↔ ∃ a, a ∈ l ∧ f a = b
Tactic:
induction l <;> aesop
State after:
no goals