Commit 2026-07-06 15:50 9ef14c7b

feat: use LE.le for subset relation in Set, Finset, PSet, ZFSet, Class (#32983) This PR uses @[use_set_notation_for_order] in Set, Finset, PSet, ZFSet and Class. So, for these types, we will write ⊆, while the underlying constant is LE.le. Some notes:

• The idea is to later extend this feature to other set notation constants, such as union/intersection.
• Dot notation on the HasSubset.Subset namespace now doesn't work anymore, and the names need to be put in the LE.le namespace instead.
• Various simp and gcongr tags needed to be removed/updated as a result of this change. See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629