mathlib3

8e275a30 - fix(order/complete_lattice): fix typo in docstring (#6925)