[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
[PROOFSTEP]
let t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * choose n m
[GOAL]
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) * ↑(Nat.choose n m)
⊢ (x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
[PROOFSTEP]
change (x + y) ^ n = ∑ m in range (n + 1), t n m
[GOAL]
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) * ↑(Nat.choose n m)
⊢ (x + y) ^ n = ∑ m in range (n + 1), t n m
[PROOFSTEP]
have h_first : ∀ n, t n 0 = y ^ n := fun n ↦ by
  simp only [choose_zero_right, _root_.pow_zero, Nat.cast_one, mul_one, one_mul, tsub_zero]
[GOAL]
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) * ↑(Nat.choose n m)
n : ℕ
⊢ t n 0 = y ^ n
[PROOFSTEP]
simp only [choose_zero_right, _root_.pow_zero, Nat.cast_one, mul_one, one_mul, tsub_zero]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
⊢ (x + y) ^ n = ∑ m in range (n + 1), t n m
[PROOFSTEP]
have h_last : ∀ n, t n n.succ = 0 := fun n ↦ by simp only [ge_iff_le, choose_succ_self, cast_zero, mul_zero]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
n : ℕ
⊢ t n (succ n) = 0
[PROOFSTEP]
simp only [ge_iff_le, choose_succ_self, cast_zero, mul_zero]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
⊢ (x + y) ^ n = ∑ m in range (n + 1), t n m
[PROOFSTEP]
have h_middle : ∀ n i : ℕ, i ∈ range n.succ → (t n.succ ∘ Nat.succ) i = x * t n i + y * t n i.succ :=
  by
  intro n i h_mem
  have h_le : i ≤ n := Nat.le_of_lt_succ (mem_range.mp h_mem)
  dsimp only
  rw [Function.comp_apply, choose_succ_succ, Nat.cast_add, mul_add]
  congr 1
  · rw [pow_succ x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
  · rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
    by_cases h_eq : i = n
    · rw [h_eq, choose_succ_self, Nat.cast_zero, mul_zero, mul_zero]
    · rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
      rw [pow_succ y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
⊢ ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
[PROOFSTEP]
intro n i h_mem
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
⊢ (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
[PROOFSTEP]
have h_le : i ≤ n := Nat.le_of_lt_succ (mem_range.mp h_mem)
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
[PROOFSTEP]
dsimp only
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ ((fun m => x ^ m * y ^ (succ n - m) * ↑(Nat.choose (succ n) m)) ∘ succ) i =
    x * (x ^ i * y ^ (n - i) * ↑(Nat.choose n i)) + y * (x ^ succ i * y ^ (n - succ i) * ↑(Nat.choose n (succ i)))
[PROOFSTEP]
rw [Function.comp_apply, choose_succ_succ, Nat.cast_add, mul_add]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n i) +
      x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n (succ i)) =
    x * (x ^ i * y ^ (n - i) * ↑(Nat.choose n i)) + y * (x ^ succ i * y ^ (n - succ i) * ↑(Nat.choose n (succ i)))
[PROOFSTEP]
congr 1
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n i) = x * (x ^ i * y ^ (n - i) * ↑(Nat.choose n i))
[PROOFSTEP]
rw [pow_succ x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n (succ i)) =
    y * (x ^ succ i * y ^ (n - succ i) * ↑(Nat.choose n (succ i)))
[PROOFSTEP]
rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n (succ i)) =
    x ^ succ i * y * y ^ (n - succ i) * ↑(Nat.choose n (succ i))
[PROOFSTEP]
by_cases h_eq : i = n
[GOAL]
case pos
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
h_eq : i = n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n (succ i)) =
    x ^ succ i * y * y ^ (n - succ i) * ↑(Nat.choose n (succ i))
[PROOFSTEP]
rw [h_eq, choose_succ_self, Nat.cast_zero, mul_zero, mul_zero]
[GOAL]
case neg
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n (succ i)) =
    x ^ succ i * y * y ^ (n - succ i) * ↑(Nat.choose n (succ i))
[PROOFSTEP]
rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
[GOAL]
case neg
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ succ i * y ^ succ (n - succ i) * ↑(Nat.choose n (succ i)) =
    x ^ succ i * y * y ^ (n - succ i) * ↑(Nat.choose n (succ i))
