AnalyticOn_divRemovable_zero_closedBall

@[blueprint "AnalyticOn_divRemovable_zero_closedBall"  (title := "AnalyticOn-divRemovable-zero-closedBall")  (statement := /--    Let $f$ be a complex function analytic on the closed ball    $|z|\leq R$ such that $f(0)=0$.    Then, with $g$ defined as in    Definition~\ref{divRemovable_zero}, $g$ is analytic on    $|z|\leq R$.  -/)  (proof := /--    The proof is similar to that of    Lemma~\ref{AnalyticOn_divRemovable_zero}, but we need to    consider two cases: when $x$ is on the boundary of the closed    ball and when it is in the interior.    In the first case, we take a small open ball around $x$ that    lies entirely within the closed ball, and apply    Lemma~\ref{AnalyticOn_divRemovable_zero} on this smaller ball.    In the second case, we can take the entire open ball centered    at $0$ with radius $R$, and again apply    Lemma~\ref{AnalyticOn_divRemovable_zero}.    In both cases, we use the fact that $f(0)=0$ to ensure that    the removable singularity at $0$ is handled correctly.  -/)  (latexEnv := "lemma")]lemma AnalyticOn_divRemovable_zero_closedBall {f : ℂ → ℂ}    {R : ℝ} (Rpos : 0 < R)    (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R))    (zero : f 0 = 0) :    AnalyticOn ℂ (divRemovable_zero f) (Metric.closedBall 0 R) := by  apply analyticOn_of_locally_analyticOn  intro x x_hyp  simp only [Metric.mem_closedBall, dist_zero_right] at x_hyp  cases x_hyp.eq_or_lt with  | inl h =>    use Metric.ball x (R / 2)    refine ⟨Metric.isOpen_ball, ?_, ?_⟩    · simp [Rpos]    · have (x₂) (hyp_x₂ : x₂ ∈ Metric.closedBall 0 R ∩ Metric.ball x (R / 2)) : x₂ ≠ 0 := by        rw [ball_eq, Set.mem_inter_iff, Metric.mem_closedBall, dist_zero_right,          Set.mem_setOf_eq] at hyp_x₂        rw [← norm_pos_iff]        calc 0          _ < R - ‖x₂ - x‖ := by            obtain ⟨-, v⟩ := hyp_x₂            linarith          _ = ‖x‖ - ‖x - x₂‖ := by            rw [h, norm_sub_rev]          _ ≤ ‖x - (x - x₂)‖ := norm_sub_norm_le ..          _ ≤ ‖x₂‖ := by rw [sub_sub_cancel]      apply AnalyticOn.congr      · exact (analytic.mono Set.inter_subset_left).div analyticOn_id this      · intro x₃ hyp_x₃        exact divRemovable_zero_of_ne_zero _ (this _ hyp_x₃)  | inr h =>    use Metric.ball 0 R    refine ⟨Metric.isOpen_ball, ?_, ?_⟩    · simp only [ball_eq, sub_zero, Set.mem_setOf_eq, h]    · have si : Metric.closedBall (0 : ℂ) R ∩ Metric.ball (0 : ℂ) R =        Metric.ball (0 : ℂ) R := by        apply Set.inter_eq_self_of_subset_right        exact Metric.ball_subset_closedBall      rw [si]      exact AnalyticOn_divRemovable_zero        (Metric.ball_mem_nhds 0 Rpos)        zero Metric.isOpen_ball        (analytic.mono Metric.ball_subset_closedBall)