mathlib

4d26028e - chore(order/basic): add a lemma expanding `le` on pi types (#6023)