mathlib3

0d842f08 - fix(order/closure): unincorporated reviewer comments from #7446 (#7761)