CH2.meromorphicAt_B

lemma meromorphicAt_B (ε : ℝ) (z₀ : ℂ) : MeromorphicAt (B ε) z₀ := by  have h_comp : ∀ z, MeromorphicAt      (fun s => s * (Complex.cosh (s / 2) / Complex.sinh (s / 2) + ε) / 2) z := by    have meromorphic_coth'' := meromorphic_coth''    intro z    exact (by apply_rules [MeromorphicAt.div, MeromorphicAt.add, MeromorphicAt.mul,      MeromorphicAt.id, MeromorphicAt.const])  specialize h_comp z₀  convert h_comp.congr _  rw [Filter.EventuallyEq, eventually_nhdsWithin_iff]  unfold B  rw [Metric.eventually_nhds_iff]  by_cases h : z₀ = 0  · simp_all only [gt_iff_lt, dist_zero_right, Set.mem_compl_iff, Set.mem_singleton_iff,      ↓reduceIte, coth, one_div, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_left_inj',        mul_eq_mul_left_iff, add_left_inj, or_false]    norm_num [Complex.tanh_eq_sinh_div_cosh]    exact ⟨1, by norm_num⟩  · simp_all only [gt_iff_lt, Set.mem_compl_iff, Set.mem_singleton_iff, coth, one_div]    exact ⟨‖z₀‖, norm_pos_iff.mpr h, fun y hy hy' => by      rw [Complex.tanh_eq_sinh_div_cosh]; aesop⟩