feat: More ways of bijecting finsets

[YaelDillies]

trafficstars

It is still annoyingly painful to prove that two finsets have equal size by exhibiting a bijection between. This PR remedies this problem by copying over the lemmas that show that two finite sums/products are in bijection. Copy over the names. As a result, rename Finset.card_congr to Finset.card_bij.

---