mathlib3

117e93f8 - feat(data/set/finite): Align `set.to_finset` and `set.finite.to_finset` (#17959)

feat(data/set/finite): Align `set.to_finset` and `set.finite.to_finset` (#17959) Match lemmas about `set.to_finset` and `set.finite.to_finset`. This mostly involves making sure we have all pairs of the form `set.to_finset_whatever`/`set.finite.to_finset_whatever`. Also add a few lemmas and tag existing ones with simp.