awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 𝕂 𝔸)
x : 𝔸
h₁ : x = (expSeries 𝕂 𝔸 1 : (a : (i : Fin 1) → 𝔸) → 𝔸) fun (x_1 : Fin 1) ↦ x
⊢ Eq (α := 𝔸) ((1 : (a : 𝔸) → 𝔸) x : 𝔸)
    ((((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸 : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ 𝔸) 𝔸) → 𝔸 →L[𝕂] 𝔸)
              (expSeries 𝕂 𝔸 1) :
            𝔸 →L[𝕂] 𝔸) :
          (a : 𝔸) → 𝔸)
        x :
      𝔸)

Tactic:
change x = expSeries 𝕂 𝔸 1 fun _ => x

Premises used: NormedSpace.expSeries, OfNat.ofNat, DFunLike.coe
-- 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 𝕂 𝔸)
x : 𝔸
⊢ x = (expSeries 𝕂 𝔸 1 : (a : (i : Fin 1) → 𝔸) → 𝔸) fun (x_1 : Fin 1) ↦ x

Tactic:
simp [expSeries_apply_eq, Nat.factorial]

Premises used: NormedSpace.expSeries_apply_eq, Nat.factorial
-- 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 𝕂 𝔸)
⊢ HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) exp 1 0

Tactic:
(hasStrictFDerivAt_exp_zero_of_radius_pos h).hasFDerivAt

