Commit 2024-10-04 14:05 674ce265

feat(Data/Multiset/Basic): add lemma on Multiset (#17273) It used to have a following lemma:

s.Disjoint t → s ≤ u → t ≤ u → s + t ≤ u

Now it only has the lemma:

a ∉ s → a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t