Commit 2025-09-09 11:19 2237732b
View on Github →chore(Data/Set): golf a lemma that is a duplicate (#29452)
The Subtype API is still full of coe vs val duplication.
This serves simply to record yet another pair, rather than to try and solve this problem.
Note that Subtype.image_val_subset is in a different namespace and has different argument explicitness.