simp [deriv, smul]
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : R = 0
⊢ { toFun := 0, h1 := ⋯, h2 := ⋯ }.deriv.toFun v = 0
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : R = 0
⊢ _root_.deriv 0 v = 0