mathlib3

3a16e9f8 - feat(data/set/finite): add to_finset lemma (#5883)

feat(data/set/finite): add to_finset lemma (#5883) Add lemma stating that taking to_finset of the union of two sets is the same as taking the union of to_finset of the sets.