Theorem: List.toFinset_map (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : α → β
l : List α
⊢ (map f l).toFinset = Finset.image f l.toFinset
Tactic:
induction l <;> simp[*]
State after:
no goals