card of `finsuppAntidiag`

Stream: new members

[Ralf Stephan]

Intuitively the second example describes the same thing as the first, but how to get there from finsuppAntidiag? It is not used much so there is no code to learn from, and unfolding it successively does not open a path to a lemma that has something about cardinality. Can you please give a hint, how to approach the proof?

import Mathlib

set_option autoImplicit false
open Finset
variable (n : ℕ)

example : (antidiagonal n).card = n + 1 := Nat.card_antidiagonal n

example : ((range 2).finsuppAntidiag n).card = n + 1 := by
    unfold finsuppAntidiag
    unfold piAntidiag
    unfold finAntidiagonal
    sorry