[PROOFSTEP]
rw [pow_succ y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
⊢ (x + y) ^ n = ∑ m in range (n + 1), t n m
[PROOFSTEP]
induction' n with n ih
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
⊢ (x + y) ^ zero = ∑ m in range (zero + 1), t zero m
[PROOFSTEP]
rw [_root_.pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
⊢ 1 = t zero zero
[PROOFSTEP]
dsimp only
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
⊢ 1 = x ^ zero * y ^ (zero - zero) * ↑(Nat.choose zero zero)
[PROOFSTEP]
rw [_root_.pow_zero, _root_.pow_zero, choose_self, Nat.cast_one, mul_one, mul_one]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
n : ℕ
ih : (x + y) ^ n = ∑ m in range (n + 1), t n m
⊢ (x + y) ^ succ n = ∑ m in range (succ n + 1), t (succ n) m
[PROOFSTEP]
rw [sum_range_succ', h_first]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
n : ℕ
ih : (x + y) ^ n = ∑ m in range (n + 1), t n m
⊢ (x + y) ^ succ n = ∑ k in range (n + 1), t (succ n) (k + 1) + y ^ succ n
[PROOFSTEP]
erw [sum_congr rfl (h_middle n), sum_add_distrib, add_assoc]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
n : ℕ
ih : (x + y) ^ n = ∑ m in range (n + 1), t n m
⊢ (x + y) ^ succ n = ∑ x_1 in range (succ n), x * t n x_1 + (∑ x in range (succ n), y * t n (succ x) + y ^ succ n)
[PROOFSTEP]
rw [pow_succ (x + y), ih, add_mul, mul_sum, mul_sum]
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
n : ℕ
ih : (x + y) ^ n = ∑ m in range (n + 1), t n m
⊢ ∑ x_1 in range (n + 1), x * t n x_1 + ∑ x in range (n + 1), y * t n x =
    ∑ x_1 in range (succ n), x * t n x_1 + (∑ x in range (succ n), y * t n (succ x) + y ^ succ n)
[PROOFSTEP]
congr 1
[GOAL]
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) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
n : ℕ
ih : (x + y) ^ n = ∑ m in range (n + 1), t n m
⊢ ∑ x in range (n + 1), y * t n x = ∑ x in range (succ n), y * t n (succ x) + y ^ succ n
[PROOFSTEP]
rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ]
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (n + 1), choose n m = 2 ^ n
[PROOFSTEP]
have := (add_pow 1 1 n).symm
[GOAL]
R : Type u_1
n : ℕ
this : ∑ m in range (n + 1), 1 ^ m * 1 ^ (n - m) * ↑(choose n m) = (1 + 1) ^ n
⊢ ∑ m in range (n + 1), choose n m = 2 ^ n
[PROOFSTEP]
simpa [one_add_one_eq_two] using this
[GOAL]
R : Type u_1
m i : ℕ
hi : i ∈ range (m + 1)
⊢ i ≤ 2 * m + 1
[PROOFSTEP]
linarith [mem_range.1 hi]
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * ∑ i in range (m + 1), choose (2 * m + 1) i =
    ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i)
[PROOFSTEP]
rw [two_mul, this]
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) =
    ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in Ico (m + 1) (2 * m + 2), choose (2 * m + 1) i
[PROOFSTEP]
{ rw [range_eq_Ico, sum_Ico_reflect]
  · congr
    have A : m + 1 ≤ 2 * m + 1 := by linarith
    rw [add_comm, add_tsub_assoc_of_le A, ← add_comm]
    congr
    rw [tsub_eq_iff_eq_add_of_le A]
    ring
  · linarith
}
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) =
    ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in Ico (m + 1) (2 * m + 2), choose (2 * m + 1) i
[PROOFSTEP]
rw [range_eq_Ico, sum_Ico_reflect]
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ ∑ i in Ico 0 (m + 1), choose (2 * m + 1) i +
      ∑ j in Ico (2 * m + 1 + 1 - (m + 1)) (2 * m + 1 + 1 - 0), choose (2 * m + 1) j =
    ∑ i in Ico 0 (m + 1), choose (2 * m + 1) i + ∑ i in Ico (m + 1) (2 * m + 2), choose (2 * m + 1) i
