awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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 𝕂 𝔸)
⊢ Eq (α := 𝔸 →L[𝕂] 𝔸) (1 : 𝔸 →L[𝕂] 𝔸)
    ((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸 : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ 𝔸) 𝔸) → 𝔸 →L[𝕂] 𝔸)
        (expSeries 𝕂 𝔸 1) :
      𝔸 →L[𝕂] 𝔸)
have h₁ : ∀ (x : 𝔸),
  Eq (α := 𝔸) ((1 : (a : 𝔸) → 𝔸) x : 𝔸)
    ((((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸 : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ 𝔸) 𝔸) → 𝔸 →L[𝕂] 𝔸)
              (expSeries 𝕂 𝔸 1) :
            𝔸 →L[𝕂] 𝔸) :
          (a : 𝔸) → 𝔸)
        x :
      𝔸)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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 : 𝔸
⊢ Eq (α := 𝔸) ((1 : (a : 𝔸) → 𝔸) x : 𝔸)
    ((((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸 : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ 𝔸) 𝔸) → 𝔸 →L[𝕂] 𝔸)
              (expSeries 𝕂 𝔸 1) :
            𝔸 →L[𝕂] 𝔸) :
          (a : 𝔸) → 𝔸)
        x :
      𝔸)
have h₁ : x = (expSeries 𝕂 𝔸 1 : (a : (i : Fin 1) → 𝔸) → 𝔸) fun (x_1 : Fin 1) ↦ x
Tactic: change x = expSeries 𝕂 𝔸 1 fun _ => x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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
⊢ HasFDerivAt exp (HSMul.hSMul (β := 𝔸 →L[𝕂] 𝔸) (exp x) 1) x
have 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
Tactic: rw [hasFDerivAt_iff_isLittleO_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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
have refine : IsLittleO (E := 𝔸) (F := 𝔸) (𝓝 0)
  (fun (x : 𝔸) ↦ HSub.hSub (β := 𝔸) (exp (0 + x) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) x : 𝔸))
  fun (h : 𝔸) ↦ h
Tactic: refine (IsLittleO.const_mul_left ?_ _).congr' this (EventuallyEq.refl _ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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 (x : 𝔸) ↦ HSub.hSub (β := 𝔸) (exp (0 + x) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) x : 𝔸))
    fun (h : 𝔸) ↦ h
have rw : HasFDerivAt exp (ContinuousLinearMap.id 𝕂 𝔸) 0
Tactic: rw [← hasFDerivAt_iff_isLittleO_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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
⊢ IsLittleO (E := 𝔸) (F := 𝔸) (𝓝 0)
    (fun (h : 𝔸) ↦
      HSub.hSub (β := 𝔸) (exp (x + h) - exp x) ((HSMul.hSMul (β := 𝔸 →L[𝕂] 𝔸) (exp x) 1 : (a : 𝔸) → 𝔸) h : 𝔸))
    fun (h : 𝔸) ↦ h
have 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 : 𝔸)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (hypothesis)
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
⊢ 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 : 𝔸)
have this : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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
⊢ 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 : 𝔸)
have 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 : 𝔸)
Tactic: filter_upwards [this] with _ hh
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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 * HSub.hSub (β := 𝔸) (exp (0 + a) - exp 0) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) a : 𝔸) =
    exp (x + a) - exp x - HSMul.hSMul (β := 𝔸) (exp x) ((ContinuousLinearMap.id 𝕂 𝔸 : (a : 𝔸) → 𝔸) a : 𝔸)
have h : exp x * (exp a - 1 - a) = exp x * exp a - exp x - exp x * a
Tactic: rw [exp_add_of_mem_ball hx hh, exp_zero, zero_add, ContinuousLinearMap.id_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
Goal:
⊢ cexp = NormedSpace.exp
have refine : ∀ (x : ℂ), cexp x = NormedSpace.exp x
Tactic: refine funext fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
Goal:
x : ℂ
⊢ cexp x = NormedSpace.exp x
have rw : (exp' x).lim = (fun (x : ℂ) ↦ (∑' (n : ℕ), x ^ n / (↑n ! : ℂ) : ℂ)) x
Tactic: rw [Complex.exp, exp_eq_tsum_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
Goal:
⊢ rexp = NormedSpace.exp
have h : ∀ (x : ℝ), rexp x = NormedSpace.exp x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
⊢ HasFDerivAt (fun (u : 𝕊) ↦ exp (u • x))
    (HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)) t
have 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
Tactic: rw [hasFDerivAt_iff_isLittleO_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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 : 𝔸)
⊢ 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
have 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
Tactic: apply (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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 : 𝔸)
⊢ 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
have rw : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) 0
Tactic: rw [← hasFDerivAt_iff_isLittleO_nhds_zero (f := fun u => exp (u • x))
      (f' := (1 : 𝕊 →L[𝕂] 𝕊).smulRight x) (x := 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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 : 𝔸)
⊢ HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (exp : (x : 𝔸) → 𝔸) (1 : 𝔸 →L[𝕂] 𝔸)
    ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) 0 : 𝔸)
have rw : HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) exp 1 0
Tactic: rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (hypothesis)
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 : 𝔸)
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) 0
have this₁ : HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (exp : (x : 𝔸) → 𝔸) (1 : 𝔸 →L[𝕂] 𝔸)
  ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) 0 : 𝔸)
Tactic: have : HasFDerivAt exp (1 : 𝔸 →L[𝕂] 𝔸) ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x 0) := by
      rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul]
      exact hasFDerivAt_exp_zero_of_radius_pos htx.pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
⊢ 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
have suffices : 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 : 𝔸)
Tactic: suffices (fun (h : 𝕊) => exp (t • x) *
      (exp ((0 + h) • x) - exp ((0 : 𝕊) • x) - ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x) h)) =ᶠ[𝓝 0]
        fun h =>
          exp ((t + h) • x) - exp (t • x) - (exp (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smulRight x) h by
    apply (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)
    rw [← hasFDerivAt_iff_isLittleO_nhds_zero (f := fun u => exp (u • x))
      (f' := (1 : 𝕊 →L[𝕂] 𝕊).smulRight x) (x := 0)]
    have : HasFDerivAt exp (1 : 𝔸 →L[𝕂] 𝔸) ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x 0) := by
      rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul]
      exact hasFDerivAt_exp_zero_of_radius_pos htx.pos
    exact this.comp 0 ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).hasFDerivAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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)
⊢ Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
have rw : Tendsto (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
Tactic: rw [← zero_smul 𝕊 x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (hypothesis)
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)
⊢ 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 : 𝔸)
have this : Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
Tactic: have : Tendsto (fun h : 𝕊 => h • x) (𝓝 0) (𝓝 0) := by
    rw [← zero_smul 𝕊 x]
    exact tendsto_id.smul_const x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (hypothesis)
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 : Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
⊢ 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 : 𝔸)
have this₁ : ∀ᶠ (h : 𝕊) in 𝓝 0,
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (h • x)
Tactic: have : ∀ᶠ h in 𝓝 (0 : 𝕊), h • x ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
    this.eventually (Metric.eball_mem_nhds _ htx.pos)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
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_1 : Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
this :
  ∀ᶠ (h : 𝕊) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
      (h • x)
⊢ 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 : 𝔸)
have h : ∀ (h : 𝕊)
  (hh :
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
      (h • x)),
  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 : 𝔸) =
    HSub.hSub (β := 𝔸) (exp ((t + h) • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
Tactic: filter_upwards [this] with h hh