no goals
α : Type u_1
β : Type u_2
γ : Type ?u.40518
f✝ : α ↪ β
s✝ : Finset α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α ↪ β
a : α
s : Finset α
⊢ map f (insert a s) = insert (↑f a) (map f s)
simp only [insert_eq, map_union, map_singleton]