[GOAL]
R : Type u_1
inst✝ : Semiring R
r✝ : R
f✝ : R[X]
r c : R
f : R[X]
⊢ AddHom.toFun
      { toFun := fun f => comp f (X + ↑C r),
        map_add' := (_ : ∀ (f g : R[X]), comp (f + g) (X + ↑C r) = comp f (X + ↑C r) + comp g (X + ↑C r)) }
      (c • f) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun f => comp f (X + ↑C r),
          map_add' := (_ : ∀ (f g : R[X]), comp (f + g) (X + ↑C r) = comp f (X + ↑C r) + comp g (X + ↑C r)) }
        f
[PROOFSTEP]
simp only [smul_eq_C_mul, C_mul_comp, RingHom.id_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ↑(taylor r) X = X + ↑C r
[PROOFSTEP]
simp only [taylor_apply, X_comp]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
x : R
⊢ ↑(taylor r) (↑C x) = ↑C x
[PROOFSTEP]
simp only [taylor_apply, C_comp]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ taylor 0 = LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case h.h.a
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n✝¹ n✝ : ℕ
⊢ coeff (↑(LinearMap.comp (taylor 0) (monomial n✝¹)) 1) n✝ = coeff (↑(LinearMap.comp LinearMap.id (monomial n✝¹)) 1) n✝
[PROOFSTEP]
simp only [taylor_apply, add_zero, comp_X, _root_.map_zero, LinearMap.id_comp, Function.comp_apply, LinearMap.coe_comp]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f✝ f : R[X]
⊢ ↑(taylor 0) f = f
[PROOFSTEP]
rw [taylor_zero', LinearMap.id_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ↑(taylor r) 1 = ↑C 1
[PROOFSTEP]
rw [← C_1, taylor_C]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
i : ℕ
k : R
⊢ ↑(taylor r) (↑(monomial i) k) = ↑C k * (X + ↑C r) ^ i
[PROOFSTEP]
simp [taylor_apply]
[GOAL]
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
[PROOFSTEP]
congr 1
[GOAL]
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)
[PROOFSTEP]
clear! f
[GOAL]
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)
[PROOFSTEP]
ext i
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
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)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
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)
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(Nat.choose i n)
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑(Nat.choose i n)
[PROOFSTEP]
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ coeff (↑(taylor r) f) 0 = eval r f
[PROOFSTEP]
rw [taylor_coeff, hasseDeriv_zero, LinearMap.id_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ coeff (↑(taylor r) f) 1 = eval r (↑derivative f)
[PROOFSTEP]
rw [taylor_coeff, hasseDeriv_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
⊢ natDegree (↑(taylor r) p) = natDegree p
[PROOFSTEP]
refine' map_natDegree_eq_natDegree _ _
[GOAL]
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑(taylor r) (↑(monomial n) c)) = n
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
✝ : Nontrivial R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑(taylor r) (↑(monomial n) c)) = n
[PROOFSTEP]
intro n c c0
[GOAL]
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
✝ : Nontrivial R
n : ℕ
c : R
c0 : c ≠ 0
⊢ natDegree (↑(taylor r) (↑(monomial n) c)) = n
[PROOFSTEP]
simp [taylor_monomial, natDegree_C_mul_eq_of_mul_ne_zero, natDegree_pow_X_add_C, c0]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f : R✝[X]
R : Type u_2
inst✝ : CommSemiring R
r : R
p q : R[X]
⊢ ↑(taylor r) (p * q) = ↑(taylor r) p * ↑(taylor r) q
[PROOFSTEP]
simp only [taylor_apply, mul_comp]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommSemiring R
f : R[X]
r s : R
⊢ ↑(taylor r) (↑(taylor s) f) = ↑(taylor (r + s)) f
[PROOFSTEP]
simp only [taylor_apply, comp_assoc, map_add, add_comp, X_comp, C_comp, C_add, add_assoc]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommSemiring R
r : R
f : R[X]
s : R
⊢ eval s (↑(taylor r) f) = eval (s + r) f
[PROOFSTEP]
simp only [taylor_apply, eval_comp, eval_C, eval_X, eval_add]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
r : R
f : R[X]
s : R
⊢ eval (s - r) (↑(taylor r) f) = eval s f
[PROOFSTEP]
rw [taylor_eval, sub_add_cancel]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f : R✝[X]
R : Type u_2
inst✝ : CommRing R
r : R
⊢ Function.Injective ↑(taylor r)
[PROOFSTEP]
intro f g h
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
r : R
f g : R[X]
h : ↑(taylor r) f = ↑(taylor r) g
⊢ f = g
[PROOFSTEP]
apply_fun taylor (-r) at h 
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
r : R
f g : R[X]
h : ↑(taylor (-r)) (↑(taylor r) f) = ↑(taylor (-r)) (↑(taylor r) g)
⊢ f = g
[PROOFSTEP]
simpa only [taylor_apply, comp_assoc, add_comp, X_comp, C_comp, C_neg, neg_add_cancel_right, comp_X] using h
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ f = 0
[PROOFSTEP]
apply taylor_injective r
[GOAL]
case a
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ ↑(taylor r) f = ↑(taylor r) 0
[PROOFSTEP]
rw [LinearMap.map_zero]
[GOAL]
case a
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ ↑(taylor r) f = 0
[PROOFSTEP]
ext k
[GOAL]
case a.a
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
k : ℕ
⊢ coeff (↑(taylor r) f) k = coeff 0 k
[PROOFSTEP]
simp only [taylor_coeff, h, coeff_zero]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
⊢ (sum (↑(taylor r) f) fun i a => ↑C a * (X - ↑C r) ^ i) = f
[PROOFSTEP]
rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_self, taylor_zero]
