Commit 2024-02-26 09:39 c8bd1526
View on Github →feat: Add Set.subset_setOf and Set.setOf_subset lemmas (#10812)
Expressions like s ⊆ setOf p often appear unintentionally; these replace them with clean ∀ statements.
These aren't registered as @[simp], not least because doing so breaks a few things in mathlib, and it's not clear one always wants to do these.