chore(Data/Set/Basic): predicate is equal to membership in setOf. (#1…

…5554)

We add a lemma stating that for `p : α -> Prop` we have `p = (· ∈ {a | p a})`. This lemma fills a gap that came up a couple of times when adapting `minimals` to the new `Minimal`, the alternative being an awkward `show`/`change` or `funext`. 

(See [this example from mathlib](#14721 (review)) (@j-loreaux 's first comment) and [this example](https://github.com/fpvandoorn/carleson/pull/109/files#r1705631209) from the Carleson project)

Mathlib/Data/Set/Basic.lean

@@ -199,6 +199,11 @@ theorem forall_in_swap {p : α → β → Prop} : (∀ a ∈ s, ∀ (b), p a b)
 theorem mem_setOf {a : α} {p : α → Prop} : a ∈ { x | p x } ↔ p a :=
   Iff.rfl
 
+/-- This lemma is intended for use with `rw` where a membership predicate is needed,
+hence the explicit argument and the equality in the reverse direction from normal.
+See also `Set.mem_setOf_eq` for the reverse direction applied to an argument. -/
+theorem eq_mem_setOf (p : α → Prop) : p = (· ∈ {a | p a}) := rfl
+
 /-- If `h : a ∈ {x | p x}` then `h.out : p x`. These are definitionally equal, but this can
 nevertheless be useful for various reasons, e.g. to apply further projection notation or in an
 argument to `simp`. -/