𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt htx
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h) =o[𝓝 0]
    fun h => h
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
rw [hasFDerivAt_iff_isLittleO_nhds_zero]
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (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
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h) =o[𝓝 0]
    fun h => h
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 _ _ _ _ _ _ _ _ (fun u => exp 𝕂 (u • x))
    ((1 : 𝕊 →L[𝕂] 𝕊).smulRight 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 hpos
  exact this.comp 0 ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).hasFDerivAt
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
⊢ (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
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (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
have : Tendsto (fun h : 𝕊 => h • x) (𝓝 0) (𝓝 0) := by
  rw [← zero_smul 𝕊 x]
  exact tendsto_id.smul_const x
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this✝ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (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
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
⊢ (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
have : ∀ᶠ h in 𝓝 (0 : 𝕊), h • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
  this.eventually (EMetric.ball_mem_nhds _ hpos)
case h
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this✝ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : 𝕊
hh : h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ 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
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this✝ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (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
filter_upwards [this] with h hh
case h
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this✝¹ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this✝ : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : 𝕊
hh : h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
this : Commute (t • x) (h • x)
⊢ 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
case h
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this✝ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : 𝕊
hh : h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ 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
have : Commute (t • x) (h • x) := ((Commute.refl x).smul_left t).smul_right h
no goals
case h
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this✝¹ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
this✝ : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : 𝕊
hh : h • x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
this : Commute (t • x) (h • x)
⊢ 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
rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
  ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply,
  ContinuousLinearMap.one_apply, smul_eq_mul, mul_sub_left_distrib, mul_sub_left_distrib, mul_one]
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
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
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
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
apply (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
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 (fun u => exp 𝕂 (u • x)) (ContinuousLinearMap.smulRight 1 x) 0
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
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
rw [← @hasFDerivAt_iff_isLittleO_nhds_zero _ _ _ _ _ _ _ _ (fun u => exp 𝕂 (u • x))
  ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x) 0]
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
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
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
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 (fun u => exp 𝕂 (u • x)) (ContinuousLinearMap.smulRight 1 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 hpos
no goals
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
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
exact this.comp 0 ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).hasFDerivAt
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
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
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
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)
rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul]
no goals
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
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
exact hasFDerivAt_exp_zero_of_radius_pos hpos
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ Tendsto (fun h => h • x) (𝓝 0) (𝓝 (0 • x))
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
rw [← zero_smul 𝕊 x]
no goals
𝕂 : Type u_3
𝕊 : Type u_2
𝔸 : Type u_1
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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ Tendsto (fun h => h • x) (𝓝 0) (𝓝 (0 • x))
exact tendsto_id.smul_const x