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)
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ HasStrictFDerivAt (exp 𝕂) 1 0
convert (hasFPowerSeriesAt_exp_zero_of_radius_pos h).hasStrictFDerivAt
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
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)
ext x
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
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
change x = expSeries 𝕂 𝔸 1 fun _ => x
no goals
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
simp [expSeries_apply_eq]