Theorem: SchwartzMap.Real.fourierIntegrand_eq_hasTemperateGrowth_smul (ForML/SchwartzRealFourier.lean)

State before:
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
Tactic:
simp [hasTemperateGrowth_smul_apply]
State after:
no goals