no goals
α : Type u_1
β : Type ?u.14880
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ map Embedding.some (↑eraseNone s) = erase s none
rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]