mathlib

37212a78 - feat(data/fin*): uniqueness of increasing bijection (#2258)

feat(data/fin*): uniqueness of increasing bijection (#2258) * feat(data/fin*): uniqueness of increasing bijection * protect * remove tidy call * Update src/data/finset.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/finset.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * prove prod_add, and use this to prove sum_pow_mul_eq_add_pow * forgot to save * fix build * remove card_sub_card Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>