mathlib

d8d6e18c - feat(data/finset/basic): equivalence of finsets from equivalence of types (#4560)

feat(data/finset/basic): equivalence of finsets from equivalence of types (#4560) Broken off from #4259. Given an equivalence `α` to `β`, produce an equivalence between `finset α` and `finset β`, and simp lemmas about it.