-- Mathlib/Analysis/SpecialFunctions/Exponential.lean
theorem hasFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸}
    (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasFDerivAt (exp 𝕂) (exp 𝕂 x • (1 : 𝔸 →L[𝕂] 𝔸)) x

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ HasFDerivAt (exp 𝕂) (exp 𝕂 x • 1) x

Tactic:
have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt hx

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
⊢ HasFDerivAt (exp 𝕂) (exp 𝕂 x • 1) x

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
⊢ (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

Tactic:
have : ∀ᶠ h in 𝓝 (0 : 𝔸), h ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
  EMetric.ball_mem_nhds _ hpos

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ (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

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
⊢ HasFDerivAt (exp 𝕂) (exp 𝕂 x • 1) x

Tactic:
rw [hasFDerivAt_iff_isLittleO_nhds_zero]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
⊢ (fun h => exp 𝕂 (x + h) - exp 𝕂 x - (exp 𝕂 x • 1) h) =o[𝓝 0] fun h => h

Proof state:
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ exp 𝕂 x * (exp 𝕂 (0 + a✝) - exp 𝕂 0 - (ContinuousLinearMap.id 𝕂 𝔸) a✝) =
    exp 𝕂 (x + a✝) - exp 𝕂 x - exp 𝕂 x • (ContinuousLinearMap.id 𝕂 𝔸) a✝

Tactic:
rw [exp_add_of_mem_ball hx hh, exp_zero, zero_add, ContinuousLinearMap.id_apply, smul_eq_mul]

Result:
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ exp 𝕂 x * (exp 𝕂 a✝ - 1 - a✝) = exp 𝕂 x * exp 𝕂 a✝ - exp 𝕂 x - exp 𝕂 x * a✝

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
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

Tactic:
rw [← hasFDerivAt_iff_isLittleO_nhds_zero]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
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

Proof state:
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ exp 𝕂 x * (exp 𝕂 a✝ - 1 - a✝) = exp 𝕂 x * exp 𝕂 a✝ - exp 𝕂 x - exp 𝕂 x * a✝

Tactic:
ring

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
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

Tactic:
exact hasFDerivAt_exp_zero_of_radius_pos hpos

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
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

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

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
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