mathlib3

feat(*): some simple lemmas about sets and finite sets

#1903

Merged