CH2.analyticAt_B

theorem analyticAt_B (ε : ℝ) (z₀ : ℂ) (h_not_pole : ∀ n : ℤ, n ≠ 0 → z₀ ≠ 2 * π * I * n) :    AnalyticAt ℂ (B ε) z₀ := by  apply analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt  · obtain ⟨V, hV_nhds, b, hb, hV_anal⟩ := (meromorphicAt_B ε z₀).eventually_analyticAt    filter_upwards [nhdsWithin_le_nhds hV_nhds, self_mem_nhdsWithin] with w hw hne    have : w ∈ V ∩ b := ⟨hw, hb hne⟩    have h_an : AnalyticAt ℂ (B ε) w := by rwa [← hV_anal] at this    exact h_an.differentiableAt  · unfold B    by_cases h0 : z₀ = 0    · subst h0      have h_lim : Filter.Tendsto (fun s ↦ s * (coth (s / 2) + ε) / 2) (nhdsWithin 0 {0}ᶜ) (nhds 1) := by        have h1 : Filter.Tendsto (fun s ↦ (s / 2) / Complex.sinh (s / 2)) (nhdsWithin 0 {0}ᶜ) (nhds 1) := by          have h_deriv : HasDerivAt (fun s ↦ Complex.sinh (s / 2)) (1 / 2) 0 := by            have h := (Complex.hasDerivAt_sinh (0 / 2)).comp 0 ((hasDerivAt_id (0 : ℂ)).div_const 2)            simp only [zero_div, Complex.cosh_zero, id_eq] at h            convert! h using 1; ring          rw [hasDerivAt_iff_tendsto_slope] at h_deriv          rw [slope_fun_def_field] at h_deriv          simp only [Complex.sinh_zero, sub_zero, zero_div] at h_deriv          have h_inv := h_deriv.inv₀ (by norm_num)          field_simp [mul_comm] at h_inv          convert h_inv.div_const 2 using 1          · ext s; field_simp          · simp        have h_lim' : Filter.Tendsto (fun s ↦ ((s / 2) / Complex.sinh (s / 2)) * Complex.cosh (s / 2) + s * ε / 2) (nhdsWithin 0 {0}ᶜ) (nhds (1 * 1 + 0 * ε / 2)) := by          apply Filter.Tendsto.add          · apply Filter.Tendsto.mul h1            have : Filter.Tendsto (fun s ↦ Complex.cosh (s / 2)) (nhds 0) (nhds (Complex.cosh (0 / 2))) := by              apply (Complex.continuous_cosh.continuousAt.comp (continuous_id.div_const 2).continuousAt).tendsto            simp only [zero_div, Complex.cosh_zero] at this            exact this.mono_left nhdsWithin_le_nhds          · apply Filter.Tendsto.div_const            apply Filter.Tendsto.mul (Filter.tendsto_id.mono_left nhdsWithin_le_nhds) tendsto_const_nhds        simp only [mul_one, zero_mul, zero_div, add_zero] at h_lim'        refine h_lim'.congr' ?_        filter_upwards [self_mem_nhdsWithin] with s hs        rw [coth, Complex.tanh_eq_sinh_div_cosh]        field_simp      rw [continuousAt_iff_punctured_nhds]      simp only [↓reduceIte]      apply h_lim.congr'      · filter_upwards [self_mem_nhdsWithin] with s hs        split_ifs with h        · contradiction        · rfl    · have h_eq : (fun s ↦ if s = 0 then 1 else s * (coth (s / 2) + ε) / 2) =ᶠ[nhds z₀]          (fun s ↦ s * (coth (s / 2) + ε) / 2) := by        filter_upwards [continuous_id.continuousAt.eventually_ne h0] with s hs        split_ifs with h_s0        · contradiction        · rfl      apply ContinuousAt.congr_of_eventuallyEq _ h_eq      apply ContinuousAt.div_const      apply ContinuousAt.mul continuousAt_id      apply ContinuousAt.add _ continuousAt_const      apply ContinuousAt.coth (continuousAt_id.div_const 2)      intro hc      rw [sinh_zero_iff] at hc      obtain ⟨n, hn⟩ := hc      have : z₀ = 2 * π * I * n := by        simp only [id_eq] at hn        field_simp [hn]        linear_combination 2 * hn      by_cases hn0 : n = 0      · subst hn0; simp at this; contradiction      · exact h_not_pole n hn0 this