refine tendsto_of_tendsto_of_tendsto_of_le_of_le (h := fun x => C * (1 + |x|)⁻¹) tendsto_const_nhds ?_ ?_ ?_
case intro
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds 0)

case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖

case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