mathlib3

ff970553 - feat(data/finset/basic): insert_singleton_comm (#3914)

feat(data/finset/basic): insert_singleton_comm (#3914) Add the result that `({a, b} : finset α) = {b, a}`. This came up in #3872, and `library_search` does not show it as already present.