mathlib3

8d90fcdb - feat(data/finset/basic): Add `coe_pair` lemmas (#16235)

feat(data/finset/basic): Add `coe_pair` lemmas (#16235) Adds `coe_pair` lemmas to go with `coe_singleton` and `coe_eq_singleton` (and fixes a couple of style issues).