Premises used: HasStrictFDerivAt.hasFDerivAt, hasStrictFDerivAt_exp_zero_of_radius_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
rw :
  IsLittleO (E := 𝔸) (F := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦
      HSub.hSub (β := 𝔸) (exp (x + h) - exp x) ((HSMul.hSMul (β := 𝔸 →L[𝕂] 𝔸) (exp x) 1 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ h
⊢ HasFDerivAt exp (HSMul.hSMul (β := 𝔸 →L[𝕂] 𝔸) (exp x) 1) x

Tactic:
rw [hasFDerivAt_iff_isLittleO_nhds_zero]

Premises used: hasFDerivAt_iff_isLittleO_nhds_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
this :
  EventuallyEq (β := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦ exp x * HSub.hSub (β := 𝔸) (exp (0 + h) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ exp (x + h) - exp x - HSMul.hSMul (β := 𝔸) (exp x) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸)
⊢ IsLittleO (E := 𝔸) (F := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦
      HSub.hSub (β := 𝔸) (exp (x + h) - exp x) ((HSMul.hSMul (β := 𝔸 →L[𝕂] 𝔸) (exp x) 1 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ h

Tactic:
(IsLittleO.const_mul_left ?_ _).congr' this (EventuallyEq.refl _ _)

Premises used: Asymptotics.IsLittleO.const_mul_left, Asymptotics.IsLittleO.congr', Filter.EventuallyEq.refl
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
this :
  EventuallyEq (β := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦ exp x * HSub.hSub (β := 𝔸) (exp (0 + h) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ exp (x + h) - exp x - HSMul.hSMul (β := 𝔸) (exp x) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸)
refine :
  IsLittleO (E := 𝔸) (F := 𝔸) (𝓝 0)
    (fun (x : 𝔸) ↦ HSub.hSub (β := 𝔸) (exp (0 + x) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) x : 𝔸))
    fun (h : 𝔸) ↦ h
⊢ IsLittleO (E := 𝔸) (F := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦
      HSub.hSub (β := 𝔸) (exp (x + h) - exp x) ((HSMul.hSMul (β := 𝔸 →L[𝕂] 𝔸) (exp x) 1 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ h

Tactic:
refine (IsLittleO.const_mul_left ?_ _).congr' this (EventuallyEq.refl _ _)

Premises used: Asymptotics.IsLittleO.const_mul_left, Asymptotics.IsLittleO.congr', Filter.EventuallyEq.refl
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
this :
  EventuallyEq (β := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦ exp x * HSub.hSub (β := 𝔸) (exp (0 + h) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ exp (x + h) - exp x - HSMul.hSMul (β := 𝔸) (exp x) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸)
rw : HasFDerivAt exp (ContinuousLinearMap.id 𝕂 𝔸) 0
⊢ IsLittleO (E := 𝔸) (F := 𝔸) (𝓝 0)
    (fun (x : 𝔸) ↦ HSub.hSub (β := 𝔸) (exp (0 + x) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) x : 𝔸))
    fun (h : 𝔸) ↦ h

Tactic:
rw [← hasFDerivAt_iff_isLittleO_nhds_zero]

Premises used: hasFDerivAt_iff_isLittleO_nhds_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
this :
  EventuallyEq (β := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦ exp x * HSub.hSub (β := 𝔸) (exp (0 + h) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ exp (x + h) - exp x - HSMul.hSMul (β := 𝔸) (exp x) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸)
⊢ HasFDerivAt exp (ContinuousLinearMap.id 𝕂 𝔸) 0

Tactic:
hasFDerivAt_exp_zero_of_radius_pos hx.pos

Premises used: LT.lt.pos, hasFDerivAt_exp_zero_of_radius_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
this :
  EventuallyEq (β := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦ exp x * HSub.hSub (β := 𝔸) (exp (0 + h) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ exp (x + h) - exp x - HSMul.hSMul (β := 𝔸) (exp x) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸)
⊢ HasFDerivAt exp (ContinuousLinearMap.id 𝕂 𝔸) 0

Tactic:
exact hasFDerivAt_exp_zero_of_radius_pos hx.pos

Premises used: LT.lt.pos, hasFDerivAt_exp_zero_of_radius_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
h :
  EventuallyEq (β := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦ exp x * HSub.hSub (β := 𝔸) (exp (0 + h) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ exp (x + h) - exp x - HSMul.hSMul (β := 𝔸) (exp x) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸)
⊢ IsLittleO (E := 𝔸) (F := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦
      HSub.hSub (β := 𝔸) (exp (x + h) - exp x) ((HSMul.hSMul (β := 𝔸 →L[𝕂] 𝔸) (exp x) 1 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ h

Tactic:
suffices
    (fun h => exp x * (exp (0 + h) - exp 0 - ContinuousLinearMap.id 𝕂 𝔸 h)) =ᶠ[𝓝 0] fun h =>
      exp (x + h) - exp x - exp x • ContinuousLinearMap.id 𝕂 𝔸 h by
    refine (IsLittleO.const_mul_left ?_ _).congr' this (EventuallyEq.refl _ _)
    rw [← hasFDerivAt_iff_isLittleO_nhds_zero]
    exact hasFDerivAt_exp_zero_of_radius_pos hx.pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ ∀ᶠ (h : 𝔸) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) h

Tactic:
have : ∀ᶠ h in 𝓝 (0 : 𝔸), h ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
    Metric.eball_mem_nhds _ hx.pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
this :
  ∀ᶠ (h : 𝔸) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) h
h :
  ∀ (a : 𝔸)
    (hh :
      Membership.mem (γ := Set 𝔸)
        (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) a),
    exp x * HSub.hSub (β := 𝔸) (exp (0 + a) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) a : 𝔸) =
      exp (x + a) - exp x - HSMul.hSMul (β := 𝔸) (exp x) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) a : 𝔸)
⊢ EventuallyEq (β := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦ exp x * HSub.hSub (β := 𝔸) (exp (0 + h) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ exp (x + h) - exp x - HSMul.hSMul (β := 𝔸) (exp x) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) h : 𝔸)

Tactic:
filter_upwards [this] with _ hh
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
this :
  ∀ᶠ (h : 𝔸) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) h
a : 𝔸
hh :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) a
h : exp x * (exp a - 1 - a) = exp x * exp a - exp x - exp x * a
⊢ exp x * HSub.hSub (β := 𝔸) (exp (0 + a) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) a : 𝔸) =
    exp (x + a) - exp x - HSMul.hSMul (β := 𝔸) (exp x) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) a : 𝔸)

Tactic:
rw [exp_add_of_mem_ball hx hh, exp_zero, zero_add, ContinuousLinearMap.id_apply, smul_eq_mul]

Premises used: ContinuousLinearMap.id_apply, zero_add, NormedSpace.exp_zero, smul_eq_mul, NormedSpace.exp_add_of_mem_ball
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
this :
  ∀ᶠ (h : 𝔸) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) h
a : 𝔸
hh :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) a
⊢ exp x * (exp a - 1 - a) = exp x * exp a - exp x - exp x * a

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
inst_4 : CharZero 𝕂
x : 𝔸
hx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) x
⊢ HasStrictFDerivAt exp (HSMul.hSMul (β := 𝔸 →L[𝕂] 𝔸) (exp x) 1) x

Tactic:
let ⟨_, hp⟩ := analyticAt_exp_of_mem_ball x hx
  hp.hasFDerivAt.unique (hasFDerivAt_exp_of_mem_ball hx) ▸ hp.hasStrictFDerivAt

Premises used: NormedSpace.exp, NormedSpace.analyticAt_exp_of_mem_ball, Eq.rec, HasFPowerSeriesAt.hasFDerivAt, HasStrictFDerivAt, _private.0.hasStrictFDerivAt_exp_of_mem_ball.match_1, HSMul.hSMul, HasFDerivAt.unique, OfNat.ofNat, HasFPowerSeriesAt.hasStrictFDerivAt, hasFDerivAt_exp_of_mem_ball
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
inst : NontriviallyNormedField 𝕂
inst_1 : CompleteSpace 𝕂
inst_2 : CharZero 𝕂
x : 𝕂
hx :
  Membership.mem (γ := Set 𝕂)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕂) (E := 𝕂) (F := 𝕂) (expSeries 𝕂 𝕂))) x
