mathlib3

32700f50 - refactor(*): `insert_singleton` → `pair` (#14210)

refactor(*): `insert_singleton` → `pair` (#14210) We rename various theorems with `insert_singleton` in the name to the more sensible and searchable `pair`. We also golf `finset.pair_comm`.