awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ DifferentiableAt 𝕜 cexp x

Tactic:
differentiable_exp x

Premises used: Complex.differentiable_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
⊢ deriv cexp = cexp

Tactic:
funext fun x => (hasDerivAt_exp x).deriv

Premises used: HasDerivAt.deriv, funext, Complex.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
n : ℕ
rw : deriv^[n] (deriv cexp) = cexp
rw₁ : deriv^[n] cexp = cexp
rw₂ rw₃ : cexp = cexp
⊢ deriv^[n + 1] cexp = cexp

Tactic:
rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]

Premises used: Function.iterate_succ_apply, Complex.deriv_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
n : WithTop ℕ∞
⊢ ContDiff 𝕜 n cexp

Tactic:
analyticOnNhd_cexp.restrictScalars.contDiff

Premises used: AnalyticOnNhd.contDiff, analyticOnNhd_cexp, AnalyticOnNhd.restrictScalars
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
⊢ HasStrictDerivAt cexp (cexp x) x

Tactic:
contDiff_exp.contDiffAt.hasStrictDerivAt' (hasDerivAt_exp x) one_ne_zero

Premises used: Complex.contDiff_exp, one_ne_zero, Complex.hasDerivAt_exp, ContDiffAt.hasStrictDerivAt', ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℂ
⊢ HasStrictFDerivAt cexp (HSMul.hSMul (β := ℂ →L[ℝ] ℂ) (cexp x) 1) x

Tactic:
(hasStrictDerivAt_exp x).complexToReal_fderiv

Premises used: Complex.hasStrictDerivAt_exp, HasStrictDerivAt.complexToReal_fderiv
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
f : 𝕜 → ℂ
f' : ℂ
x : 𝕜
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ Complex.exp (f x)) (Complex.exp (f x) * f') x

Tactic:
(Complex.hasStrictDerivAt_exp (f x)).comp x hf

Premises used: HasStrictDerivAt.comp, Complex.hasStrictDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
f : 𝕜 → ℂ
f' : ℂ
x : 𝕜
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : 𝕜) ↦ Complex.exp (f x)) (Complex.exp (f x) * f') x

Tactic:
(Complex.hasDerivAt_exp (f x)).comp x hf

Premises used: HasDerivAt.comp, Complex.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
f : 𝕜 → ℂ
f' : ℂ
x : 𝕜
s : Set 𝕜
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ Complex.exp (f x)) (Complex.exp (f x) * f') s x

Tactic:
(Complex.hasDerivAt_exp (f x)).comp_hasDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasDerivWithinAt, Complex.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
f : 𝕜 → ℂ
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (x : 𝕜) ↦ Complex.exp (f x)) s x = Complex.exp (f x) * derivWithin f s x

Tactic:
hf.hasDerivWithinAt.cexp.derivWithin hxs

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.cexp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
f : 𝕜 → ℂ
x : 𝕜
hc : DifferentiableAt 𝕜 f x
⊢ deriv (fun (x : 𝕜) ↦ Complex.exp (f x)) x = Complex.exp (f x) * deriv f x

