no goals
α : Type u_1
β : Type u_2
γ : Type ?u.30514
f✝ : α ↪ β
s : Finset α
f : α ≃ β
p : α → Prop
inst✝ : DecidablePred p
⊢ map (Equiv.toEmbedding f) (filter p s) = filter (p ∘ ↑f.symm) (map (Equiv.toEmbedding f) s)
simp only [filter_map, Function.comp, Equiv.toEmbedding_apply, Equiv.symm_apply_apply]