mathlib

664247fc - chore(data/set/intervals/ord_connected): Golf proof (#12923)