mathlib3

24e75f1e - chore(order/filter/basic): protect 3 lemmas (#18331)