x : ℂ
⊢ exp x = _root_.exp ℂ x
⊢ exp = _root_.exp ℂ
refine' funext fun x => _
x : ℂ
⊢ CauSeq.lim (exp' x) = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
x : ℂ
⊢ exp x = _root_.exp ℂ x
rw [Complex.exp, exp_eq_tsum_div]
x : ℂ
this : CauSeq.IsComplete ℂ norm
⊢ CauSeq.lim (exp' x) = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
x : ℂ
⊢ CauSeq.lim (exp' x) = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
have : CauSeq.IsComplete ℂ norm := Complex.instIsComplete
no goals
x : ℂ
this : CauSeq.IsComplete ℂ norm
⊢ CauSeq.lim (exp' x) = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable ℝ x).hasSum.tendsto_sum_nat