𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ HasFDerivAt (exp 𝕂) (exp 𝕂 x • 1) x
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasFDerivAt (exp 𝕂) (exp 𝕂 x • 1) x
have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt hx
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (fun h => exp 𝕂 (x + h) - exp 𝕂 x - ↑(exp 𝕂 x • 1) h) =o[𝓝 0] fun h => h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ HasFDerivAt (exp 𝕂) (exp 𝕂 x • 1) x
rw [hasFDerivAt_iff_isLittleO_nhds_zero]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (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
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (fun h => exp 𝕂 (x + h) - exp 𝕂 x - ↑(exp 𝕂 x • 1) h) =o[𝓝 0] fun h => h
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 hpos
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (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
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ (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
have : ∀ᶠ h in 𝓝 (0 : 𝔸), h ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
  EMetric.ball_mem_nhds _ hpos
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
a✝ : 𝔸
hh : a✝ ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 x * (exp 𝕂 (0 + a✝) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) a✝) =
    exp 𝕂 (x + a✝) - exp 𝕂 x - exp 𝕂 x • ↑(ContinuousLinearMap.id 𝕂 𝔸) a✝
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (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
filter_upwards [this] with _ hh
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
a✝ : 𝔸
hh : a✝ ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 x * (exp 𝕂 a✝ - 1 - a✝) = exp 𝕂 x * exp 𝕂 a✝ - exp 𝕂 x - exp 𝕂 x * a✝
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
a✝ : 𝔸
hh : a✝ ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 x * (exp 𝕂 (0 + a✝) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) a✝) =
    exp 𝕂 (x + a✝) - exp 𝕂 x - exp 𝕂 x • ↑(ContinuousLinearMap.id 𝕂 𝔸) a✝
rw [exp_add_of_mem_ball hx hh, exp_zero, zero_add, ContinuousLinearMap.id_apply, smul_eq_mul]
no goals
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
a✝ : 𝔸
hh : a✝ ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ exp 𝕂 x * (exp 𝕂 a✝ - 1 - a✝) = exp 𝕂 x * exp 𝕂 a✝ - exp 𝕂 x - exp 𝕂 x * a✝
ring
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (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
⊢ (fun x => exp 𝕂 (0 + x) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) x) =o[𝓝 0] fun h => h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (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
⊢ (fun h => exp 𝕂 (x + h) - exp 𝕂 x - ↑(exp 𝕂 x • 1) h) =o[𝓝 0] fun h => h
refine' (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (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
⊢ HasFDerivAt (exp 𝕂) (ContinuousLinearMap.id 𝕂 𝔸) 0
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (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
⊢ (fun x => exp 𝕂 (0 + x) - exp 𝕂 0 - ↑(ContinuousLinearMap.id 𝕂 𝔸) x) =o[𝓝 0] fun h => h
rw [← hasFDerivAt_iff_isLittleO_nhds_zero]
no goals
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
this :
  (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
⊢ HasFDerivAt (exp 𝕂) (ContinuousLinearMap.id 𝕂 𝔸) 0
exact hasFDerivAt_exp_zero_of_radius_pos hpos