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

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cos x
Tactic:
simp_rw [cos, Complex.cos]
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => ((cexp (↑x * I) + cexp (-↑x * I)) / 2).re

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => ((cexp (↑x * I) + cexp (-↑x * I)) / 2).re
Tactic:
refine ((Function.HasTemperateGrowth.add ?_ ?_).div_const 2).re
State after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑x * I)

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-↑x * I)

State before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (↑x * I)

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-↑x * I)
Tactic:
. simp_rw [← Complex.real_smul]
  exact Complex.hasTemperateGrowth_exp_real_smul_I
State after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-↑x * I)

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

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

State before:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (-x • I)
Tactic:
exact Function.hasTemperateGrowth_neg.cexp_real_smul_I
State after:
no goals

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

State before:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (x • I)
Tactic:
exact Complex.hasTemperateGrowth_exp_real_smul_I
State after:
no goals