apply Tendsto.comp (tendsto_nhds_of_eventually_eq ?_) tendsto_id
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
⊢ Tendsto f atTop (𝓝 0)
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x' : ℝ) in atTop, f x' = 0