-- Mathlib/Analysis/SpecialFunctions/Exponential.lean
theorem hasFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕊)
    (htx : t • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasFDerivAt (fun u : 𝕊 => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smulRight x) t

Proof state:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ (fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h) =o[𝓝 0]
    fun h => h

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

Result:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ (fun x_1 => exp 𝕂 ((0 + x_1) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) x_1) =o[𝓝 0] fun h => h

Proof state:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this✝ :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
this : HasFDerivAt (exp 𝕂) 1 ((ContinuousLinearMap.smulRight 1 x) 0)
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (ContinuousLinearMap.smulRight 1 x) 0

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

Result:
no goals

Proof state:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this✝ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h

Tactic:
filter_upwards [this] with h hh

Result:
case h
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this✝ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
h : 𝕊
hh : h • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h) =
    exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h

Proof state:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ HasFDerivAt (exp 𝕂) 1 ((ContinuousLinearMap.smulRight 1 x) 0)

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

Result:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this :
  (fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0]
    fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
⊢ HasFDerivAt (exp 𝕂) 1 0

Proof state:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
⊢ Tendsto (fun h => h • x) (𝓝 0) (𝓝 (0 • x))

Tactic:
exact tendsto_id.smul_const x

Result:
no goals