mathlib

df3792f8 - refactor(data/set): generalize `set.restrict` and take set argument first in both `set.restrict` and `subtype.restrict` (#12510)

refactor(data/set): generalize `set.restrict` and take set argument first in both `set.restrict` and `subtype.restrict` (#12510) Generalizes `set.restrict` to Pi types and makes both this function and `subtype.restrict` take the restricting index set before the Pi type to restrict, which makes taking the image/preimage of a set of Pi types easier (`s.restrict '' pis` is shorter than `(λ p, set.restrict p s) '' pis` -- I'd argue that this is the more common case than taking the image of a set of restricting sets on a single Pi type). Changed uses of `set.restrict` to use dot notation where possible.