exact ((f.hasDerivAt (R⁻¹ • v)).scomp v (by simpa using (hasDerivAt_id v).const_smul R⁻¹)).deriv
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
no goals