mathlib

0b1c333f - Proved `sup_eq_lsub_iff_lt_sup`