⊢ HasStrictDerivAt exp (exp x) x

Tactic:
simpa using (hasStrictFDerivAt_exp_of_mem_ball hx).hasStrictDerivAt

Premises used: hasStrictFDerivAt_exp_of_mem_ball, HasStrictFDerivAt.hasStrictDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
inst : NontriviallyNormedField 𝕂
inst_1 : CompleteSpace 𝕂
inst_2 : CharZero 𝕂
x : 𝕂
hx :
  Membership.mem (γ := Set 𝕂)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕂) (E := 𝕂) (F := 𝕂) (expSeries 𝕂 𝕂))) x
⊢ HasDerivAt exp (exp x) x

Tactic:
(hasStrictDerivAt_exp_of_mem_ball hx).hasDerivAt

Premises used: HasStrictDerivAt.hasDerivAt, hasStrictDerivAt_exp_of_mem_ball
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
inst : NontriviallyNormedField 𝕂
inst_1 : CompleteSpace 𝕂
inst_2 : CharZero 𝕂
h : 0 < FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕂) (E := 𝕂) (F := 𝕂) (expSeries 𝕂 𝕂)
⊢ HasStrictDerivAt.{u_1, u_1} (𝕜 := 𝕂) exp 1 0

Tactic:
(hasStrictFDerivAt_exp_zero_of_radius_pos h).hasStrictDerivAt

Premises used: hasStrictFDerivAt_exp_zero_of_radius_pos, HasStrictFDerivAt.hasStrictDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
inst : NontriviallyNormedField 𝕂
inst_1 : CompleteSpace 𝕂
inst_2 : CharZero 𝕂
h : 0 < FormalMultilinearSeries.radius.{u_1, u_1, u_1} (𝕜 := 𝕂) (E := 𝕂) (F := 𝕂) (expSeries 𝕂 𝕂)
⊢ HasDerivAt.{u_1, u_1} (𝕜 := 𝕂) exp 1 0

Tactic:
(hasStrictDerivAt_exp_zero_of_radius_pos h).hasDerivAt

Premises used: HasStrictDerivAt.hasDerivAt, hasStrictDerivAt_exp_zero_of_radius_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
⊢ HasStrictFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) exp 1 0

Tactic:
hasStrictFDerivAt_exp_zero_of_radius_pos (expSeries_radius_pos 𝕂 𝔸)

Premises used: hasStrictFDerivAt_exp_zero_of_radius_pos, NormedSpace.expSeries_radius_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
⊢ HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) exp 1 0

Tactic:
hasStrictFDerivAt_exp_zero.hasFDerivAt

Premises used: HasStrictFDerivAt.hasFDerivAt, hasStrictFDerivAt_exp_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
x : 𝔸
⊢ HasStrictFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕂) exp (HSMul.hSMul (β := 𝔸 →L[𝕂] 𝔸) (exp x) 1) x

Tactic:
hasStrictFDerivAt_exp_of_mem_ball ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

Premises used: hasStrictFDerivAt_exp_of_mem_ball, Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : RCLike 𝕂
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
inst_3 : CompleteSpace 𝔸
x : 𝔸
⊢ HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕂) exp (HSMul.hSMul (β := 𝔸 →L[𝕂] 𝔸) (exp x) 1) x

Tactic:
hasStrictFDerivAt_exp.hasFDerivAt

Premises used: hasStrictFDerivAt_exp, HasStrictFDerivAt.hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
x : 𝕂
⊢ HasStrictDerivAt exp (exp x) x

Tactic:
hasStrictDerivAt_exp_of_mem_ball ((expSeries_radius_eq_top 𝕂 𝕂).symm ▸ edist_lt_top _ _)

Premises used: Eq.rec, NormedSpace.expSeries_radius_eq_top, edist_lt_top, hasStrictDerivAt_exp_of_mem_ball, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
x : 𝕂
⊢ HasDerivAt exp (exp x) x

Tactic:
hasStrictDerivAt_exp.hasDerivAt

Premises used: HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
⊢ HasStrictDerivAt.{u_1, u_1} (𝕜 := 𝕂) exp 1 0

