case a
R✝ : Type ?u.227456
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ ↑(taylor r) f = ↑(taylor r) 0
R✝ : Type ?u.227456
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ f = 0
apply taylor_injective r
case a
R✝ : Type ?u.227456
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ ↑(taylor r) f = 0
case a
R✝ : Type ?u.227456
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ ↑(taylor r) f = ↑(taylor r) 0
rw [LinearMap.map_zero]
case a.a
R✝ : Type ?u.227456
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
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
case a
R✝ : Type ?u.227456
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ ↑(taylor r) f = 0
ext k
no goals
case a.a
R✝ : Type ?u.227456
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
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
simp only [taylor_coeff, h, coeff_zero]