meromorphicAt_riemannZeta

theorem meromorphicAt_riemannZeta (s : ℂ) : MeromorphicAt riemannZeta s := by  have hΛ : MeromorphicAt completedRiemannZeta s := by    rw [show completedRiemannZeta = fun z ↦ completedRiemannZeta₀ z - 1 / z - 1 / (1 - z) from      funext completedRiemannZeta_eq]    exact (((differentiable_completedZeta₀.analyticAt s).meromorphicAt.sub      ((MeromorphicAt.const 1 s).div analyticAt_id.meromorphicAt)).sub      ((MeromorphicAt.const 1 s).div ((analyticAt_const.sub analyticAt_id).meromorphicAt)))  have hG : MeromorphicAt Gammaℝ s := by    rw [show Gammaℝ = fun z ↦ (Real.pi : ℂ) ^ (-z / 2) * Complex.Gamma (z / 2) from funext Gammaℝ_def]    refine MeromorphicAt.mul (AnalyticAt.meromorphicAt ?_)      (MeromorphicAt.comp_analyticAt (f := Complex.Gamma) (g := fun z : ℂ ↦ z / 2) (x := s)        ((MeromorphicOn.Gamma (s := Set.univ)) (s / 2) (Set.mem_univ _)) (by fun_prop))    rw [show (fun z : ℂ ↦ (Real.pi : ℂ) ^ (-z / 2))        = fun z ↦ Complex.exp (Complex.log (Real.pi : ℂ) * (-z / 2)) from by      funext z; rw [Complex.cpow_def_of_ne_zero (by simp [Real.pi_ne_zero])]]    fun_prop  have hz0 : ∀ᶠ z in 𝓝[≠] s, z ≠ 0 := by    rcases eq_or_ne s 0 with h | h    · subst h; exact self_mem_nhdsWithin    · exact (isOpen_compl_singleton.eventually_mem (Set.mem_compl_singleton_iff.mpr h)).filter_mono        nhdsWithin_le_nhds  exact (hΛ.div hG).congr ((by filter_upwards [hz0] with z hz using riemannZeta_def_of_ne_zero hz :    riemannZeta =ᶠ[𝓝[≠] s] fun z ↦ completedRiemannZeta z / Gammaℝ z)).symm