apply (tendsto_funscale f.continuous.continuousAt x).congr'
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS n E
x : ℝ
⊢ Tendsto (fun R => (f.scale R).toFun x) atTop (𝓝 (f.toFun 0))
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS n E
x : ℝ
⊢ (fun R => funscale f.toFun R x) =ᶠ[atTop] fun R => (f.scale R).toFun x