no goals
R✝ : Type ?u.383760
M : Type ?u.383763
R : Type u_1
inst✝¹ : CommMonoid M
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ ij in Nat.antidiagonal (n + 1), ↑(Nat.choose (n + 1) ij.fst) * f ij.fst ij.snd =
    ∑ ij in Nat.antidiagonal n, ↑(Nat.choose n ij.fst) * f ij.fst (ij.snd + 1) +
      ∑ ij in Nat.antidiagonal n, ↑(Nat.choose n ij.snd) * f (ij.fst + 1) ij.snd
simpa only [nsmul_eq_mul] using sum_antidiagonal_choose_succ_nsmul f n