riemannZeta_eq_zetaAbelContinuationFormula

theorem riemannZeta_eq_zetaAbelContinuationFormula (s : ℂ) (hs : s ∈ zetaAbelContinuationDomain) :    riemannZeta s = zetaAbelContinuationFormula s := by  have hUo := isOpen_zetaAbelContinuationDomain  have hζ : AnalyticOnNhd ℂ riemannZeta zetaAbelContinuationDomain := by    rw [← hUo.analyticOn_iff_analyticOnNhd]    have h : AnalyticOn ℂ riemannZeta ({1} : Set ℂ)ᶜ :=      isOpen_compl_singleton.analyticOn_iff_analyticOnNhd.mpr analyticOn_riemannZeta    exact AnalyticOn.mono h fun _ hz => hz.1  have hF : AnalyticOnNhd ℂ zetaAbelContinuationFormula zetaAbelContinuationDomain := by    rw [← hUo.analyticOn_iff_analyticOnNhd]    exact analyticOn_zetaAbelContinuationFormula  have hEq : riemannZeta =ᶠ[𝓝 (2 : ℂ)] zetaAbelContinuationFormula := by    have hopen : IsOpen {w : ℂ | 1 < w.re} :=      isOpen_lt continuous_const Complex.continuous_re    filter_upwards [hopen.mem_nhds (by norm_num : (1 : ℝ) < (2 : ℂ).re)] with w hw      using riemannZeta_abel_integral w hw  exact (AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq    hζ hF isPreconnected_zetaAbelContinuationDomain two_mem_zetaAbelContinuationDomain hEq) hs