let f'' := f'.deriv
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
⊢ Tendsto (fun R => ‖f - W21.ofCS2 (g.scale R * f)‖) atTop (𝓝 0)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
⊢ Tendsto (fun R => ‖f - W21.ofCS2 (g.scale R * f)‖) atTop (𝓝 0)