[PROOFSTEP]
congr
[GOAL]
case e_a.e_s.e_a
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * m + 1 + 1 - (m + 1) = m + 1
[PROOFSTEP]
have A : m + 1 ≤ 2 * m + 1 := by linarith
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ m + 1 ≤ 2 * m + 1
[PROOFSTEP]
linarith
[GOAL]
case e_a.e_s.e_a
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 + 1 - (m + 1) = m + 1
[PROOFSTEP]
rw [add_comm, add_tsub_assoc_of_le A, ← add_comm]
[GOAL]
case e_a.e_s.e_a
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 - (m + 1) + 1 = m + 1
[PROOFSTEP]
congr
[GOAL]
case e_a.e_s.e_a.e_a
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 - (m + 1) = m
[PROOFSTEP]
rw [tsub_eq_iff_eq_add_of_le A]
[GOAL]
case e_a.e_s.e_a.e_a
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 = m + (m + 1)
[PROOFSTEP]
ring
[GOAL]
case h
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ m + 1 ≤ 2 * m + 1 + 1
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ m + 1 ≤ 2 * m + 2
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 ^ (2 * m + 1) = 2 * 4 ^ m
[PROOFSTEP]
rw [pow_succ, pow_mul, mul_comm]
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * (2 ^ 2) ^ m = 2 * 4 ^ m
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
n : ℕ
⊢ choose (2 * n + 1) n ≤ 4 ^ n
[PROOFSTEP]
have t : choose (2 * n + 1) n ≤ ∑ i in range (n + 1), choose (2 * n + 1) i :=
  single_le_sum (fun x _ ↦ by linarith) (self_mem_range_succ n)
[GOAL]
R : Type u_1
n x : ℕ
x✝ : x ∈ range (n + 1)
⊢ 0 ≤ choose (2 * n + 1) x
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
n : ℕ
t : choose (2 * n + 1) n ≤ ∑ i in range (n + 1), choose (2 * n + 1) i
⊢ choose (2 * n + 1) n ≤ 4 ^ n
[PROOFSTEP]
simpa [sum_range_choose_halfway n] using t
[GOAL]
R : Type u_1
n : ℕ
⊢ 4 ^ n = (1 + 1) ^ (2 * n)
[PROOFSTEP]
simp only [pow_mul, one_add_one_eq_two]
[GOAL]
R : Type u_1
n : ℕ
⊢ 4 ^ n = (2 ^ 2) ^ n
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
n : ℕ
⊢ (1 + 1) ^ (2 * n) = ∑ m in range (2 * n + 1), choose (2 * n) m
[PROOFSTEP]
simp [add_pow]
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (2 * n + 1), choose (2 * n) m ≤ ∑ m in range (2 * n + 1), choose (2 * n) (2 * n / 2)
[PROOFSTEP]
gcongr
[GOAL]
case h
R : Type u_1
n i✝ : ℕ
a✝ : i✝ ∈ range (2 * n + 1)
⊢ choose (2 * n) i✝ ≤ choose (2 * n) (2 * n / 2)
[PROOFSTEP]
apply choose_le_middle
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (2 * n + 1), choose (2 * n) (2 * n / 2) = (2 * n + 1) * choose (2 * n) n
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (n + 1), (-1) ^ m * ↑(Nat.choose n m) = if n = 0 then 1 else 0
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
⊢ ∑ m in range (zero + 1), (-1) ^ m * ↑(Nat.choose zero m) = if zero = 0 then 1 else 0
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
n✝ : ℕ
⊢ ∑ m in range (Nat.succ n✝ + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n✝) m) = if Nat.succ n✝ = 0 then 1 else 0
[PROOFSTEP]
case succ n =>
  have h := add_pow (-1 : ℤ) 1 n.succ
  simp only [one_pow, mul_one, add_left_neg] at h 
  rw [← h, zero_pow (Nat.succ_pos n), if_neg (Nat.succ_ne_zero n)]
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
[PROOFSTEP]
case succ n =>
  have h := add_pow (-1 : ℤ) 1 n.succ
  simp only [one_pow, mul_one, add_left_neg] at h 
  rw [← h, zero_pow (Nat.succ_pos n), if_neg (Nat.succ_ne_zero n)]
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
[PROOFSTEP]
have h := add_pow (-1 : ℤ) 1 n.succ
[GOAL]
R : Type u_1
n : ℕ
h :
  (-1 + 1) ^ Nat.succ n = ∑ m in range (Nat.succ n + 1), (-1) ^ m * 1 ^ (Nat.succ n - m) * ↑(Nat.choose (Nat.succ n) m)
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
[PROOFSTEP]
simp only [one_pow, mul_one, add_left_neg] at h 
[GOAL]
R : Type u_1
n : ℕ
h : 0 ^ Nat.succ n = ∑ x in range (Nat.succ n + 1), (-1) ^ x * ↑(Nat.choose (Nat.succ n) x)
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
[PROOFSTEP]
rw [← h, zero_pow (Nat.succ_pos n), if_neg (Nat.succ_ne_zero n)]
[GOAL]
R : Type u_1
n : ℕ
h0 : n ≠ 0
⊢ ∑ m in range (n + 1), (-1) ^ m * ↑(Nat.choose n m) = 0
[PROOFSTEP]
rw [Int.alternating_sum_range_choose, if_neg h0]
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in powerset x, f (card m) = ∑ m in range (card x + 1), Nat.choose (card x) m • f m
[PROOFSTEP]
trans ∑ m in range (x.card + 1), ∑ j in x.powerset.filter fun z ↦ z.card = m, f j.card
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in powerset x, f (card m) =
    ∑ m in range (card x + 1), ∑ j in filter (fun z => card z = m) (powerset x), f (card j)