Tactic:
hc.hasDerivAt.cexp.deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.cexp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
f' : E →L[𝕜] ℂ
x : E
hf : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (fun (x : E) ↦ Complex.exp (f x)) (Complex.exp (f x) • f') x

Tactic:
(Complex.hasStrictDerivAt_exp (f x)).comp_hasStrictFDerivAt x hf

Premises used: HasStrictDerivAt.comp_hasStrictFDerivAt, Complex.hasStrictDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
f' : E →L[𝕜] ℂ
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ Complex.exp (f x)) (Complex.exp (f x) • f') s x

Tactic:
(Complex.hasDerivAt_exp (f x)).comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, Complex.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
f' : E →L[𝕜] ℂ
x : E
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun (x : E) ↦ Complex.exp (f x)) (Complex.exp (f x) • f') x

Tactic:
hasFDerivWithinAt_univ.1 <| hf.hasFDerivWithinAt.cexp

Premises used: HasFDerivAt.hasFDerivWithinAt, HasFDerivWithinAt.cexp, Iff.mp, hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
x : E
s : Set E
hf : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (F := ℂ) (fun (x : E) ↦ Complex.exp (f x)) s x

Tactic:
hf.hasFDerivWithinAt.cexp.differentiableWithinAt

Premises used: HasFDerivWithinAt.cexp, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
x : E
hc : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (F := ℂ) (fun (x : E) ↦ Complex.exp (f x)) x

Tactic:
hc.hasFDerivAt.cexp.differentiableAt

Premises used: HasFDerivAt.cexp, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
s : Set E
hc : DifferentiableOn 𝕜 f s
⊢ DifferentiableOn 𝕜 (F := ℂ) (fun (x : E) ↦ Complex.exp (f x)) s

Tactic:
fun x h => (hc x h).cexp

Premises used: DifferentiableOn, DifferentiableWithinAt.cexp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
hc : Differentiable 𝕜 f
⊢ Differentiable 𝕜 (F := ℂ) fun (x : E) ↦ Complex.exp (f x)

Tactic:
fun x => (hc x).cexp

Premises used: Differentiable, DifferentiableAt.cexp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
n : ℕ∞ω
h : ContDiff 𝕜 n f
⊢ ContDiff 𝕜 (F := ℂ) n fun (x : E) ↦ Complex.exp (f x)

Tactic:
Complex.contDiff_exp.comp h

Premises used: Complex.contDiff_exp, ContDiff.comp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt 𝕜 (F := ℂ) n (fun (x : E) ↦ Complex.exp (f x)) x

Tactic:
Complex.contDiff_exp.contDiffAt.comp x hf

Premises used: Complex.contDiff_exp, ContDiffAt.comp, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
s : Set E
n : WithTop ℕ∞
hf : ContDiffOn 𝕜 n f s
⊢ ContDiffOn 𝕜 (F := ℂ) n (fun (x : E) ↦ Complex.exp (f x)) s

Tactic:
Complex.contDiff_exp.comp_contDiffOn hf

Premises used: ContDiff.comp_contDiffOn, Complex.contDiff_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra 𝕜 ℂ
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : E → ℂ
x : E
s : Set E
n : WithTop ℕ∞
hf : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt 𝕜 (F := ℂ) n (fun (x : E) ↦ Complex.exp (f x)) s x

Tactic:
Complex.contDiff_exp.contDiffAt.comp_contDiffWithinAt x hf

Premises used: Complex.contDiff_exp, ContDiffAt.comp_contDiffWithinAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
n : ℕ
c : ℂ
rw : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ c ^ n * iteratedDeriv n cexp (c * x)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
rw₁ : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ c ^ n * deriv^[n] cexp (c * x)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
rw₂ rw₃ : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ c ^ n * cexp (c * x)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)
⊢ Eq (α := (x : ℂ) → ℂ) (iteratedDeriv n fun (s : ℂ) ↦ cexp (c * s)) fun (s : ℂ) ↦ c ^ n * cexp (c * s)

Tactic:
rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]

Premises used: iteratedDeriv_comp_const_mul, Complex.iter_deriv_exp, Complex.contDiff_exp, iteratedDeriv_eq_iterate
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
rw : AnalyticOnNhd ℝ (E := ℝ) NormedSpace.exp univ
⊢ AnalyticOnNhd ℝ rexp univ

Tactic:
rw [Real.exp_eq_exp_ℝ]

Premises used: Real.exp_eq_exp_ℝ
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
⊢ AnalyticOnNhd ℝ (E := ℝ) NormedSpace.exp univ

Tactic:
fun x _ ↦ NormedSpace.exp_analytic x

Premises used: AnalyticOnNhd, NormedSpace.exp_analytic
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
⊢ AnalyticOnNhd ℝ (E := ℝ) NormedSpace.exp univ

Tactic:
exact fun x _ ↦ NormedSpace.exp_analytic x