Tactic:
hasStrictDerivAt_exp_zero_of_radius_pos (expSeries_radius_pos 𝕂 𝕂)

Premises used: hasStrictDerivAt_exp_zero_of_radius_pos, NormedSpace.expSeries_radius_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
⊢ HasDerivAt.{u_1, u_1} (𝕜 := 𝕂) exp 1 0

Tactic:
hasStrictDerivAt_exp_zero.hasDerivAt

Premises used: HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
⊢ cexp = NormedSpace.exp

Tactic:
funext fun x => ?_

Premises used: funext
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
refine : ∀ (x : ℂ), cexp x = NormedSpace.exp x
⊢ cexp = NormedSpace.exp

Tactic:
refine funext fun x => ?_

Premises used: funext
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
x : ℂ
rw : (exp' x).lim = (fun (x : ℂ) ↦ (∑' (n : ℕ), x ^ n / (↑n ! : ℂ) : ℂ)) x
⊢ cexp x = NormedSpace.exp x

Tactic:
rw [Complex.exp, exp_eq_tsum_div]

Premises used: NormedSpace.exp_eq_tsum_div, Complex.exp
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
x : ℂ
⊢ (exp' x).lim = (fun (x : ℂ) ↦ (∑' (n : ℕ), x ^ n / (↑n ! : ℂ) : ℂ)) x

Tactic:
tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable x).hasSum.tendsto_sum_nat

Premises used: HasSum.tendsto_sum_nat, Complex.exp', NormedSpace.expSeries_div_summable, CauSeq.tendsto_limit, Summable.hasSum, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
x : ℂ
⊢ (exp' x).lim = (fun (x : ℂ) ↦ (∑' (n : ℕ), x ^ n / (↑n ! : ℂ) : ℂ)) x

Tactic:
exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable x).hasSum.tendsto_sum_nat

Premises used: HasSum.tendsto_sum_nat, Complex.exp', NormedSpace.expSeries_div_summable, CauSeq.tendsto_limit, Summable.hasSum, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
h : ∀ (x : ℝ), rexp x = NormedSpace.exp x
⊢ rexp = NormedSpace.exp

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
x : ℝ
⊢ rexp x = NormedSpace.exp x

Tactic:
mod_cast congr_fun Complex.exp_eq_exp_ℂ x

Premises used: Complex.exp_eq_exp_ℂ, Complex.ofReal_exp._simp_1, congrArg, cast, Complex.ofReal, congr, congr_fun, NormedSpace.ofReal_exp_ℝ_ℝ._simp_1, Eq, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
x : ℝ
⊢ rexp x = NormedSpace.exp x

Tactic:
exact mod_cast congr_fun Complex.exp_eq_exp_ℂ x

Premises used: Complex.exp_eq_exp_ℂ, Complex.ofReal, congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
rw :
  IsLittleO.{u_2, u_3, u_2} (E := 𝔸) (F := 𝕊) (𝓝 0)
    (fun (h : 𝕊) ↦
      HSub.hSub (β := 𝔸) (exp ((t + h) • x) - exp (t • x))
        ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸))
    fun (h : 𝕊) ↦ h
⊢ HasFDerivAt (fun (u : 𝕊) ↦ exp (u • x))
    (HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)) t

Tactic:
rw [hasFDerivAt_iff_isLittleO_nhds_zero]

Premises used: hasFDerivAt_iff_isLittleO_nhds_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exponential
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
this :
  EventuallyEq.{u_2, u_3} (β := 𝔸) (𝓝 0)
    (fun (h : 𝕊) ↦
      exp (t • x) *
        HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
          ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸))
    fun (h : 𝕊) ↦
    HSub.hSub (β := 𝔸) (exp ((t + h) • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
apply :
  IsLittleO.{u_2, u_3, u_2} (E := 𝔸) (F := 𝕊) (𝓝 0)
    (fun (x_1 : 𝕊) ↦
      HSub.hSub (β := 𝔸) (exp ((0 + x_1) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) x_1 : 𝔸))
    fun (h : 𝕊) ↦ h
⊢ IsLittleO.{u_2, u_3, u_2} (E := 𝔸) (F := 𝕊) (𝓝 0)
    (fun (h : 𝕊) ↦
      HSub.hSub (β := 𝔸) (exp ((t + h) • x) - exp (t • x))
        ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸))
    fun (h : 𝕊) ↦ h

Tactic:
apply (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)

Premises used: Asymptotics.IsLittleO.const_mul_left, Asymptotics.IsLittleO.congr', Filter.EventuallyEq.refl