mathlib

6b936a9d - feat(data/set/basic): simp-normal form for `↥{x | p x}` (#14441)

feat(data/set/basic): simp-normal form for `↥{x | p x}` (#14441) We make `{x // p x}` the simp-normal form for `↥{x | p x}`. We also rewrite some lemmas to use the former instead of the latter.