awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 𝔸)
rw : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) 0
⊢ 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:
rw [← hasFDerivAt_iff_isLittleO_nhds_zero (f := fun u => exp (u • x))
      (f' := (1 : 𝕊 →L[𝕂] 𝕊).smulRight x) (x := 0)]

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 : 𝔸)
rw : HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) exp 1 0
⊢ HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (exp : (x : 𝔸) → 𝔸) (1 : 𝔸 →L[𝕂] 𝔸)
    ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) 0 : 𝔸)

Tactic:
rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul]

Premises used: ContinuousLinearMap.one_apply, zero_smul, ContinuousLinearMap.smulRight_apply
-- 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 : 𝔸)
⊢ HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) exp 1 0

Tactic:
hasFDerivAt_exp_zero_of_radius_pos htx.pos

Premises used: LT.lt.pos, hasFDerivAt_exp_zero_of_radius_pos
-- 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 : 𝔸)
⊢ HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) exp 1 0

Tactic:
exact hasFDerivAt_exp_zero_of_radius_pos htx.pos

Premises used: LT.lt.pos, hasFDerivAt_exp_zero_of_radius_pos
-- 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 : 𝔸)
⊢ 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
-- 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_1 :
  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 : 𝔸)
this :
  HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (exp : (x : 𝔸) → 𝔸) (1 : 𝔸 →L[𝕂] 𝔸)
    ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) 0 : 𝔸)
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) 0

Tactic:
this.comp 0 ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).hasFDerivAt

Premises used: ContinuousLinearMap.hasFDerivAt, ContinuousLinearMap.smulRight, LinearMap.smulRight, OfNat.ofNat, HasFDerivAt.comp
-- 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_1 :
  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 : 𝔸)
this :
  HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (exp : (x : 𝔸) → 𝔸) (1 : 𝔸 →L[𝕂] 𝔸)
    ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) 0 : 𝔸)
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) 0

Tactic:
exact this.comp 0 ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).hasFDerivAt

Premises used: ContinuousLinearMap.hasFDerivAt, ContinuousLinearMap.smulRight, OfNat.ofNat, HasFDerivAt.comp
-- 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)
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 : 𝔸)
⊢ 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:
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
-- 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 : Tendsto (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
⊢ Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)

Tactic:
rw [← zero_smul 𝕊 x]

Premises used: zero_smul
-- 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)
⊢ Tendsto (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))

Tactic:
tendsto_id.smul_const x

Premises used: Filter.tendsto_id, Filter.Tendsto.smul_const
-- 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)
⊢ Tendsto (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))

Tactic:
exact tendsto_id.smul_const x

Premises used: Filter.tendsto_id, Filter.Tendsto.smul_const
-- 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)
⊢ 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
-- 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 : Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (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)
-- 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_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)
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 : 𝔸)
⊢ 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:
filter_upwards [this] with h hh
-- 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_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)
h : 𝕊
hh :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (h • x)
⊢ Commute (t • x) (h • x)

Tactic:
have : Commute (t • x) (h • x) := ((Commute.refl x).smul_left t).smul_right h
-- 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)
⊢ HasFDerivAt (fun (u : 𝕊) ↦ exp (u • x))
    (HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)) t

Tactic:
hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx

Premises used: hasFDerivAt_exp_smul_const_of_mem_ball
-- 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)
h :
  ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) =
    HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) (fun (u : 𝕊) ↦ exp (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x))) t

Tactic:
convert! hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1

Premises used: hasFDerivAt_exp_smul_const_of_mem_ball
-- 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)
h :
  ∀ (t' : 𝕊),
    Eq.{u_3 + 1} (α := 𝔸)
      ((ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) : (a : 𝕊) → 𝔸) t' : 𝔸)
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) t' : 𝔸)
⊢ ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) =
    HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x)

Tactic:
ext t'
-- 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)
t' : 𝕊
h : Commute (t' • x) (exp (t • x))
⊢ Eq.{u_3 + 1} (α := 𝔸)
    ((ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) (exp (t • x)) : (a : 𝕊) → 𝔸) t' : 𝔸)
    ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) t' : 𝔸)

Tactic:
change Commute (t' • x) (exp (t • x))

Premises used: NormedSpace.exp, Commute, HSMul.hSMul
-- 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)
t' : 𝕊
⊢ Commute (t' • x) (exp (t • x))

Tactic:
(((Commute.refl x).smul_left t').smul_right t).exp_right

Premises used: Commute.exp_right, Commute.smul_left, Commute.smul_right, Commute.refl
-- 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)
t' : 𝕊
⊢ Commute (t' • x) (exp (t • x))

Tactic:
exact (((Commute.refl x).smul_left t').smul_right t).exp_right

Premises used: Commute.exp_right, Commute.smul_left, Commute.smul_right, Commute.refl