Premises used: NormedSpace.exp_analytic
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
⊢ AnalyticOn ℝ rexp univ

Tactic:
analyticOnNhd_rexp.analyticOn

Premises used: analyticOnNhd_rexp, AnalyticOnNhd.analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℝ
⊢ AnalyticAt ℝ rexp x

Tactic:
analyticOnNhd_rexp x (mem_univ _)

Premises used: analyticOnNhd_rexp, Set.mem_univ
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℝ
s : Set ℝ
⊢ AnalyticWithinAt ℝ rexp s x

Tactic:
analyticAt_rexp.analyticWithinAt

Premises used: analyticAt_rexp, AnalyticAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
fa : AnalyticAt ℝ f x
⊢ AnalyticAt ℝ (rexp ∘ f) x

Tactic:
analyticAt_rexp.comp fa

Premises used: analyticAt_rexp, AnalyticAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
fa : AnalyticAt ℝ f x
⊢ AnalyticAt ℝ (F := ℝ) (fun (z : E) ↦ rexp (f z)) x

Tactic:
fa.rexp

Premises used: AnalyticAt.rexp, Real.exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x : E
fa : AnalyticWithinAt ℝ f s x
⊢ AnalyticWithinAt ℝ (F := ℝ) (fun (z : E) ↦ rexp (f z)) s x

Tactic:
analyticAt_rexp.comp_analyticWithinAt fa

Premises used: AnalyticAt.comp_analyticWithinAt, analyticAt_rexp, Real.exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
fs : AnalyticOnNhd ℝ f s
⊢ AnalyticOnNhd ℝ (F := ℝ) (fun (z : E) ↦ rexp (f z)) s

Tactic:
fun z n ↦ analyticAt_rexp.comp (fs z n)

Premises used: analyticAt_rexp, AnalyticOnNhd, Real.exp, AnalyticAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
fs : AnalyticOn ℝ f s
⊢ AnalyticOn ℝ (F := ℝ) (fun (z : E) ↦ rexp (f z)) s

Tactic:
analyticOnNhd_rexp.comp_analyticOn fs (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, analyticOnNhd_rexp, Real.exp, AnalyticOnNhd.comp_analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℝ
⊢ HasStrictDerivAt rexp (rexp x) x

Tactic:
(Complex.hasStrictDerivAt_exp x).real_of_complex

Premises used: HasStrictDerivAt.real_of_complex, Real.exp, Complex.ofReal, Complex.hasStrictDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℝ
⊢ HasDerivAt rexp (rexp x) x

Tactic:
(Complex.hasDerivAt_exp x).real_of_complex

Premises used: Real.exp, Complex.ofReal, HasDerivAt.real_of_complex, Complex.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
n : WithTop ℕ∞
⊢ ContDiff ℝ n rexp

Tactic:
Complex.contDiff_exp.real_of_complex

Premises used: Real.exp, Complex.contDiff_exp, ContDiff.real_of_complex
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
⊢ Differentiable ℝ rexp

Tactic:
fun x => (hasDerivAt_exp x).differentiableAt

Premises used: Differentiable, HasDerivAt.differentiableAt, Real.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
x : ℝ
⊢ DifferentiableAt ℝ rexp x

Tactic:
differentiable_exp x

Premises used: Real.differentiable_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
⊢ deriv rexp = rexp

Tactic:
funext fun x => (hasDerivAt_exp x).deriv

Premises used: HasDerivAt.deriv, funext, Real.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
n : ℕ
rw : deriv^[n] (deriv rexp) = rexp
rw₁ : deriv^[n] rexp = rexp
rw₂ rw₃ : rexp = rexp
⊢ deriv^[n + 1] rexp = rexp

Tactic:
rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]

