∀ (n : ℕ),
  Finset.antidiagonal (n + 1) =
    Finset.cons (n + 1, 0)
      (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
        (Finset.antidiagonal n))
      ⋯