Theorem: Real.hasTemperateGrowth_fourierChar (ForML/Trigonometric.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => ↑(fourierChar (Multiplicative.ofAdd x))
Tactic:
simp [fourierChar_apply]
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (2 * ↑π * ↑x * I)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (2 * ↑π * ↑x * I)
Tactic:
norm_cast
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑(2 * π * x) * I)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑(2 * π * x) * I)
Tactic:
simp_rw [← Complex.real_smul]
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp ((2 * π * x) • I)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp ((2 * π * x) • I)
Tactic:
exact (Function.hasTemperateGrowth_const_mul (2 * π)).cexp_real_smul_I
State after:
no goals