convert hasDerivAt (f.scale R) x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ HasDerivAt (f.scale R).toFun (R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x)) x
case h.e'_7
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x) = (f.scale R).deriv.toFun x