feat: `Small.{u}` sets are closed under various operations

[timotree3]

trafficstars

This PR adds lemmas showing that sets constructed by applying basic set operations to small sets are themselves small. We now have corresponding Small ↥s versions of almost all of the Finite ↥s instances in the Finite.Set namespace.

---

[timotree3]

!bench

[leanprover-bot]

Here are the benchmark results for commit e2773f52e2940720618099b07f1969c56a3e4430. There were significant changes against commit 5112b8d86cb2216cc2be2132da26ac33267b8f8c:

  Benchmark                                           Metric         Change
  =========================================================================
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Affine   instructions   -16.3%