[GOAL]
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ HasStrictFDerivAt (exp 𝕂) 1 0
[PROOFSTEP]
convert (hasFPowerSeriesAt_exp_zero_of_radius_pos h).hasStrictFDerivAt
[GOAL]
case h.e'_10
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ 1 = ↑(continuousMultilinearCurryFin1 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 1)
[PROOFSTEP]
ext x
[GOAL]
case h.e'_10.h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
x : 𝔸
⊢ ↑1 x = ↑(↑(continuousMultilinearCurryFin1 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 1)) x
[PROOFSTEP]
change x = expSeries 𝕂 𝔸 1 fun _ => x
[GOAL]
case h.e'_10.h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
x : 𝔸
⊢ x = ↑(expSeries 𝕂 𝔸 1) fun x_1 => x
[PROOFSTEP]
simp [expSeries_apply_eq]
[GOAL]
𝕂 : 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
[PROOFSTEP]
have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt hx
[GOAL]
𝕂 : 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
[PROOFSTEP]
rw [hasFDerivAt_iff_isLittleO_nhds_zero]
[GOAL]
𝕂 : 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
[PROOFSTEP]
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
[GOAL]
𝕂 : 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
[PROOFSTEP]
refine' (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)
[GOAL]
𝕂 : 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
[PROOFSTEP]
rw [← hasFDerivAt_iff_isLittleO_nhds_zero]
[GOAL]
𝕂 : 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
[PROOFSTEP]
exact hasFDerivAt_exp_zero_of_radius_pos hpos
[GOAL]
𝕂 : 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
[PROOFSTEP]
have : ∀ᶠ h in 𝓝 (0 : 𝔸), h ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := EMetric.ball_mem_nhds _ hpos
[GOAL]
𝕂 : 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
[PROOFSTEP]
filter_upwards [this] with _ hh
[GOAL]
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✝
[PROOFSTEP]
rw [exp_add_of_mem_ball hx hh, exp_zero, zero_add, ContinuousLinearMap.id_apply, smul_eq_mul]
[GOAL]
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✝
[PROOFSTEP]
ring
[GOAL]
𝕂 : Type u_1
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : CompleteSpace 𝕂
inst✝ : CharZero 𝕂
x : 𝕂
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝕂))
⊢ HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x
[PROOFSTEP]
simpa using (hasStrictFDerivAt_exp_of_mem_ball hx).hasStrictDerivAt
[GOAL]
⊢ exp = _root_.exp ℂ
[PROOFSTEP]
refine' funext fun x => _
[GOAL]
x : ℂ
⊢ exp x = _root_.exp ℂ x
[PROOFSTEP]
rw [Complex.exp, exp_eq_tsum_div]
[GOAL]
x : ℂ
⊢ CauSeq.lim (exp' x) = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
[PROOFSTEP]
have : CauSeq.IsComplete ℂ norm := Complex.instIsComplete
[GOAL]
x : ℂ
this : CauSeq.IsComplete ℂ norm
⊢ CauSeq.lim (exp' x) = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
[PROOFSTEP]
exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable ℝ x).hasSum.tendsto_sum_nat
[GOAL]
⊢ exp = _root_.exp ℝ
[PROOFSTEP]
ext x
[GOAL]
case h
x : ℝ
⊢ exp x = _root_.exp ℝ x
[PROOFSTEP]
exact_mod_cast congr_fun Complex.exp_eq_exp_ℂ x
[GOAL]
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
[PROOFSTEP]
have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt htx
[GOAL]
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
[PROOFSTEP]
rw [hasFDerivAt_iff_isLittleO_nhds_zero]
[GOAL]
𝕂 : 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 (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
[PROOFSTEP]
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
[GOAL]
𝕂 : 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 (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
[PROOFSTEP]
apply (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _)
[GOAL]
𝕂 : 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 (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
[PROOFSTEP]
rw [← @hasFDerivAt_iff_isLittleO_nhds_zero _ _ _ _ _ _ _ _ (fun u => exp 𝕂 (u • x)) ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x) 0]
[GOAL]
𝕂 : 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 (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
[PROOFSTEP]
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
[GOAL]
𝕂 : 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 (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)
[PROOFSTEP]
rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul]
[GOAL]
𝕂 : 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 (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
[PROOFSTEP]
exact hasFDerivAt_exp_zero_of_radius_pos hpos
[GOAL]
𝕂 : 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 (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
[PROOFSTEP]
exact this.comp 0 ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).hasFDerivAt
[GOAL]
𝕂 : 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 (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
[PROOFSTEP]
have : Tendsto (fun h : 𝕊 => h • x) (𝓝 0) (𝓝 0) :=
  by
  rw [← zero_smul 𝕊 x]
  exact tendsto_id.smul_const x
[GOAL]
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)
[PROOFSTEP]
rw [← zero_smul 𝕊 x]
[GOAL]
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
hpos : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ Tendsto (fun h => h • x) (𝓝 0) (𝓝 (0 • x))
[PROOFSTEP]
exact tendsto_id.smul_const x
[GOAL]
𝕂 : 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 (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
[PROOFSTEP]
have : ∀ᶠ h in 𝓝 (0 : 𝕊), h • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
  this.eventually (EMetric.ball_mem_nhds _ hpos)
[GOAL]
𝕂 : 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 (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
[PROOFSTEP]
filter_upwards [this] with h hh
[GOAL]
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 (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
[PROOFSTEP]
have : Commute (t • x) (h • x) := ((Commute.refl x).smul_left t).smul_right h
[GOAL]
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 (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
[PROOFSTEP]
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]
[GOAL]
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x))) t
[PROOFSTEP]
convert hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1
[GOAL]
case h.e'_10
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x)) =
    exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x
[PROOFSTEP]
ext t'
[GOAL]
case h.e'_10.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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
t' : 𝕊
⊢ ↑(ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x))) t' =
    ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t'
