Theorem: AnalyticOn.exp (Ray/Analytic/HolomorphicUpstream.lean)

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
⊢ AnalyticOn ℂ Complex.exp univ
Tactic:
rw [analyticOn_univ_iff_differentiable]
State after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
⊢ Differentiable ℂ Complex.exp

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
⊢ Differentiable ℂ Complex.exp
Tactic:
exact Complex.differentiable_exp
State after:
no goals