simp [hasTemperateGrowth_smul_apply]
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
x : ℝ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ((hasTemperateGrowth_smul
          (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
        f)
      x
no goals