mathlib

b9492402 - feat(algebra/{lie/subalgebra,module/submodule/pointwise}): submodules and lie subalgebras form canonically ordered additive monoids under addition (#14529)

feat(algebra/{lie/subalgebra,module/submodule/pointwise}): submodules and lie subalgebras form canonically ordered additive monoids under addition (#14529) We can't actually make these instances because they result in loops for `simp`. The `le_iff_exists_sup` lemma is probably not very useful for much beyond these new instances, but it matches `le_iff_exists_add`.