exact Filter.Tendsto.mono_left (zero_at_infty _) atBot_le_cocompact
case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (⇑((hasTemperateGrowth_smul
          (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
        f))
    Filter.atBot (nhds 0)
no goals