Commit 2025-10-25 16:12 9c935d6d
View on Github →chore(Data/Fintype/Sets): deprecate duplicate toFinset_subset_toFinset_of_subset (#30884)
I accidentally added the duplicate toFinset_subset_toFinset_of_subset of toFinset_mono when working on grw. So this PR deprecates it.