Commit 2024-08-07 06:03 97719f57

chore(Data/Set/Basic): predicate is equal to membership in setOf. (#15554) 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 (@j-loreaux 's first comment) and this example from the Carleson project)