Commit 2026-05-12 10:45 7fb9d46b

feat: implementation of @[use_set_notation_for_order] (#37347) This PR allows the use of ⊆ notation while the underlying constant is ≤. Similarly for ⊂/<, ⊇/≥ and ⊃/>.

• The idea is to later extend this feature to other set notation constants, such as union/intersection.
• There are some types for which we cannot use LE.le as the underlying constant, such as List and Multiset. So, the elaborator for the ⊆ notation needs to make a decision which underlying constant to elaborate to, depending on the type. Sometimes the type is not known yet, which makes things awkward. Most of these cases are solved by delaying the elaboration until later when the type is known.
• However, in some cases this doesn't work either, such as simp_rw [and_comm (_ ⊆ _)], where it is impossible to tell the type when elaborating the term. So, some such cases need to be fixed by making it simp_rw [and_comm ((_ : Set _) ⊆ _)]. This is because simp_rw, unlike rw, fully elaborates the rewrite rules before using them. A linter warns you whever there is such an ambiguity. See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629