Commit 2024-02-12 10:30 4841d69d

fix(Data/Set/Image): simp confluence issues with image_subset_iff (#8683) image_subset_iff is a questionable simp lemma because it converts an application of Set.image into an application of Set.preimage unconditionally. This means that if any simp lemma applies to images, there must be a corresponding lemma for preimages. These lemmas are what I found missing after loogling. I also added machine-checked examples of each confluence issue to a new file tests/simp_confluence.