doc: Example use case of Finset.filter (#9239)

Mention the spelling `s.filter (· ∈ t)` for the intersection of `s : Finset α` and `t : Set α` as a `Finset α` in the docstring of `Finset.filter`.

See [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Intersection.20of.20a.20Finset.20and.20a.20Set.20as.20a.20Finset.3F/near/409632763) on Zulip.



Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

Mathlib/Data/Finset/Basic.lean

@@ -2710,7 +2710,10 @@ section Filter
 
 variable (p q : α → Prop) [DecidablePred p] [DecidablePred q] {s : Finset α}
 
-/-- `Finset.filter p s` is the set of elements of `s` that satisfy `p`. -/
+/-- `Finset.filter p s` is the set of elements of `s` that satisfy `p`.
+
+For example, one can use `s.filter (· ∈ t)` to get the intersection of `s` with `t : Set α`
+as a `Finset α` (when a `DecidablePred (· ∈ t)` instance is available). -/
 def filter (s : Finset α) : Finset α :=
   ⟨_, s.2.filter p⟩
 #align finset.filter Finset.filter