Theorem: HasDerivAt.cexp_real_smul_I (ForML/Trigonometric.lean)

State before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (↑f' * I * cexp (f x • I)) x
Tactic:
suffices : HasDerivAt (fun x : ℝ => Complex.exp (f x • I)) (f' • (I * Complex.exp (f x • I))) x
State after:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
this : HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
⊢ HasDerivAt (fun x => cexp (f x • I)) (↑f' * I * cexp (f x • I)) x

case this
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x

State before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
this : HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
⊢ HasDerivAt (fun x => cexp (f x • I)) (↑f' * I * cexp (f x • I)) x

case this
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
Tactic:
. simpa [← mul_assoc] using this
State after:
case this
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x

State before:
case this
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
Tactic:
exact HasDerivAt.comp_of_tower x Complex.hasDerivAt_exp_real_smul_I hf
State after:
no goals

State before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
this : HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
⊢ HasDerivAt (fun x => cexp (f x • I)) (↑f' * I * cexp (f x • I)) x
Tactic:
simpa [← mul_assoc] using this
State after:
no goals