Commit 2023-08-25 14:43 7e9ae5f4
View on Github →chore(Data/Finset/NatAntidiagonal): naming of antidiagonalEquivFin (#6784)
and add simps, as pointed out by @eric-wieser in
https://github.com/leanprover-community/mathlib4/pull/6766#pullrequestreview-1595354618