no goals
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ m in Nat.antidiagonal n, Nat.choose n m.fst • (x ^ m.fst * y ^ m.snd)
simp_rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ choose n m • (x ^ m * y ^ p),
  _root_.nsmul_eq_mul, cast_comm, h.add_pow]