feat(algebra/pointwise): instances in locale pointwise (#8689)
@rwbarton and @bryangingechen mentioned in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Friday.20afternoon.20puzzle.20--.2037.20.E2.88.88.2037.3F that we should put pointwise instances on sets in a locale.
This PR does that. You now have to write `open_locale pointwise` to get algebraic operations on sets and finsets.
Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
