case e_a
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ LinearMap.comp (lcoeff R n) (taylor r) = LinearMap.comp (leval r) (hasseDeriv n)
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ ↑(LinearMap.comp (lcoeff R n) (taylor r)) f = ↑(LinearMap.comp (leval r) (hasseDeriv n)) f
congr 1
case e_a
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ LinearMap.comp (lcoeff R n) (taylor r) = LinearMap.comp (leval r) (hasseDeriv n)
case e_a
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ LinearMap.comp (lcoeff R n) (taylor r) = LinearMap.comp (leval r) (hasseDeriv n)
clear! f
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ ↑(LinearMap.comp (LinearMap.comp (lcoeff R n) (taylor r)) (monomial i)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (leval r) (hasseDeriv n)) (monomial i)) 1
case e_a
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ LinearMap.comp (lcoeff R n) (taylor r) = LinearMap.comp (leval r) (hasseDeriv n)
ext i
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ (Finset.sum (Finset.range (i + 1)) fun x => ↑(lcoeff R n) (X ^ x * ↑C r ^ (i - x) * ↑(Nat.choose i x))) =
    ↑(Nat.choose i n) * r ^ (i - n)
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ ↑(LinearMap.comp (LinearMap.comp (lcoeff R n) (taylor r)) (monomial i)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (leval r) (hasseDeriv n)) (monomial i)) 1
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,
  LinearMap.map_sum]
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ (if n < i + 1 then r ^ (i - n) * ↑(Nat.choose i n) else 0) = r ^ (i - n) * ↑(Nat.choose i n)
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ (Finset.sum (Finset.range (i + 1)) fun x => ↑(lcoeff R n) (X ^ x * ↑C r ^ (i - x) * ↑(Nat.choose i x))) =
    ↑(Nat.choose i n) * r ^ (i - n)
simp only [lcoeff_apply, ← C_eq_nat_cast, 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]
case e_a.h.h.inl
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * ↑(Nat.choose i n) = r ^ (i - n) * ↑(Nat.choose i n)

case e_a.h.h.inr
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(Nat.choose i n)
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ (if n < i + 1 then r ^ (i - n) * ↑(Nat.choose i n) else 0) = r ^ (i - n) * ↑(Nat.choose i n)
split_ifs with h
case e_a.h.h.inr
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑(Nat.choose i n)
case e_a.h.h.inr
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(Nat.choose i n)
push_neg at h
no goals
case e_a.h.h.inr
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑(Nat.choose i n)
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, MulZeroClass.mul_zero]
no goals
case e_a.h.h.inl
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * ↑(Nat.choose i n) = r ^ (i - n) * ↑(Nat.choose i n)
rfl