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. 





leanprover-community/mathlib,leanprover-community/mathlib