-- Mathlib/RingTheory/PowerSeries/Binomial.lean
@[simp]
lemma binomialSeries_nat [CommRing A] (d : ℕ) :
    binomialSeries A (d : ℤ) = (1 + X) ^ d

Proof state:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
k : ℕ
hk : k ∈ range (d + 1)
hkd : k ≤ d
⊢ (coeff A (n - k)) ↑(d.choose k) = 0

Tactic:
rw [← map_natCast (C A), coeff_ne_zero_C (by omega)]

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CommRing A
d : ℕ
⊢ binomialSeries A ↑d = (1 + X) ^ d

Tactic:
ext n

Result:
case h
A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ (coeff A n) (binomialSeries A ↑d) = (coeff A n) ((1 + X) ^ d)

Proof state:
case neg
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ ↑↑(d.choose n) = if n ≤ n then (coeff A (n - n)) ↑(d.choose n) else 0

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
k : ℕ
hk : k ∈ range (d + 1)
hkn : k ≠ n
⊢ (if n = k then ↑(d.choose k) else 0) = 0

Tactic:
exact if_neg (Ne.symm hkn)

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ n < d + 1

Tactic:
omega

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ n ∈ range (d + 1)

Tactic:
simp only [mem_range]

Result:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ n < d + 1

Proof state:
case neg
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ (coeff A n) (binomialSeries A ↑d) = (coeff A n) ((1 + X) ^ d)

Tactic:
rw [binomialSeries_coeff, add_comm, add_pow]

Result:
case neg
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ Ring.choose (↑d) n • 1 = (coeff A n) (∑ m ∈ range (d + 1), X ^ m * 1 ^ (d - m) * ↑(d.choose m))

Proof state:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ ∀ b ∈ range (d + 1), b ≠ n → (coeff A n) (X ^ b * ↑(d.choose b)) = 0

Tactic:
intro k hk hkn

Result:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
k : ℕ
hk : k ∈ range (d + 1)
hkn : k ≠ n
⊢ (coeff A n) (X ^ k * ↑(d.choose k)) = 0

Proof state:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
⊢ (coeff A n) (binomialSeries A ↑d) = (coeff A n) ((1 + X) ^ d)

Tactic:
rw [binomialSeries_coeff, add_comm, add_pow, map_sum, Ring.choose_natCast, natCast_zsmul,
  Nat.choose_eq_zero_of_lt h, zero_nsmul, sum_eq_zero]

Result:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
⊢ ∀ x ∈ range (d + 1), (coeff A n) (X ^ x * 1 ^ (d - x) * ↑(d.choose x)) = 0

Proof state:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
k : ℕ
hk : k ∈ range (d + 1)
⊢ (coeff A n) (X ^ k * 1 ^ (d - k) * ↑(d.choose k)) = 0

Tactic:
rw [one_pow, mul_one, coeff_X_pow_mul']

Result:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
k : ℕ
hk : k ∈ range (d + 1)
⊢ (if k ≤ n then (coeff A (n - k)) ↑(d.choose k) else 0) = 0

Proof state:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
k : ℕ
hk : k ∈ range (d + 1)
hkn : k ≠ n
⊢ (coeff A n) (X ^ k * ↑(d.choose k)) = 0

Tactic:
rw [mul_comm, ← map_natCast (C A), coeff_C_mul_X_pow]

Result:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
k : ℕ
hk : k ∈ range (d + 1)
hkn : k ≠ n
⊢ (if n = k then ↑(d.choose k) else 0) = 0

Proof state:
case h
A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ (coeff A n) (binomialSeries A ↑d) = (coeff A n) ((1 + X) ^ d)

Tactic:
by_cases h : d < n

Result:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
⊢ (coeff A n) (binomialSeries A ↑d) = (coeff A n) ((1 + X) ^ d)

case neg
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ (coeff A n) (binomialSeries A ↑d) = (coeff A n) ((1 + X) ^ d)

Proof state:
case neg
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ ↑(Ring.choose (↑d) n) = ∑ x ∈ range (d + 1), (coeff A n) (X ^ x * ↑(d.choose x))

Tactic:
rw [sum_eq_single_of_mem n (by simp only [mem_range]; omega) ?_, coeff_X_pow_mul',
  Ring.choose_eq_nat_choose]

Result:
case neg
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ ↑↑(d.choose n) = if n ≤ n then (coeff A (n - n)) ↑(d.choose n) else 0

A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ ∀ b ∈ range (d + 1), b ≠ n → (coeff A n) (X ^ b * ↑(d.choose b)) = 0

Proof state:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
⊢ ∀ x ∈ range (d + 1), (coeff A n) (X ^ x * 1 ^ (d - x) * ↑(d.choose x)) = 0

Tactic:
intro k hk

Result:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
k : ℕ
hk : k ∈ range (d + 1)
⊢ (coeff A n) (X ^ k * 1 ^ (d - k) * ↑(d.choose k)) = 0

Proof state:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
k : ℕ
hk : k ∈ range (d + 1)
hkd : k ≤ d
⊢ (if k ≤ n then (coeff A (n - k)) ↑(d.choose k) else 0) = 0

Tactic:
simp only [hkd.trans (le_of_lt h), ↓reduceIte]

Result:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
k : ℕ
hk : k ∈ range (d + 1)
hkd : k ≤ d
⊢ (coeff A (n - k)) ↑(d.choose k) = 0

Proof state:
case neg
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ Ring.choose (↑d) n • 1 = (coeff A n) (∑ m ∈ range (d + 1), X ^ m * 1 ^ (d - m) * ↑(d.choose m))

Tactic:
simp only [zsmul_eq_mul, mul_one, one_pow, map_sum]

Result:
case neg
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : ¬d < n
⊢ ↑(Ring.choose (↑d) n) = ∑ x ∈ range (d + 1), (coeff A n) (X ^ x * ↑(d.choose x))

Proof state:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
k : ℕ
hk : k ∈ range (d + 1)
hkd : k ≤ d
⊢ n - k ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
k : ℕ
hk : k ∈ range (d + 1)
⊢ (if k ≤ n then (coeff A (n - k)) ↑(d.choose k) else 0) = 0

Tactic:
have hkd : k ≤ d := mem_range_succ_iff.mp hk

Result:
case pos
A : Type u_2
inst✝ : CommRing A
d n : ℕ
h : d < n
k : ℕ
hk : k ∈ range (d + 1)
hkd : k ≤ d
⊢ (if k ≤ n then (coeff A (n - k)) ↑(d.choose k) else 0) = 0