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

State before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ deriv (fun x => cexp (f x • I)) x = ↑(deriv f x) * I * cexp (f x • I)
Tactic:
rw [deriv_cexp (hf.smul_const I)]
State after:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (f x • I) * deriv (fun y => f y • I) x = ↑(deriv f x) * I * cexp (f x • I)

State before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (f x • I) * deriv (fun y => f y • I) x = ↑(deriv f x) * I * cexp (f x • I)
Tactic:
rw [deriv_smul hf (differentiableAt_const I)]
State after:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (f x • I) * (f x • deriv (fun x => I) x + deriv f x • I) = ↑(deriv f x) * I * cexp (f x • I)

State before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (f x • I) * (f x • deriv (fun x => I) x + deriv f x • I) = ↑(deriv f x) * I * cexp (f x • I)
Tactic:
simp
State after:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (↑(f x) * I) * (↑(deriv f x) * I) = ↑(deriv f x) * I * cexp (↑(f x) * I)

State before:
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (↑(f x) * I) * (↑(deriv f x) * I) = ↑(deriv f x) * I * cexp (↑(f x) * I)
Tactic:
ring_nf
State after:
no goals