mathlib3

f3586f28 - feat(data/fintype/basic): add missing bounded_order instance for finset (#17370)