∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {p : α → Prop} [inst : DecidablePred p],
  Finset.map f.toEmbedding (Finset.filter p s) = Finset.filter (p ∘ ⇑f.symm) (Finset.map f.toEmbedding s)