Theorem finset.eq_empty_of_subset_empty

refactor(data/finset): redefine finsets as subtype of multisets

feat(data/finset): add fold; add simp rules for insert, empty, singleton and mem

fix(data/finset): use the type class projections for insert; hide most constants using protected; add image of finset

Merge branch 'master' of https://github.com/leanprover/mathlib

fix(algebra/group): add every transport theorem from main Lean repository

refactor(data/finset): fix formatting issues

feat(topology): add topological structures for groups, ring, and linear orders; add instances for rat and real

feat(data/finset): add basics for finsets