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

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => sin x
Tactic:
simp_rw [sin, Complex.sin]
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => ((cexp (-↑x * I) - cexp (↑x * I)) * 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)) * I / 2).re
Tactic:
refine (((Function.HasTemperateGrowth.sub ?_ ?_).mul_const Complex.I).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:
. norm_cast
  simp_rw [← Complex.real_smul]
  exact Function.hasTemperateGrowth_neg.cexp_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:
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 Complex.hasTemperateGrowth_exp_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:
norm_cast
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:
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 Function.hasTemperateGrowth_neg.cexp_real_smul_I
State after:
no goals