Theorem: CS.tendsto_scale (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
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))
Tactic:
apply (tendsto_funscale f.continuous.continuousAt x).congr'
State after:
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

State before:
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
Tactic:
filter_upwards [eventually_ne_atTop 0] with R hR
State after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS n E
x R : ℝ
hR : R ≠ 0
⊢ funscale f.toFun R x = (f.scale R).toFun x

State before:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS n E
x R : ℝ
hR : R ≠ 0
⊢ funscale f.toFun R x = (f.scale R).toFun x
Tactic:
simp [scale, hR]
State after:
no goals