[PROOFSTEP]
show Commute (t' • x) (exp 𝕂 (t • x))
[GOAL]
case h.e'_10.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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
t' : 𝕊
⊢ Commute (t' • x) (exp 𝕂 (t • x))
[PROOFSTEP]
exact (((Commute.refl x).smul_left t').smul_right t).exp_right 𝕂
[GOAL]
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasStrictFDerivAt (fun u => exp 𝕂 (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x))) t
[PROOFSTEP]
let ⟨_, _⟩ := analyticAt_exp_of_mem_ball (t • x) htx
[GOAL]
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸
h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)
⊢ HasStrictFDerivAt (fun u => exp 𝕂 (u • x))
    (ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x))) t
[PROOFSTEP]
convert hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1
[GOAL]
case h.e'_10
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸
h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)
⊢ ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x)) =
    exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x
[PROOFSTEP]
ext t'
[GOAL]
case h.e'_10.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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸
h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)
t' : 𝕊
⊢ ↑(ContinuousLinearMap.smulRight (ContinuousLinearMap.smulRight 1 x) (exp 𝕂 (t • x))) t' =
    ↑(exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t'
[PROOFSTEP]
show Commute (t' • x) (exp 𝕂 (t • x))
[GOAL]
case h.e'_10.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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸
h✝ : HasFPowerSeriesAt (exp 𝕂) w✝ (t • x)
t' : 𝕊
⊢ Commute (t' • x) (exp 𝕂 (t • x))
[PROOFSTEP]
exact (((Commute.refl x).smul_left t').smul_right t).exp_right 𝕂
[GOAL]
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasStrictDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t
[PROOFSTEP]
simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx).hasStrictDerivAt
[GOAL]
𝕂 : 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 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasStrictDerivAt (fun u => exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t
[PROOFSTEP]
simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 x t htx).hasStrictDerivAt
