-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem geom_sum_X_comp_X_add_one_eq_sum (n : ℕ) :
    (∑ i ∈ range n, (X : R[X]) ^ i).comp (X + 1) =
      (Finset.range n).sum fun i : ℕ => (n.choose (i + 1) : R[X]) * X ^ i

Proof state:
case zero
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (comp 0 (X + 1)).coeff i = ↑0

Tactic:
simp only [zero_comp, coeff_zero, Nat.cast_zero]

Result:
no goals

Proof state:
case h₁
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ i ∉ range n → (if i = i then ↑(n.choose (i + 1)) else 0) = 0

Tactic:
simp +contextual only [Nat.lt_add_one_iff, Nat.choose_eq_zero_of_lt,
  Nat.cast_zero, Finset.mem_range, not_lt, eq_self_iff_true, if_true, imp_true_iff]

Result:
no goals

Proof state:
case a
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

Tactic:
trans (n.choose (i + 1) : R)

Result:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

Proof state:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = ∑ x ∈ range n, if i = x then ↑(n.choose (x + 1)) else 0

Tactic:
rw [Finset.sum_eq_single i, if_pos rfl]

Result:
case h₀
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ∀ b ∈ range n, b ≠ i → (if i = b then ↑(n.choose (b + 1)) else 0) = 0

case h₁
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ i ∉ range n → (if i = i then ↑(n.choose (i + 1)) else 0) = 0

Proof state:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

Tactic:
induction' n with n ih generalizing i

Result:
case zero
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ ((∑ i ∈ range 0, X ^ i).comp (X + 1)).coeff i = ↑(Nat.choose 0 (i + 1))

case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : ∀ (i : ℕ), ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))
i : ℕ
⊢ ((∑ i ∈ range (n + 1), X ^ i).comp (X + 1)).coeff i = ↑((n + 1).choose (i + 1))

Proof state:
case zero
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ ((∑ i ∈ range 0, X ^ i).comp (X + 1)).coeff i = ↑(Nat.choose 0 (i + 1))

Tactic:
dsimp

Result:
case zero
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (comp 0 (X + 1)).coeff i = ↑0

Proof state:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

Tactic:
swap

Result:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

Proof state:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

Tactic:
simp only [finset_sum_coeff, ← C_eq_natCast, coeff_C_mul_X_pow]

Result:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = ∑ x ∈ range n, if i = x then ↑(n.choose (x + 1)) else 0

Proof state:
case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : ∀ (i : ℕ), ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))
i : ℕ
⊢ ((∑ i ∈ range (n + 1), X ^ i).comp (X + 1)).coeff i = ↑((n + 1).choose (i + 1))

Tactic:
simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ,
Nat.cast_add, coeff_X_add_one_pow]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (∑ i ∈ range n, X ^ i).comp (X + 1) = ∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i

Tactic:
ext i

Result:
case a
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

Proof state:
case h₀
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ∀ b ∈ range n, b ≠ i → (if i = b then ↑(n.choose (b + 1)) else 0) = 0

Tactic:
simp +contextual only [@eq_comm _ i, if_false, eq_self_iff_true,
  imp_true_iff]

Result:
no goals