-- Mathlib/Data/Nat/Choose/Sum.lean
theorem add_pow (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * n.choose m

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
n : ℕ
⊢ t n 0 = y ^ n

Tactic:
simp only [t, choose_zero_right, pow_zero, cast_one, mul_one, one_mul, tsub_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), t n m

Tactic:
induction n with
| zero =>
  rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
  dsimp only [t]
  rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
| succ n ih =>
  rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc,
    pow_succ' (x + y), ih, add_mul, mul_sum, mul_sum]
  congr 1
  rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
n : ℕ
⊢ t n n.succ = 0

Tactic:
simp only [t, choose_succ_self, cast_zero, mul_zero]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = x ^ 0 * y ^ (0 - 0) * ↑(Nat.choose 0 0)

Tactic:
rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) ^ (n + 1) = ∑ m ∈ range (n + 1 + 1), t (n + 1) m

Tactic:
rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc,
  pow_succ' (x + y), ih, add_mul, mul_sum, mul_sum]

Result:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ i ∈ range (n + 1), x * t n i + ∑ i ∈ range (n + 1), y * t n i =
    ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
change (x + y) ^ n = ∑ m ∈ range (n + 1), t n m

Result:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), t n m

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ (x + y) ^ 0 = ∑ m ∈ range (0 + 1), t 0 m

Tactic:
rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]

Result:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = t 0 0

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = t 0 0

Tactic:
dsimp only [t]

Result:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = x ^ 0 * y ^ (0 - 0) * ↑(Nat.choose 0 0)

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
let t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * n.choose m

Result:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)

Proof state:
case succ.e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)

Tactic:
rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
⊢ t n.succ i.succ = x * t n i + y * t n i.succ

Tactic:
have h_le : i ≤ n := le_of_lt_succ (mem_range.mp h_mem)

Result:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ t n.succ i.succ = x * t n i + y * t n i.succ

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i) + x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
congr 1

Result:
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))

case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))