mathlib3

474656fd - chore(algebra/order/lattice_group): Golf (#18046)

chore(algebra/order/lattice_group): Golf (#18046) Golf proofs and remove a duplicate lemma. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>