Theorem: fderiv_cexp_real (ForML/Util.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ fderiv ℝ (fun x => Complex.exp (f x)) x = Complex.exp (f x) • fderiv ℝ f x
Tactic:
change fderiv ℝ (Complex.exp ∘ f) x = _
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ fderiv ℝ (Complex.exp ∘ f) x = Complex.exp (f x) • fderiv ℝ f x

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ fderiv ℝ (Complex.exp ∘ f) x = Complex.exp (f x) • fderiv ℝ f x
Tactic:
rw [fderiv.comp x Complex.differentiable_exp.differentiableAt hf]
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ ContinuousLinearMap.comp (fderiv ℝ Complex.exp (f x)) (fderiv ℝ f x) = Complex.exp (f x) • fderiv ℝ f x

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ ContinuousLinearMap.comp (fderiv ℝ Complex.exp (f x)) (fderiv ℝ f x) = Complex.exp (f x) • fderiv ℝ f x
Tactic:
rw [(Complex.hasStrictFDerivAt_exp_real (f x)).hasFDerivAt.fderiv]
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ ContinuousLinearMap.comp (Complex.exp (f x) • 1) (fderiv ℝ f x) = Complex.exp (f x) • fderiv ℝ f x

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ ContinuousLinearMap.comp (Complex.exp (f x) • 1) (fderiv ℝ f x) = Complex.exp (f x) • fderiv ℝ f x
Tactic:
simp [ContinuousLinearMap.one_def]
State after:
no goals