Premises used: Real.deriv_exp, Function.iterate_succ_apply
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
f : ℝ → ℝ
f' x : ℝ
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ Real.exp (f x)) (Real.exp (f x) * f') x

Tactic:
(Real.hasStrictDerivAt_exp (f x)).comp x hf

Premises used: Real.exp, HasStrictDerivAt.comp, Real.hasStrictDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : ℝ) ↦ Real.exp (f x)) (Real.exp (f x) * f') x

Tactic:
(Real.hasDerivAt_exp (f x)).comp x hf

Premises used: HasDerivAt.comp, Real.exp, Real.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
f : ℝ → ℝ
f' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ Real.exp (f x)) (Real.exp (f x) * f') s x

Tactic:
(Real.hasDerivAt_exp (f x)).comp_hasDerivWithinAt x hf

Premises used: Real.exp, HasDerivAt.comp_hasDerivWithinAt, Real.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
hf : DifferentiableWithinAt ℝ f s x
hxs : UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun (x : ℝ) ↦ Real.exp (f x)) s x = Real.exp (f x) * derivWithin f s x

Tactic:
hf.hasDerivWithinAt.exp.derivWithin hxs

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
f : ℝ → ℝ
x : ℝ
hc : DifferentiableAt ℝ f x
⊢ deriv (fun (x : ℝ) ↦ Real.exp (f x)) x = Real.exp (f x) * deriv f x

Tactic:
hc.hasDerivAt.exp.deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
n : ℕ∞ω
hf : ContDiff ℝ n f
⊢ ContDiff ℝ (F := ℝ) n fun (x : E) ↦ Real.exp (f x)

Tactic:
Real.contDiff_exp.comp hf

Premises used: Real.exp, ContDiff.comp, Real.contDiff_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ Real.exp (f x)) x

Tactic:
Real.contDiff_exp.contDiffAt.comp x hf

Premises used: Real.exp, ContDiffAt.comp, Real.contDiff_exp, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
⊢ ContDiffOn ℝ (F := ℝ) n (fun (x : E) ↦ Real.exp (f x)) s

Tactic:
Real.contDiff_exp.comp_contDiffOn hf

Premises used: ContDiff.comp_contDiffOn, Real.exp, Real.contDiff_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
s : Set E
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x : E) ↦ Real.exp (f x)) s x

Tactic:
Real.contDiff_exp.contDiffAt.comp_contDiffWithinAt x hf

Premises used: Real.exp, ContDiffAt.comp_contDiffWithinAt, Real.contDiff_exp, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ Real.exp (f x)) (Real.exp (f x) • f') s x

Tactic:
(Real.hasDerivAt_exp (f x)).comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, Real.exp, Real.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun (x : E) ↦ Real.exp (f x)) (Real.exp (f x) • f') x

Tactic:
(Real.hasDerivAt_exp (f x)).comp_hasFDerivAt x hf

Premises used: Real.exp, Real.hasDerivAt_exp, HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (fun (x : E) ↦ Real.exp (f x)) (Real.exp (f x) • f') x

Tactic:
(Real.hasStrictDerivAt_exp (f x)).comp_hasStrictFDerivAt x hf

Premises used: Real.exp, HasStrictDerivAt.comp_hasStrictFDerivAt, Real.hasStrictDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
s : Set E
hf : DifferentiableWithinAt ℝ f s x
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ Real.exp (f x)) s x

Tactic:
hf.hasFDerivWithinAt.exp.differentiableWithinAt

Premises used: HasFDerivWithinAt.exp, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hc : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ Real.exp (f x)) x

Tactic:
hc.hasFDerivAt.exp.differentiableAt

Premises used: HasFDerivAt.exp, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
hc : DifferentiableOn ℝ f s
⊢ DifferentiableOn ℝ (F := ℝ) (fun (x : E) ↦ Real.exp (f x)) s

Tactic:
fun x h => (hc x h).exp

Premises used: DifferentiableOn, DifferentiableWithinAt.exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
hc : Differentiable ℝ f
⊢ Differentiable ℝ (F := ℝ) fun (x : E) ↦ Real.exp (f x)

Tactic:
fun x => (hc x).exp

