case a
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ coeff (comp (∑ i in range n, X ^ i) (X + 1)) i = coeff (∑ i in range n, ↑(Nat.choose n (i + 1)) * X ^ i) i
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n : ℕ
⊢ comp (∑ i in range n, X ^ i) (X + 1) = ∑ i in range n, ↑(Nat.choose n (i + 1)) * X ^ i
ext i
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ coeff (comp (∑ i in range n, X ^ i) (X + 1)) i = ↑(Nat.choose n (i + 1))

R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ ↑(Nat.choose n (i + 1)) = coeff (∑ i in range n, ↑(Nat.choose n (i + 1)) * X ^ i) i
case a
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ coeff (comp (∑ i in range n, X ^ i) (X + 1)) i = coeff (∑ i in range n, ↑(Nat.choose n (i + 1)) * X ^ i) i
trans (n.choose (i + 1) : R)
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ ↑(Nat.choose n (i + 1)) = coeff (∑ i in range n, ↑(Nat.choose n (i + 1)) * X ^ i) i

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

R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ ↑(Nat.choose n (i + 1)) = coeff (∑ i in range n, ↑(Nat.choose n (i + 1)) * X ^ i) i
swap
case zero
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
i✝ i : ℕ
⊢ coeff (comp (∑ i in range Nat.zero, X ^ i) (X + 1)) i = ↑(Nat.choose Nat.zero (i + 1))

case succ
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
i✝ n : ℕ
ih : ∀ (i : ℕ), coeff (comp (∑ i in range n, X ^ i) (X + 1)) i = ↑(Nat.choose n (i + 1))
i : ℕ
⊢ coeff (comp (∑ i in range (Nat.succ n), X ^ i) (X + 1)) i = ↑(Nat.choose (Nat.succ n) (i + 1))
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ coeff (comp (∑ i in range n, X ^ i) (X + 1)) i = ↑(Nat.choose n (i + 1))
induction' n with n ih generalizing i
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ ↑(Nat.choose n (i + 1)) = ∑ x in range n, if i = x then ↑(Nat.choose n (x + 1)) else 0
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ ↑(Nat.choose n (i + 1)) = coeff (∑ i in range n, ↑(Nat.choose n (i + 1)) * X ^ i) i
simp only [finset_sum_coeff, ← C_eq_nat_cast, coeff_C_mul_X_pow]
case h₀
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ ∀ (b : ℕ), b ∈ range n → b ≠ i → (if i = b then ↑(Nat.choose n (b + 1)) else 0) = 0

case h₁
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ ¬i ∈ range n → (if i = i then ↑(Nat.choose n (i + 1)) else 0) = 0
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ ↑(Nat.choose n (i + 1)) = ∑ x in range n, if i = x then ↑(Nat.choose n (x + 1)) else 0
rw [Finset.sum_eq_single i, if_pos rfl]
no goals
case h₀
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ ∀ (b : ℕ), b ∈ range n → b ≠ i → (if i = b then ↑(Nat.choose n (b + 1)) else 0) = 0
simp (config := { contextual := true }) only [@eq_comm _ i, if_false, eq_self_iff_true,
  imp_true_iff]
no goals
case h₁
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
n i : ℕ
⊢ ¬i ∈ range n → (if i = i then ↑(Nat.choose n (i + 1)) else 0) = 0
simp (config := { contextual := true }) 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]
case zero
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
i✝ i : ℕ
⊢ coeff (comp 0 (X + 1)) i = ↑0
case zero
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
i✝ i : ℕ
⊢ coeff (comp (∑ i in range Nat.zero, X ^ i) (X + 1)) i = ↑(Nat.choose Nat.zero (i + 1))
dsimp
no goals
case zero
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
i✝ i : ℕ
⊢ coeff (comp 0 (X + 1)) i = ↑0
simp only [zero_comp, coeff_zero, Nat.cast_zero]
case succ
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
i✝ n : ℕ
ih : ∀ (i : ℕ), coeff (comp (∑ i in range n, X ^ i) (X + 1)) i = ↑(Nat.choose n (i + 1))
i : ℕ
⊢ coeff (comp (∑ i in range (Nat.succ n), X ^ i) (X + 1)) i = ↑(Nat.choose (Nat.succ n) (i + 1))
case succ
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
i✝ n : ℕ
ih : ∀ (i : ℕ), coeff (comp (∑ i in range n, X ^ i) (X + 1)) i = ↑(Nat.choose n (i + 1))
i : ℕ
⊢ coeff (comp (∑ i in range (Nat.succ n), X ^ i) (X + 1)) i = ↑(Nat.choose (Nat.succ n) (i + 1))
dsimp
no goals
case succ
R : Type u
S : Type ?u.49481
inst✝ : Semiring R
i✝ n : ℕ
ih : ∀ (i : ℕ), coeff (comp (∑ i in range n, X ^ i) (X + 1)) i = ↑(Nat.choose n (i + 1))
i : ℕ
⊢ coeff (comp (∑ i in range (Nat.succ n), X ^ i) (X + 1)) i = ↑(Nat.choose (Nat.succ n) (i + 1))
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]