Commit 2026-02-01 18:45 dd7678a9

View on Github →

refactor: remove order instances from SetLike (#32984)

Estimated changes

modified theorem SubgroupClass.coe_inclusion
modified theorem SubgroupClass.inclusion_mk
modified theorem SubgroupClass.subset_union
added def LE.ofSetLike
modified theorem SetLike.coe_ssubset_coe
modified theorem SetLike.coe_subset_coe
modified theorem SetLike.exists_of_lt
modified theorem SetLike.le_def
modified theorem SetLike.mem_of_subsingleton
modified theorem SetLike.not_le_iff_exists