Commit 2024-11-08 09:53 57f9c20e
View on Github →feat: add simp annotation to Subtype.val_injective (#18457)
My original motivation was to make Set.preimage_image_eq _ Subtype.val_injective available to the simplifier, and this seemed like the best way to achieve this.