Premises used: Differentiable, DifferentiableAt.exp
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
s : Set E
hf : DifferentiableWithinAt ℝ f s x
hxs : UniqueDiffWithinAt ℝ s x
⊢ fderivWithin ℝ (fun (x : E) ↦ Real.exp (f x)) s x =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.exp (f x)) (fderivWithin ℝ f s x)

Tactic:
hf.hasFDerivWithinAt.exp.fderivWithin hxs

Premises used: HasFDerivWithinAt.exp, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hc : DifferentiableAt ℝ f x
⊢ fderiv ℝ (fun (x : E) ↦ Real.exp (f x)) x = HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.exp (f x)) (fderiv ℝ f x)

Tactic:
hc.hasFDerivAt.exp.fderiv

Premises used: HasFDerivAt.exp, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv
Goal:
n : ℕ
c : ℝ
rw : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ c ^ n * iteratedDeriv n rexp (c * x)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
rw₁ : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ c ^ n * deriv^[n] rexp (c * x)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
rw₂ rw₃ : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ c ^ n * rexp (c * x)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)
⊢ Eq (α := (x : ℝ) → ℝ) (iteratedDeriv n fun (s : ℝ) ↦ rexp (c * s)) fun (s : ℝ) ↦ c ^ n * rexp (c * s)

Tactic:
rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]

Premises used: iteratedDeriv_comp_const_mul, Real.iter_deriv_exp, iteratedDeriv_eq_iterate, Real.contDiff_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : CharZero 𝕂
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)
⊢ HasStrictFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) exp
    ((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸 : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ 𝔸) 𝔸) → 𝔸 →L[𝕂] 𝔸)
      (expSeries 𝕂 𝔸 1))
    0

Tactic:
(hasFPowerSeriesAt_exp_zero_of_radius_pos h).hasStrictFDerivAt

Premises used: NormedSpace.hasFPowerSeriesAt_exp_zero_of_radius_pos, HasFPowerSeriesAt.hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : CharZero 𝕂
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)
h₁ :
  Eq.{u_2 + 1} (α := AddCommGroup 𝔸) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module 𝕂 𝔸) (toModule : Module 𝕂 𝔸) (β := Module 𝕂 𝔸) (toModule : Module 𝕂 𝔸) →
      Eq (α := 𝔸 →L[𝕂] 𝔸) (1 : 𝔸 →L[𝕂] 𝔸)
        ((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸 : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ 𝔸) 𝔸) → 𝔸 →L[𝕂] 𝔸)
            (expSeries 𝕂 𝔸 1) :
          𝔸 →L[𝕂] 𝔸)
⊢ HasStrictFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) exp 1 0

Tactic:
convert! (hasFPowerSeriesAt_exp_zero_of_radius_pos h).hasStrictFDerivAt

Premises used: NormedSpace.hasFPowerSeriesAt_exp_zero_of_radius_pos, HasFPowerSeriesAt.hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedRing 𝔸
inst_2 : CharZero 𝕂
inst_3 : NormedAlgebra 𝕂 𝔸
inst_4 : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)
e_4 : Eq.{u_2 + 1} (α := AddCommGroup 𝔸) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module 𝕂 𝔸) (toModule : Module 𝕂 𝔸) (β := Module 𝕂 𝔸) (toModule : Module 𝕂 𝔸)
h₁ :
  ∀ (x : 𝔸),
    Eq (α := 𝔸) ((1 : (a : 𝔸) → 𝔸) x : 𝔸)
      ((((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸 : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ 𝔸) 𝔸) → 𝔸 →L[𝕂] 𝔸)
                (expSeries 𝕂 𝔸 1) :
              𝔸 →L[𝕂] 𝔸) :
            (a : 𝔸) → 𝔸)
          x :
        𝔸)
⊢ Eq (α := 𝔸 →L[𝕂] 𝔸) (1 : 𝔸 →L[𝕂] 𝔸)
    ((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸 : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ 𝔸) 𝔸) → 𝔸 →L[𝕂] 𝔸)
        (expSeries 𝕂 𝔸 1) :
      𝔸 →L[𝕂] 𝔸)

Tactic:
ext x