by_cases hR : R = 0 <;> simp [hR, scale]
case toFun.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
⊢ (f.scale R).deriv.toFun v = (R⁻¹ • f.deriv.scale R).toFun v
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 neg
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 := fun x => funscale f.toFun R x, h1 := ⋯, h2 := ⋯ }.deriv.toFun v = R⁻¹ • funscale f.deriv.toFun R v