feat: complex differentiable functions are continuously differentiable (

#5629)

Mathlib/Analysis/Analytic/Basic.lean

@@ -1379,6 +1379,16 @@ theorem isOpen_analyticAt : IsOpen { x | AnalyticAt 𝕜 f x } := by
   exact mem_of_superset (EMetric.ball_mem_nhds _ hr.r_pos) fun y hy => hr.analyticAt_of_mem hy
 #align is_open_analytic_at isOpen_analyticAt
 
+variable {𝕜}
+
+theorem AnalyticAt.eventually_analyticAt {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) :
+    ∀ᶠ y in 𝓝 x, AnalyticAt 𝕜 f y :=
+(isOpen_analyticAt 𝕜 f).mem_nhds h
+
+theorem AnalyticAt.exists_mem_nhds_analyticOn {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) :
+    ∃ s ∈ 𝓝 x, AnalyticOn 𝕜 f s :=
+h.eventually_analyticAt.exists_mem
+
 end
 
 section

Mathlib/Analysis/Calculus/FDerivAnalytic.lean

@@ -161,6 +161,11 @@ theorem AnalyticOn.contDiffOn [CompleteSpace F] (h : AnalyticOn 𝕜 f s) {n : 
     exact iteratedFDerivWithin_of_isOpen _ t_open hx
 #align analytic_on.cont_diff_on AnalyticOn.contDiffOn
 
+theorem AnalyticAt.contDiffAt [CompleteSpace F] (h : AnalyticAt 𝕜 f x) {n : ℕ∞} :
+    ContDiffAt 𝕜 n f x := by
+  obtain ⟨s, hs, hf⟩ := h.exists_mem_nhds_analyticOn
+  exact hf.contDiffOn.contDiffAt hs
+
 end fderiv
 
 section deriv

Mathlib/Analysis/Complex/CauchyIntegral.lean

@@ -15,6 +15,7 @@ import Mathlib.Analysis.Calculus.Dslope
 import Mathlib.Analysis.Analytic.Basic
 import Mathlib.Analysis.Complex.ReImTopology
 import Mathlib.Analysis.Calculus.DiffContOnCl
+import Mathlib.Analysis.Calculus.FDerivAnalytic
 import Mathlib.Data.Real.Cardinality
 
 /-!
@@ -605,12 +606,23 @@ theorem _root_.DifferentiableOn.analyticOn {s : Set ℂ} {f : ℂ → E} (hd : D
     (hs : IsOpen s) : AnalyticOn ℂ f s := fun _z hz => hd.analyticAt (hs.mem_nhds hz)
 #align differentiable_on.analytic_on DifferentiableOn.analyticOn
 
+/-- If `f : ℂ → E` is complex differentiable on some open set `s`, then it is continuously
+differentiable on `s`. -/
+protected theorem _root_.DifferentiableOn.contDiffOn {s : Set ℂ} {f : ℂ → E}
+    (hd : DifferentiableOn ℂ f s) (hs : IsOpen s) : ContDiffOn ℂ n f s :=
+  (hd.analyticOn hs).contDiffOn
+
 /-- A complex differentiable function `f : ℂ → E` is analytic at every point. -/
 protected theorem _root_.Differentiable.analyticAt {f : ℂ → E} (hf : Differentiable ℂ f) (z : ℂ) :
     AnalyticAt ℂ f z :=
   hf.differentiableOn.analyticAt univ_mem
 #align differentiable.analytic_at Differentiable.analyticAt
 
+/-- A complex differentiable function `f : ℂ → E` is continuously differentiable at every point. -/
+protected theorem _root_.Differentiable.contDiff {f : ℂ → E} (hf : Differentiable ℂ f) {n : ℕ∞} :
+    ContDiff ℂ n f :=
+  contDiff_iff_contDiffAt.mpr $ fun z ↦ (hf.analyticAt z).contDiffAt
+
 /-- When `f : ℂ → E` is differentiable, the `cauchyPowerSeries f z R` represents `f` as a power
 series centered at `z` in the entirety of `ℂ`, regardless of `R : ℝ≥0`, with  `0 < R`. -/
 protected theorem _root_.Differentiable.hasFPowerSeriesOnBall {f : ℂ → E} (h : Differentiable ℂ f)