-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_coeff (n : ℕ) : (taylor r f).coeff n = (hasseDeriv n f).eval r :=
  show (lcoeff R n).comp (taylor r) f = (leval r).comp (hasseDeriv n) f by
    congr 1; clear! f; ext i
    simp only [leval_apply, mul_one, one_mul, eval_monomial, LinearMap.comp_apply, coeff_C_mul,
      hasseDeriv_monomial, taylor_apply, monomial_comp, C_1, (commute_X (C r)).add_pow i,
      map_sum]
    simp only [lcoeff_apply, ← C_eq_natCast, mul_assoc, ← C_pow, ← C_mul, coeff_mul_C,
      (Nat.cast_commute _ _).eq, coeff_X_pow, boole_mul, Finset.sum_ite_eq, Finset.mem_range]
    split_ifs with h; · rfl
    push_neg at h; rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]

Proof state:
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ ((lcoeff R n ∘ₗ taylor r) ∘ₗ monomial i) 1 = ((leval r ∘ₗ hasseDeriv n) ∘ₗ monomial i) 1

Tactic:
simp only [leval_apply, mul_one, one_mul, eval_monomial, LinearMap.comp_apply, coeff_C_mul,
  hasseDeriv_monomial, taylor_apply, monomial_comp, C_1, (commute_X (C r)).add_pow i,
  map_sum]

Result:
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ ∑ x ∈ Finset.range (i + 1), (lcoeff R n) (X ^ x * C r ^ (i - x) * ↑(i.choose x)) = ↑(i.choose n) * r ^ (i - n)

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * ↑(i.choose n) = r ^ (i - n) * ↑(i.choose n)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ (lcoeff R n ∘ₗ taylor r) f = (leval r ∘ₗ hasseDeriv n) f

Tactic:
congr 1

Result:
case e_a
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑(i.choose n)

Tactic:
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(i.choose n)

Tactic:
push_neg at h

Result:
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑(i.choose n)

Proof state:
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ ∑ x ∈ Finset.range (i + 1), (lcoeff R n) (X ^ x * C r ^ (i - x) * ↑(i.choose x)) = ↑(i.choose n) * r ^ (i - n)

Tactic:
simp only [lcoeff_apply, ← C_eq_natCast, mul_assoc, ← C_pow, ← C_mul, coeff_mul_C,
  (Nat.cast_commute _ _).eq, coeff_X_pow, boole_mul, Finset.sum_ite_eq, Finset.mem_range]

Result:
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ (if n < i + 1 then r ^ (i - n) * ↑(i.choose n) else 0) = r ^ (i - n) * ↑(i.choose n)

Proof state:
case e_a
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n

Tactic:
ext i

Result:
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ ((lcoeff R n ∘ₗ taylor r) ∘ₗ monomial i) 1 = ((leval r ∘ₗ hasseDeriv n) ∘ₗ monomial i) 1

Proof state:
case e_a
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n

Tactic:
clear! f

Result:
case e_a
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n

Proof state:
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ (if n < i + 1 then r ^ (i - n) * ↑(i.choose n) else 0) = r ^ (i - n) * ↑(i.choose n)

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * ↑(i.choose n) = r ^ (i - n) * ↑(i.choose n)

case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(i.choose n)