refine Filter.Tendsto.comp ?_ Filter.tendsto_neg_atTop_atBot
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
    (fun x =>
      ((hasTemperateGrowth_smul
            (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
          f)
        (-x))
    Filter.atTop (nhds 0)
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)