mathlib

887f9338 - feat(data/fin/tuple/nat_antidiagonal): add an equiv and some TODO comments. (#13338)

feat(data/fin/tuple/nat_antidiagonal): add an equiv and some TODO comments. (#13338) This follows on from #13031, and: * Adds the tuple version of an antidiagonal equiv * Makes some arguments implicit * Adds some comments to tie together `finset.nat.antidiagonal_tuple` with the `cut` definition used in one of the 100 Freek problems.