Commit 2024-02-16 05:21 3660a8f3

refactor: prefer s ∩ . when passing to a subset of s (#10433) This is partial work to make s ∩ . be consistently used for passing to a subset of s. This is sort of an adjoint to (Subtype.val : s -> _) '' ., except for the fact that it does not produce a Set s. The main API changes are to Subtype.image_preimage_val and Subtype.preimage_val_eq_preimage_val_iff in Mathlib.Data.Set.Image. Changes in other modules are all proof fixups. Zulip discussion