meromorphicOrderAt_riemannZeta_ne_top

theorem meromorphicOrderAt_riemannZeta_ne_top (z : ℂ) : meromorphicOrderAt riemannZeta z ≠ ⊤ := by  rcases eq_or_ne z 1 with h | h  · subst h    exact (meromorphicOrderAt_ne_top_iff_eventually_ne_zero (meromorphicAt_riemannZeta 1)).2      riemannZeta_eventually_ne_zero  · have hz1 : z ∈ ({(1 : ℂ)}ᶜ : Set ℂ) := h    rw [(riemannZeta_analyticOn_compl_one z hz1).meromorphicOrderAt_eq, Ne, ENat.map_eq_top_iff]    have h2 : (2 : ℂ) ∈ ({(1 : ℂ)}ᶜ : Set ℂ) := by simp    have hconn : IsPreconnected ({(1 : ℂ)}ᶜ : Set ℂ) :=      (isConnected_compl_singleton_of_one_lt_rank (by simp) 1).isPreconnected    have hord2 : analyticOrderAt riemannZeta 2 ≠ ⊤ := by      rw [(riemannZeta_analyticOn_compl_one 2 h2).analyticOrderAt_eq_zero.mpr        (riemannZeta_ne_zero_of_one_le_re (by norm_num))]; simp    exact riemannZeta_analyticOn_compl_one.analyticOrderAt_ne_top_of_isPreconnected hconn h2 hz1 hord2