AnalyticOn_divRemovable_zero

@[blueprint "AnalyticOn_divRemovable_zero"  (title := "AnalyticOn-divRemovable-zero")  (statement := /--    Let $f$ be a complex function analytic on an open set $s$    containing $0$ such that $f(0)=0$.    Then, with $g$ defined as in    Definition~\ref{divRemovable_zero}, $g$ is analytic on $s$.  -/)  (proof := /--    We need to show that $g$ is complex differentiable at every    point in $s$. For $z\neq 0$, this follows directly from the    definition of $g$ and the fact that $f$ is analytic on $s$.    For $z=0$, we use the definition of the derivative and the    fact that $f(0)=0$:    \[    \lim_{z\to 0}\frac{g(z)-g(0)}{z-0}    =\lim_{z\to 0}\frac{\frac{f(z)}{z}-f'(0)}{z}    =\lim_{z\to 0}\frac{f(z)-f'(0)z}{z^2}    =\lim_{z\to 0}\frac{f(z)-f(0)-f'(0)(z-0)}{(z-0)^2}=0,    \]    where the last equality follows from the definition of the    derivative of $f$ at $0$. Thus, $g$ is complex differentiable    at $0$ with derivative $0$, completing the proof.  -/)  (latexEnv := "lemma")]lemma AnalyticOn_divRemovable_zero {f : ℂ → ℂ} {s : Set ℂ}    (sInNhds0 : s ∈ nhds 0) (zero : f 0 = 0) (o : IsOpen s)    (analytic : AnalyticOn ℂ f s) :    AnalyticOn ℂ (divRemovable_zero f) s := by  rw [Complex.analyticOn_iff_differentiableOn o,    ← Complex.differentiableOn_compl_singleton_and_continuousAt_iff sInNhds0]  constructor  · have (x) (hx : x ∈ s \ {0}) : x ≠ 0 := by      rw [Set.mem_sdiff, Set.mem_singleton_iff] at hx      exact hx.right    rw [differentiableOn_congr (fun x hyp_x => Function.update_of_ne (this x hyp_x) _ _)]    exact      (analytic.mono Set.sdiff_subset).differentiableOn.fun_div      (differentiableOn_id.mono (Set.subset_univ (s \ {0})))      this  · have U :=      HasDerivAt.continuousAt_div (c := 0) (a := deriv f 0)        (f := f)        (DifferentiableOn.hasDerivAt          ((Complex.analyticOn_iff_differentiableOn o).mp analytic)          sInNhds0)    simpa [divRemovable_zero, zero] using U