mathlib

258686f9 - fix(order/complete_lattice): fix diamond in sup vs max and min vs inf (#11309)

fix(order/complete_lattice): fix diamond in sup vs max and min vs inf (#11309) `complete_linear_order` has separate `max` and `sup` fields. There is no need to have both, so this removes one of them by telling the structure compiler to merge the two fields. The same is true of `inf` and `min`. As well as diamonds being possible in the abstract case, a handful of concrete example of this diamond existed. `linear_order` instances with default-populated fields were usually to blame.