[PROOFSTEP]
refine' (sum_fiberwise_of_maps_to _ _).symm
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∀ (x_1 : Finset β), x_1 ∈ powerset x → card x_1 ∈ range (card x + 1)
[PROOFSTEP]
intro y hy
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ powerset x
⊢ card y ∈ range (card x + 1)
[PROOFSTEP]
rw [mem_range, Nat.lt_succ_iff]
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ powerset x
⊢ card y ≤ card x
[PROOFSTEP]
rw [mem_powerset] at hy 
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ⊆ x
⊢ card y ≤ card x
[PROOFSTEP]
exact card_le_of_subset hy
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in range (card x + 1), ∑ j in filter (fun z => card z = m) (powerset x), f (card j) =
    ∑ m in range (card x + 1), Nat.choose (card x) m • f m
[PROOFSTEP]
refine' sum_congr rfl fun y _ ↦ _
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
⊢ ∑ j in filter (fun z => card z = y) (powerset x), f (card j) = Nat.choose (card x) y • f y
[PROOFSTEP]
rw [← card_powersetLen, ← sum_const]
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
⊢ ∑ j in filter (fun z => card z = y) (powerset x), f (card j) = ∑ _x in powersetLen y x, f y
[PROOFSTEP]
refine' sum_congr powersetLen_eq_filter.symm fun z hz ↦ _
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
z : Finset β
hz : z ∈ powersetLen y x
⊢ f (card z) = f y
[PROOFSTEP]
rw [(mem_powersetLen.1 hz).2]
[GOAL]
R : Type u_1
α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m in powerset x, (-1) ^ card m = if x = ∅ then 1 else 0
[PROOFSTEP]
rw [sum_powerset_apply_card]
[GOAL]
R : Type u_1
α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m in range (card x + 1), Nat.choose (card x) m • (-1) ^ m = if x = ∅ then 1 else 0
[PROOFSTEP]
simp only [nsmul_eq_mul', ← card_eq_zero, Int.alternating_sum_range_choose]
[GOAL]
R : Type u_1
α : Type u_2
x : Finset α
h0 : Finset.Nonempty x
⊢ ∑ m in powerset x, (-1) ^ card m = 0
[PROOFSTEP]
classical
rw [sum_powerset_neg_one_pow_card, if_neg]
rw [← Ne.def, ← nonempty_iff_ne_empty]
apply h0
[GOAL]
R : Type u_1
α : Type u_2
x : Finset α
h0 : Finset.Nonempty x
⊢ ∑ m in powerset x, (-1) ^ card m = 0
[PROOFSTEP]
rw [sum_powerset_neg_one_pow_card, if_neg]
[GOAL]
case hnc
R : Type u_1
α : Type u_2
x : Finset α
h0 : Finset.Nonempty x
⊢ ¬x = ∅
[PROOFSTEP]
rw [← Ne.def, ← nonempty_iff_ne_empty]
[GOAL]
case hnc
R : Type u_1
α : Type u_2
x : Finset α
h0 : Finset.Nonempty x
⊢ Finset.Nonempty x
[PROOFSTEP]
apply h0
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i in range (n + 2), f i (n + 1 - i) ^ Nat.choose (n + 1) i =
    (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i
[PROOFSTEP]
have A :
  (∏ i in range (n + 1), f (i + 1) (n - i) ^ (n.choose (i + 1))) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ (n.choose i)
[GOAL]
case A
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
[PROOFSTEP]
rw [prod_range_succ, prod_range_succ']
[GOAL]
case A
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ x in range n, f (x + 1) (n - x) ^ Nat.choose n (x + 1)) * f (n + 1) (n - n) ^ Nat.choose n (n + 1) * f 0 (n + 1) =
    (∏ k in range n, f (k + 1) (n + 1 - (k + 1)) ^ Nat.choose n (k + 1)) * f 0 (n + 1 - 0) ^ Nat.choose n 0
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
⊢ ∏ i in range (n + 2), f i (n + 1 - i) ^ Nat.choose (n + 1) i =
    (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i
[PROOFSTEP]
rw [prod_range_succ']
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
⊢ (∏ k in range (n + 1), f (k + 1) (n + 1 - (k + 1)) ^ Nat.choose (n + 1) (k + 1)) *
      f 0 (n + 1 - 0) ^ Nat.choose (n + 1) 0 =
    (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i
[PROOFSTEP]
simpa [Nat.choose_succ_succ, pow_add, prod_mul_distrib, A, mul_assoc] using
  mul_comm _
    _
      -- porting note: new lemma
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ ij in Nat.antidiagonal (n + 1), f ij.fst ij.snd ^ Nat.choose (n + 1) ij.fst =
    (∏ ij in Nat.antidiagonal n, f ij.fst (ij.snd + 1) ^ Nat.choose n ij.fst) *
      ∏ ij in Nat.antidiagonal n, f (ij.fst + 1) ij.snd ^ Nat.choose n ij.snd
[PROOFSTEP]
simp only [Nat.prod_antidiagonal_eq_prod_range_succ_mk, prod_pow_choose_succ]
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    (∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x) *
      ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
[PROOFSTEP]
have : ∀ i ∈ range (n + 1), i ≤ n := fun i hi ↦ by simpa [Nat.lt_succ_iff] using hi
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n i : ℕ
hi : i ∈ range (n + 1)
⊢ i ≤ n
[PROOFSTEP]
simpa [Nat.lt_succ_iff] using hi
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    (∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x) *
      ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i = ∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x
[PROOFSTEP]
refine prod_congr rfl fun i hi ↦ ?_
[GOAL]
case e_a
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
i : ℕ
hi : i ∈ range (succ n)
⊢ f i (n + 1 - i) ^ Nat.choose n i = f i (n - i + 1) ^ Nat.choose n i
[PROOFSTEP]
rw [tsub_add_eq_add_tsub (this _ hi)]
[GOAL]
case e_a
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
[PROOFSTEP]
refine prod_congr rfl fun i hi ↦ ?_
[GOAL]
case e_a
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
i : ℕ
hi : i ∈ range (succ n)
⊢ f (i + 1) (n - i) ^ Nat.choose n i = f (i + 1) (n - i) ^ Nat.choose n (n - i)
[PROOFSTEP]
rw [Nat.choose_symm (this _ hi)]
  -- porting note: moved from `Mathlib.Analysis.Calculus.ContDiff`
[GOAL]
R✝ : Type u_1
M : Type u_2
R : Type u_3
inst✝¹ : CommMonoid M
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ i in range (n + 2), ↑(Nat.choose (n + 1) i) * f i (n + 1 - i) =
    ∑ i in range (n + 1), ↑(Nat.choose n i) * f i (n + 1 - i) +
      ∑ i in range (n + 1), ↑(Nat.choose n i) * f (i + 1) (n - i)
[PROOFSTEP]
simpa only [nsmul_eq_mul] using sum_choose_succ_nsmul f n
[GOAL]
R✝ : Type u_1
M : Type u_2
R : Type u_3
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
[PROOFSTEP]
simpa only [nsmul_eq_mul] using sum_antidiagonal_choose_succ_nsmul f n
