Commit 2025-03-31 14:24 e37a0ffd
View on Github →chore(Set): strengthen encard_lt_encard (#23102)
and make Finite.eq_of_subset_of_encard_le be more immediately general than Finite.eq_of_subset_of_encard_le' rather than the other way around to ensure people don't accidentally write undergeneralised proofs using it.
From my PhD (MiscYD)