CH2.B.continuous_zero

@[blueprint  "B-cts"  (title := "Continuity of $B^\\pm$ at $0$")  (statement := /--  $B^\pm$ is continuous at $0$.  -/)  (proof := /-- L'H\^opital's rule can be applied to show the continuity at $0$. -/)  (latexEnv := "lemma")]theorem B.continuous_zero (ε : ℝ) : ContinuousAt (B ε) 0 := by  have h_lim : Filter.Tendsto (fun s : ℂ => s * (Complex.cosh (s / 2)) / (2 * Complex.sinh (s / 2)) + ε * s / 2) (nhdsWithin 0 {0}ᶜ) (nhds 1) := by    have h_sinh : Filter.Tendsto (fun s : ℂ => Complex.sinh (s / 2) / s) (nhdsWithin 0 {0}ᶜ) (nhds (1 / 2)) := by        simpa [div_eq_inv_mul] using HasDerivAt.tendsto_slope_zero          (HasDerivAt.comp 0 (Complex.hasDerivAt_sinh _)            (hasDerivAt_id 0 |> HasDerivAt.div_const <| 2))    have h_lim : Filter.Tendsto (fun s : ℂ => s / (2 * Complex.sinh (s / 2))) (nhdsWithin 0 {0}ᶜ) (nhds 1) := by      convert h_sinh.inv₀ (by norm_num : (1 / 2 : ℂ) ≠ 0) |>        Filter.Tendsto.const_mul 2⁻¹ using 2 <;> norm_num; ring    simpa [mul_div_right_comm] using Filter.Tendsto.add      (h_lim.mul (Complex.continuous_cosh.continuousAt.tendsto.comp        (continuousWithinAt_id.div_const 2)))      (Filter.Tendsto.div_const (tendsto_const_nhds.mul continuousWithinAt_id) 2)  rw [Metric.tendsto_nhdsWithin_nhds] at h_lim  rw [Metric.continuousAt_iff]  intro ε hε; rcases h_lim ε hε with ⟨δ, hδ, H⟩; use δ, hδ; intro x hx  by_cases hx' : x = 0  · simp_all [B]  simp_all only [gt_iff_lt, Set.mem_compl_iff, Set.mem_singleton_iff, dist_zero_right, B,    ↓reduceIte]  convert H hx' hx using 1; norm_num [coth]  norm_num [Complex.tanh_eq_sinh_div_cosh]; ring_nf